Theorem disjor 4411

Description: Two ways to say that a collection B ( i ) for i e. A is disjoint. (Contributed by Mario Carneiro, 26-Mar-2015.) (Revised by Mario Carneiro, 14-Nov-2016.)

Hypothesis

Ref	Expression
disjor.1	|- ( i = j -> B = C )

Assertion

Ref	Expression
disjor	|- (Disj i e. A B <-> A. i e. A A. j e. A ( i = j \/ ( B i^i C ) = (/) ) )

Distinct variable groups:   i, j, A   B, j   C, i

Allowed substitution hints:   B( i)   C( j)

Proof of Theorem disjor

Dummy variable x is distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-disj 4398	. 2 |- (Disj i e. A B <-> A. x E* i e. A x e. B )
2		ralcom4 3106	. . 3 |- ( A. i e. A A. x A. j e. A ( ( x e. B /\ x e. C ) -> i = j ) <-> A. x A. i e. A A. j e. A ( ( x e. B /\ x e. C ) -> i = j ) )
3		orcom 388	. . . . . . 7 |- ( ( i = j \/ ( B i^i C ) = (/) ) <-> ( ( B i^i C ) = (/) \/ i = j ) )
4		df-or 371	. . . . . . 7 |- ( ( ( B i^i C ) = (/) \/ i = j ) <-> ( -. ( B i^i C ) = (/) -> i = j ) )
5		neq0 3778	. . . . . . . . . 10 |- ( -. ( B i^i C ) = (/) <-> E. x x e. ( B i^i C ) )
6		elin 3655	. . . . . . . . . . 11 |- ( x e. ( B i^i C ) <-> ( x e. B /\ x e. C ) )
7	6	exbii 1714	. . . . . . . . . 10 |- ( E. x x e. ( B i^i C ) <-> E. x ( x e. B /\ x e. C ) )
8	5, 7	bitri 252	. . . . . . . . 9 |- ( -. ( B i^i C ) = (/) <-> E. x ( x e. B /\ x e. C ) )
9	8	imbi1i 326	. . . . . . . 8 |- ( ( -. ( B i^i C ) = (/) -> i = j ) <-> ( E. x ( x e. B /\ x e. C ) -> i = j ) )
10		19.23v 1810	. . . . . . . 8 |- ( A. x ( ( x e. B /\ x e. C ) -> i = j ) <-> ( E. x ( x e. B /\ x e. C ) -> i = j ) )
11	9, 10	bitr4i 255	. . . . . . 7 |- ( ( -. ( B i^i C ) = (/) -> i = j ) <-> A. x ( ( x e. B /\ x e. C ) -> i = j ) )
12	3, 4, 11	3bitri 274	. . . . . 6 |- ( ( i = j \/ ( B i^i C ) = (/) ) <-> A. x ( ( x e. B /\ x e. C ) -> i = j ) )
13	12	ralbii 2863	. . . . 5 |- ( A. j e. A ( i = j \/ ( B i^i C ) = (/) ) <-> A. j e. A A. x ( ( x e. B /\ x e. C ) -> i = j ) )
14		ralcom4 3106	. . . . 5 |- ( A. j e. A A. x ( ( x e. B /\ x e. C ) -> i = j ) <-> A. x A. j e. A ( ( x e. B /\ x e. C ) -> i = j ) )
15	13, 14	bitri 252	. . . 4 |- ( A. j e. A ( i = j \/ ( B i^i C ) = (/) ) <-> A. x A. j e. A ( ( x e. B /\ x e. C ) -> i = j ) )
16	15	ralbii 2863	. . 3 |- ( A. i e. A A. j e. A ( i = j \/ ( B i^i C ) = (/) ) <-> A. i e. A A. x A. j e. A ( ( x e. B /\ x e. C ) -> i = j ) )
17		disjor.1	. . . . . 6 |- ( i = j -> B = C )
18	17	eleq2d 2499	. . . . 5 |- ( i = j -> ( x e. B <-> x e. C ) )
19	18	rmo4 3270	. . . 4 |- ( E* i e. A x e. B <-> A. i e. A A. j e. A ( ( x e. B /\ x e. C ) -> i = j ) )
20	19	albii 1687	. . 3 |- ( A. x E* i e. A x e. B <-> A. x A. i e. A A. j e. A ( ( x e. B /\ x e. C ) -> i = j ) )
21	2, 16, 20	3bitr4i 280	. 2 |- ( A. i e. A A. j e. A ( i = j \/ ( B i^i C ) = (/) ) <-> A. x E* i e. A x e. B )
22	1, 21	bitr4i 255	1 |- (Disj i e. A B <-> A. i e. A A. j e. A ( i = j \/ ( B i^i C ) = (/) ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 187   \/ wo 369   /\ wa 370   A.wal 1435   = wceq 1437   E.wex 1659   e. wcel 1870   A.wral 2782   E*wrmo 2785   i^i cin 3441   (/)c0 3767  Disj wdisj 4397

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-eu 2270  df-mo 2271  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-ne 2627  df-ral 2787  df-rmo 2790  df-v 3089  df-dif 3445  df-in 3449  df-nul 3768  df-disj 4398

This theorem is referenced by:  disjors  4412  disjxiun  4423  disjxun  4424  otsndisj  4726  otiunsndisj  4727  qsdisj2  7449  cshwsdisj  15032  dyadmbl  22435  2spotdisj  25634  2spotiundisj  25635  2spotmdisj  25641  numclwwlkdisj  25653  disjnf  28020  disjorsf  28029  poimirlem26  31669  mblfinlem2  31681  ndisj2  37029  nnfoctbdjlem  37801  iundjiun  37806  otiunsndisjX  38377