Theorem disjor 4359

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 4346	. 2 |- (Disj i e. A B <-> A. x E* i e. A x e. B )
2		ralcom4 3034	. . 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 393	. . . . . . 7 |- ( ( i = j \/ ( B i^i C ) = (/) ) <-> ( ( B i^i C ) = (/) \/ i = j ) )
4		df-or 376	. . . . . . 7 |- ( ( ( B i^i C ) = (/) \/ i = j ) <-> ( -. ( B i^i C ) = (/) -> i = j ) )
5		neq0 3710	. . . . . . . . . 10 |- ( -. ( B i^i C ) = (/) <-> E. x x e. ( B i^i C ) )
6		elin 3585	. . . . . . . . . . 11 |- ( x e. ( B i^i C ) <-> ( x e. B /\ x e. C ) )
7	6	exbii 1722	. . . . . . . . . 10 |- ( E. x x e. ( B i^i C ) <-> E. x ( x e. B /\ x e. C ) )
8	5, 7	bitri 257	. . . . . . . . 9 |- ( -. ( B i^i C ) = (/) <-> E. x ( x e. B /\ x e. C ) )
9	8	imbi1i 331	. . . . . . . 8 |- ( ( -. ( B i^i C ) = (/) -> i = j ) <-> ( E. x ( x e. B /\ x e. C ) -> i = j ) )
10		19.23v 1822	. . . . . . . 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 260	. . . . . . 7 |- ( ( -. ( B i^i C ) = (/) -> i = j ) <-> A. x ( ( x e. B /\ x e. C ) -> i = j ) )
12	3, 4, 11	3bitri 279	. . . . . 6 |- ( ( i = j \/ ( B i^i C ) = (/) ) <-> A. x ( ( x e. B /\ x e. C ) -> i = j ) )
13	12	ralbii 2804	. . . . 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 3034	. . . . 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 257	. . . 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 2804	. . 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 2515	. . . . 5 |- ( i = j -> ( x e. B <-> x e. C ) )
19	18	rmo4 3199	. . . 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 1695	. . 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 285	. 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 260	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 189   \/ wo 374   /\ wa 375   A.wal 1446   = wceq 1448   E.wex 1667   e. wcel 1891   A.wral 2737   E*wrmo 2740   i^i cin 3371   (/)c0 3699  Disj wdisj 4345

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1673  ax-4 1686  ax-5 1762  ax-6 1809  ax-7 1855  ax-10 1919  ax-11 1924  ax-12 1937  ax-13 2092  ax-ext 2432

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-tru 1451  df-ex 1668  df-nf 1672  df-sb 1802  df-eu 2304  df-mo 2305  df-clab 2439  df-cleq 2445  df-clel 2448  df-nfc 2582  df-ne 2624  df-ral 2742  df-rmo 2745  df-v 3015  df-dif 3375  df-in 3379  df-nul 3700  df-disj 4346

This theorem is referenced by:  disjors  4360  disjxiun  4371  disjxun  4372  otsndisj  4679  otiunsndisj  4680  qsdisj2  7428  cshwsdisj  15080  dyadmbl  22570  2spotdisj  25801  2spotiundisj  25802  2spotmdisj  25808  numclwwlkdisj  25820  disjnf  28191  disjorsf  28200  poimirlem26  31968  mblfinlem2  31980  ndisj2  37384  nnfoctbdjlem  38354  iundjiun  38359  otiunsndisjX  39098