Theorem disjor 4408

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 4395	. 2 |- (Disj i e. A B <-> A. x E* i e. A x e. B )
2		ralcom4 3100	. . 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 3772	. . . . . . . . . 10 |- ( -. ( B i^i C ) = (/) <-> E. x x e. ( B i^i C ) )
6		elin 3649	. . . . . . . . . . 11 |- ( x e. ( B i^i C ) <-> ( x e. B /\ x e. C ) )
7	6	exbii 1712	. . . . . . . . . 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 1811	. . . . . . . 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 2853	. . . . 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 3100	. . . . 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 2853	. . 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 2492	. . . . 5 |- ( i = j -> ( x e. B <-> x e. C ) )
19	18	rmo4 3263	. . . 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 1685	. . 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 1657   e. wcel 1872   A.wral 2771   E*wrmo 2774   i^i cin 3435   (/)c0 3761  Disj wdisj 4394

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2273  df-mo 2274  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-ne 2616  df-ral 2776  df-rmo 2779  df-v 3082  df-dif 3439  df-in 3443  df-nul 3762  df-disj 4395

This theorem is referenced by:  disjors  4409  disjxiun  4420  disjxun  4421  otsndisj  4725  otiunsndisj  4726  qsdisj2  7452  cshwsdisj  15068  dyadmbl  22556  2spotdisj  25787  2spotiundisj  25788  2spotmdisj  25794  numclwwlkdisj  25806  disjnf  28183  disjorsf  28192  poimirlem26  31930  mblfinlem2  31942  ndisj2  37362  nnfoctbdjlem  38201  iundjiun  38206  otiunsndisjX  38871