Metamath Proof Explorer


Theorem disjxun

Description: The union of two disjoint collections. (Contributed by Mario Carneiro, 14-Nov-2016)

Ref Expression
Hypothesis disjxun.1 ( 𝑥 = 𝑦𝐶 = 𝐷 )
Assertion disjxun ( ( 𝐴𝐵 ) = ∅ → ( Disj 𝑥 ∈ ( 𝐴𝐵 ) 𝐶 ↔ ( Disj 𝑥𝐴 𝐶Disj 𝑥𝐵 𝐶 ∧ ∀ 𝑥𝐴𝑦𝐵 ( 𝐶𝐷 ) = ∅ ) ) )

Proof

Step Hyp Ref Expression
1 disjxun.1 ( 𝑥 = 𝑦𝐶 = 𝐷 )
2 disjel ( ( ( 𝐴𝐵 ) = ∅ ∧ 𝑥𝐴 ) → ¬ 𝑥𝐵 )
3 eleq1w ( 𝑥 = 𝑦 → ( 𝑥𝐵𝑦𝐵 ) )
4 3 notbid ( 𝑥 = 𝑦 → ( ¬ 𝑥𝐵 ↔ ¬ 𝑦𝐵 ) )
5 2 4 syl5ibcom ( ( ( 𝐴𝐵 ) = ∅ ∧ 𝑥𝐴 ) → ( 𝑥 = 𝑦 → ¬ 𝑦𝐵 ) )
6 5 con2d ( ( ( 𝐴𝐵 ) = ∅ ∧ 𝑥𝐴 ) → ( 𝑦𝐵 → ¬ 𝑥 = 𝑦 ) )
7 6 impr ( ( ( 𝐴𝐵 ) = ∅ ∧ ( 𝑥𝐴𝑦𝐵 ) ) → ¬ 𝑥 = 𝑦 )
8 biorf ( ¬ 𝑥 = 𝑦 → ( ( 𝐶𝐷 ) = ∅ ↔ ( 𝑥 = 𝑦 ∨ ( 𝐶𝐷 ) = ∅ ) ) )
9 7 8 syl ( ( ( 𝐴𝐵 ) = ∅ ∧ ( 𝑥𝐴𝑦𝐵 ) ) → ( ( 𝐶𝐷 ) = ∅ ↔ ( 𝑥 = 𝑦 ∨ ( 𝐶𝐷 ) = ∅ ) ) )
10 9 bicomd ( ( ( 𝐴𝐵 ) = ∅ ∧ ( 𝑥𝐴𝑦𝐵 ) ) → ( ( 𝑥 = 𝑦 ∨ ( 𝐶𝐷 ) = ∅ ) ↔ ( 𝐶𝐷 ) = ∅ ) )
11 10 2ralbidva ( ( 𝐴𝐵 ) = ∅ → ( ∀ 𝑥𝐴𝑦𝐵 ( 𝑥 = 𝑦 ∨ ( 𝐶𝐷 ) = ∅ ) ↔ ∀ 𝑥𝐴𝑦𝐵 ( 𝐶𝐷 ) = ∅ ) )
12 11 anbi2d ( ( 𝐴𝐵 ) = ∅ → ( ( ∀ 𝑥𝐴𝑦𝐴 ( 𝑥 = 𝑦 ∨ ( 𝐶𝐷 ) = ∅ ) ∧ ∀ 𝑥𝐴𝑦𝐵 ( 𝑥 = 𝑦 ∨ ( 𝐶𝐷 ) = ∅ ) ) ↔ ( ∀ 𝑥𝐴𝑦𝐴 ( 𝑥 = 𝑦 ∨ ( 𝐶𝐷 ) = ∅ ) ∧ ∀ 𝑥𝐴𝑦𝐵 ( 𝐶𝐷 ) = ∅ ) ) )
13 ralunb ( ∀ 𝑦 ∈ ( 𝐴𝐵 ) ( 𝑥 = 𝑦 ∨ ( 𝐶𝐷 ) = ∅ ) ↔ ( ∀ 𝑦𝐴 ( 𝑥 = 𝑦 ∨ ( 𝐶𝐷 ) = ∅ ) ∧ ∀ 𝑦𝐵 ( 𝑥 = 𝑦 ∨ ( 𝐶𝐷 ) = ∅ ) ) )
14 13 ralbii ( ∀ 𝑥𝐴𝑦 ∈ ( 𝐴𝐵 ) ( 𝑥 = 𝑦 ∨ ( 𝐶𝐷 ) = ∅ ) ↔ ∀ 𝑥𝐴 ( ∀ 𝑦𝐴 ( 𝑥 = 𝑦 ∨ ( 𝐶𝐷 ) = ∅ ) ∧ ∀ 𝑦𝐵 ( 𝑥 = 𝑦 ∨ ( 𝐶𝐷 ) = ∅ ) ) )
15 nfv 𝑧𝑦 ∈ ( 𝐴𝐵 ) ( 𝑥 = 𝑦 ∨ ( 𝐶𝐷 ) = ∅ )
16 nfcv 𝑥 ( 𝐴𝐵 )
17 nfv 𝑥 𝑧 = 𝑤
18 nfcsb1v 𝑥 𝑧 / 𝑥 𝐶
19 nfcsb1v 𝑥 𝑤 / 𝑥 𝐶
20 18 19 nfin 𝑥 ( 𝑧 / 𝑥 𝐶 𝑤 / 𝑥 𝐶 )
21 20 nfeq1 𝑥 ( 𝑧 / 𝑥 𝐶 𝑤 / 𝑥 𝐶 ) = ∅
22 17 21 nfor 𝑥 ( 𝑧 = 𝑤 ∨ ( 𝑧 / 𝑥 𝐶 𝑤 / 𝑥 𝐶 ) = ∅ )
23 16 22 nfralw 𝑥𝑤 ∈ ( 𝐴𝐵 ) ( 𝑧 = 𝑤 ∨ ( 𝑧 / 𝑥 𝐶 𝑤 / 𝑥 𝐶 ) = ∅ )
24 equequ2 ( 𝑤 = 𝑦 → ( 𝑥 = 𝑤𝑥 = 𝑦 ) )
25 nfcv 𝑥 𝑦
26 nfcv 𝑥 𝐷
27 25 26 1 csbhypf ( 𝑤 = 𝑦 𝑤 / 𝑥 𝐶 = 𝐷 )
28 27 ineq2d ( 𝑤 = 𝑦 → ( 𝐶 𝑤 / 𝑥 𝐶 ) = ( 𝐶𝐷 ) )
29 28 eqeq1d ( 𝑤 = 𝑦 → ( ( 𝐶 𝑤 / 𝑥 𝐶 ) = ∅ ↔ ( 𝐶𝐷 ) = ∅ ) )
30 24 29 orbi12d ( 𝑤 = 𝑦 → ( ( 𝑥 = 𝑤 ∨ ( 𝐶 𝑤 / 𝑥 𝐶 ) = ∅ ) ↔ ( 𝑥 = 𝑦 ∨ ( 𝐶𝐷 ) = ∅ ) ) )
31 30 cbvralvw ( ∀ 𝑤 ∈ ( 𝐴𝐵 ) ( 𝑥 = 𝑤 ∨ ( 𝐶 𝑤 / 𝑥 𝐶 ) = ∅ ) ↔ ∀ 𝑦 ∈ ( 𝐴𝐵 ) ( 𝑥 = 𝑦 ∨ ( 𝐶𝐷 ) = ∅ ) )
32 equequ1 ( 𝑥 = 𝑧 → ( 𝑥 = 𝑤𝑧 = 𝑤 ) )
33 csbeq1a ( 𝑥 = 𝑧𝐶 = 𝑧 / 𝑥 𝐶 )
34 33 ineq1d ( 𝑥 = 𝑧 → ( 𝐶 𝑤 / 𝑥 𝐶 ) = ( 𝑧 / 𝑥 𝐶 𝑤 / 𝑥 𝐶 ) )
35 34 eqeq1d ( 𝑥 = 𝑧 → ( ( 𝐶 𝑤 / 𝑥 𝐶 ) = ∅ ↔ ( 𝑧 / 𝑥 𝐶 𝑤 / 𝑥 𝐶 ) = ∅ ) )
36 32 35 orbi12d ( 𝑥 = 𝑧 → ( ( 𝑥 = 𝑤 ∨ ( 𝐶 𝑤 / 𝑥 𝐶 ) = ∅ ) ↔ ( 𝑧 = 𝑤 ∨ ( 𝑧 / 𝑥 𝐶 𝑤 / 𝑥 𝐶 ) = ∅ ) ) )
37 36 ralbidv ( 𝑥 = 𝑧 → ( ∀ 𝑤 ∈ ( 𝐴𝐵 ) ( 𝑥 = 𝑤 ∨ ( 𝐶 𝑤 / 𝑥 𝐶 ) = ∅ ) ↔ ∀ 𝑤 ∈ ( 𝐴𝐵 ) ( 𝑧 = 𝑤 ∨ ( 𝑧 / 𝑥 𝐶 𝑤 / 𝑥 𝐶 ) = ∅ ) ) )
38 31 37 bitr3id ( 𝑥 = 𝑧 → ( ∀ 𝑦 ∈ ( 𝐴𝐵 ) ( 𝑥 = 𝑦 ∨ ( 𝐶𝐷 ) = ∅ ) ↔ ∀ 𝑤 ∈ ( 𝐴𝐵 ) ( 𝑧 = 𝑤 ∨ ( 𝑧 / 𝑥 𝐶 𝑤 / 𝑥 𝐶 ) = ∅ ) ) )
39 15 23 38 cbvralw ( ∀ 𝑥𝐴𝑦 ∈ ( 𝐴𝐵 ) ( 𝑥 = 𝑦 ∨ ( 𝐶𝐷 ) = ∅ ) ↔ ∀ 𝑧𝐴𝑤 ∈ ( 𝐴𝐵 ) ( 𝑧 = 𝑤 ∨ ( 𝑧 / 𝑥 𝐶 𝑤 / 𝑥 𝐶 ) = ∅ ) )
40 r19.26 ( ∀ 𝑥𝐴 ( ∀ 𝑦𝐴 ( 𝑥 = 𝑦 ∨ ( 𝐶𝐷 ) = ∅ ) ∧ ∀ 𝑦𝐵 ( 𝑥 = 𝑦 ∨ ( 𝐶𝐷 ) = ∅ ) ) ↔ ( ∀ 𝑥𝐴𝑦𝐴 ( 𝑥 = 𝑦 ∨ ( 𝐶𝐷 ) = ∅ ) ∧ ∀ 𝑥𝐴𝑦𝐵 ( 𝑥 = 𝑦 ∨ ( 𝐶𝐷 ) = ∅ ) ) )
41 14 39 40 3bitr3i ( ∀ 𝑧𝐴𝑤 ∈ ( 𝐴𝐵 ) ( 𝑧 = 𝑤 ∨ ( 𝑧 / 𝑥 𝐶 𝑤 / 𝑥 𝐶 ) = ∅ ) ↔ ( ∀ 𝑥𝐴𝑦𝐴 ( 𝑥 = 𝑦 ∨ ( 𝐶𝐷 ) = ∅ ) ∧ ∀ 𝑥𝐴𝑦𝐵 ( 𝑥 = 𝑦 ∨ ( 𝐶𝐷 ) = ∅ ) ) )
42 1 disjor ( Disj 𝑥𝐴 𝐶 ↔ ∀ 𝑥𝐴𝑦𝐴 ( 𝑥 = 𝑦 ∨ ( 𝐶𝐷 ) = ∅ ) )
43 42 anbi1i ( ( Disj 𝑥𝐴 𝐶 ∧ ∀ 𝑥𝐴𝑦𝐵 ( 𝐶𝐷 ) = ∅ ) ↔ ( ∀ 𝑥𝐴𝑦𝐴 ( 𝑥 = 𝑦 ∨ ( 𝐶𝐷 ) = ∅ ) ∧ ∀ 𝑥𝐴𝑦𝐵 ( 𝐶𝐷 ) = ∅ ) )
44 12 41 43 3bitr4g ( ( 𝐴𝐵 ) = ∅ → ( ∀ 𝑧𝐴𝑤 ∈ ( 𝐴𝐵 ) ( 𝑧 = 𝑤 ∨ ( 𝑧 / 𝑥 𝐶 𝑤 / 𝑥 𝐶 ) = ∅ ) ↔ ( Disj 𝑥𝐴 𝐶 ∧ ∀ 𝑥𝐴𝑦𝐵 ( 𝐶𝐷 ) = ∅ ) ) )
45 nfv 𝑤 ( 𝑧 = 𝑥 ∨ ( 𝑧 / 𝑥 𝐶𝐶 ) = ∅ )
46 equequ2 ( 𝑥 = 𝑤 → ( 𝑧 = 𝑥𝑧 = 𝑤 ) )
47 csbeq1a ( 𝑥 = 𝑤𝐶 = 𝑤 / 𝑥 𝐶 )
48 47 ineq2d ( 𝑥 = 𝑤 → ( 𝑧 / 𝑥 𝐶𝐶 ) = ( 𝑧 / 𝑥 𝐶 𝑤 / 𝑥 𝐶 ) )
49 48 eqeq1d ( 𝑥 = 𝑤 → ( ( 𝑧 / 𝑥 𝐶𝐶 ) = ∅ ↔ ( 𝑧 / 𝑥 𝐶 𝑤 / 𝑥 𝐶 ) = ∅ ) )
50 46 49 orbi12d ( 𝑥 = 𝑤 → ( ( 𝑧 = 𝑥 ∨ ( 𝑧 / 𝑥 𝐶𝐶 ) = ∅ ) ↔ ( 𝑧 = 𝑤 ∨ ( 𝑧 / 𝑥 𝐶 𝑤 / 𝑥 𝐶 ) = ∅ ) ) )
51 45 22 50 cbvralw ( ∀ 𝑥𝐴 ( 𝑧 = 𝑥 ∨ ( 𝑧 / 𝑥 𝐶𝐶 ) = ∅ ) ↔ ∀ 𝑤𝐴 ( 𝑧 = 𝑤 ∨ ( 𝑧 / 𝑥 𝐶 𝑤 / 𝑥 𝐶 ) = ∅ ) )
52 equequ1 ( 𝑧 = 𝑦 → ( 𝑧 = 𝑥𝑦 = 𝑥 ) )
53 equcom ( 𝑦 = 𝑥𝑥 = 𝑦 )
54 52 53 bitrdi ( 𝑧 = 𝑦 → ( 𝑧 = 𝑥𝑥 = 𝑦 ) )
55 25 26 1 csbhypf ( 𝑧 = 𝑦 𝑧 / 𝑥 𝐶 = 𝐷 )
56 55 ineq1d ( 𝑧 = 𝑦 → ( 𝑧 / 𝑥 𝐶𝐶 ) = ( 𝐷𝐶 ) )
57 incom ( 𝐷𝐶 ) = ( 𝐶𝐷 )
58 56 57 eqtrdi ( 𝑧 = 𝑦 → ( 𝑧 / 𝑥 𝐶𝐶 ) = ( 𝐶𝐷 ) )
59 58 eqeq1d ( 𝑧 = 𝑦 → ( ( 𝑧 / 𝑥 𝐶𝐶 ) = ∅ ↔ ( 𝐶𝐷 ) = ∅ ) )
60 54 59 orbi12d ( 𝑧 = 𝑦 → ( ( 𝑧 = 𝑥 ∨ ( 𝑧 / 𝑥 𝐶𝐶 ) = ∅ ) ↔ ( 𝑥 = 𝑦 ∨ ( 𝐶𝐷 ) = ∅ ) ) )
61 60 ralbidv ( 𝑧 = 𝑦 → ( ∀ 𝑥𝐴 ( 𝑧 = 𝑥 ∨ ( 𝑧 / 𝑥 𝐶𝐶 ) = ∅ ) ↔ ∀ 𝑥𝐴 ( 𝑥 = 𝑦 ∨ ( 𝐶𝐷 ) = ∅ ) ) )
62 51 61 bitr3id ( 𝑧 = 𝑦 → ( ∀ 𝑤𝐴 ( 𝑧 = 𝑤 ∨ ( 𝑧 / 𝑥 𝐶 𝑤 / 𝑥 𝐶 ) = ∅ ) ↔ ∀ 𝑥𝐴 ( 𝑥 = 𝑦 ∨ ( 𝐶𝐷 ) = ∅ ) ) )
63 62 cbvralvw ( ∀ 𝑧𝐵𝑤𝐴 ( 𝑧 = 𝑤 ∨ ( 𝑧 / 𝑥 𝐶 𝑤 / 𝑥 𝐶 ) = ∅ ) ↔ ∀ 𝑦𝐵𝑥𝐴 ( 𝑥 = 𝑦 ∨ ( 𝐶𝐷 ) = ∅ ) )
64 ralcom ( ∀ 𝑦𝐵𝑥𝐴 ( 𝑥 = 𝑦 ∨ ( 𝐶𝐷 ) = ∅ ) ↔ ∀ 𝑥𝐴𝑦𝐵 ( 𝑥 = 𝑦 ∨ ( 𝐶𝐷 ) = ∅ ) )
65 63 64 bitri ( ∀ 𝑧𝐵𝑤𝐴 ( 𝑧 = 𝑤 ∨ ( 𝑧 / 𝑥 𝐶 𝑤 / 𝑥 𝐶 ) = ∅ ) ↔ ∀ 𝑥𝐴𝑦𝐵 ( 𝑥 = 𝑦 ∨ ( 𝐶𝐷 ) = ∅ ) )
66 65 11 syl5bb ( ( 𝐴𝐵 ) = ∅ → ( ∀ 𝑧𝐵𝑤𝐴 ( 𝑧 = 𝑤 ∨ ( 𝑧 / 𝑥 𝐶 𝑤 / 𝑥 𝐶 ) = ∅ ) ↔ ∀ 𝑥𝐴𝑦𝐵 ( 𝐶𝐷 ) = ∅ ) )
67 66 anbi1d ( ( 𝐴𝐵 ) = ∅ → ( ( ∀ 𝑧𝐵𝑤𝐴 ( 𝑧 = 𝑤 ∨ ( 𝑧 / 𝑥 𝐶 𝑤 / 𝑥 𝐶 ) = ∅ ) ∧ ∀ 𝑧𝐵𝑤𝐵 ( 𝑧 = 𝑤 ∨ ( 𝑧 / 𝑥 𝐶 𝑤 / 𝑥 𝐶 ) = ∅ ) ) ↔ ( ∀ 𝑥𝐴𝑦𝐵 ( 𝐶𝐷 ) = ∅ ∧ ∀ 𝑧𝐵𝑤𝐵 ( 𝑧 = 𝑤 ∨ ( 𝑧 / 𝑥 𝐶 𝑤 / 𝑥 𝐶 ) = ∅ ) ) ) )
68 ralunb ( ∀ 𝑤 ∈ ( 𝐴𝐵 ) ( 𝑧 = 𝑤 ∨ ( 𝑧 / 𝑥 𝐶 𝑤 / 𝑥 𝐶 ) = ∅ ) ↔ ( ∀ 𝑤𝐴 ( 𝑧 = 𝑤 ∨ ( 𝑧 / 𝑥 𝐶 𝑤 / 𝑥 𝐶 ) = ∅ ) ∧ ∀ 𝑤𝐵 ( 𝑧 = 𝑤 ∨ ( 𝑧 / 𝑥 𝐶 𝑤 / 𝑥 𝐶 ) = ∅ ) ) )
69 68 ralbii ( ∀ 𝑧𝐵𝑤 ∈ ( 𝐴𝐵 ) ( 𝑧 = 𝑤 ∨ ( 𝑧 / 𝑥 𝐶 𝑤 / 𝑥 𝐶 ) = ∅ ) ↔ ∀ 𝑧𝐵 ( ∀ 𝑤𝐴 ( 𝑧 = 𝑤 ∨ ( 𝑧 / 𝑥 𝐶 𝑤 / 𝑥 𝐶 ) = ∅ ) ∧ ∀ 𝑤𝐵 ( 𝑧 = 𝑤 ∨ ( 𝑧 / 𝑥 𝐶 𝑤 / 𝑥 𝐶 ) = ∅ ) ) )
70 r19.26 ( ∀ 𝑧𝐵 ( ∀ 𝑤𝐴 ( 𝑧 = 𝑤 ∨ ( 𝑧 / 𝑥 𝐶 𝑤 / 𝑥 𝐶 ) = ∅ ) ∧ ∀ 𝑤𝐵 ( 𝑧 = 𝑤 ∨ ( 𝑧 / 𝑥 𝐶 𝑤 / 𝑥 𝐶 ) = ∅ ) ) ↔ ( ∀ 𝑧𝐵𝑤𝐴 ( 𝑧 = 𝑤 ∨ ( 𝑧 / 𝑥 𝐶 𝑤 / 𝑥 𝐶 ) = ∅ ) ∧ ∀ 𝑧𝐵𝑤𝐵 ( 𝑧 = 𝑤 ∨ ( 𝑧 / 𝑥 𝐶 𝑤 / 𝑥 𝐶 ) = ∅ ) ) )
71 69 70 bitri ( ∀ 𝑧𝐵𝑤 ∈ ( 𝐴𝐵 ) ( 𝑧 = 𝑤 ∨ ( 𝑧 / 𝑥 𝐶 𝑤 / 𝑥 𝐶 ) = ∅ ) ↔ ( ∀ 𝑧𝐵𝑤𝐴 ( 𝑧 = 𝑤 ∨ ( 𝑧 / 𝑥 𝐶 𝑤 / 𝑥 𝐶 ) = ∅ ) ∧ ∀ 𝑧𝐵𝑤𝐵 ( 𝑧 = 𝑤 ∨ ( 𝑧 / 𝑥 𝐶 𝑤 / 𝑥 𝐶 ) = ∅ ) ) )
72 disjors ( Disj 𝑥𝐵 𝐶 ↔ ∀ 𝑧𝐵𝑤𝐵 ( 𝑧 = 𝑤 ∨ ( 𝑧 / 𝑥 𝐶 𝑤 / 𝑥 𝐶 ) = ∅ ) )
73 72 anbi2ci ( ( Disj 𝑥𝐵 𝐶 ∧ ∀ 𝑥𝐴𝑦𝐵 ( 𝐶𝐷 ) = ∅ ) ↔ ( ∀ 𝑥𝐴𝑦𝐵 ( 𝐶𝐷 ) = ∅ ∧ ∀ 𝑧𝐵𝑤𝐵 ( 𝑧 = 𝑤 ∨ ( 𝑧 / 𝑥 𝐶 𝑤 / 𝑥 𝐶 ) = ∅ ) ) )
74 67 71 73 3bitr4g ( ( 𝐴𝐵 ) = ∅ → ( ∀ 𝑧𝐵𝑤 ∈ ( 𝐴𝐵 ) ( 𝑧 = 𝑤 ∨ ( 𝑧 / 𝑥 𝐶 𝑤 / 𝑥 𝐶 ) = ∅ ) ↔ ( Disj 𝑥𝐵 𝐶 ∧ ∀ 𝑥𝐴𝑦𝐵 ( 𝐶𝐷 ) = ∅ ) ) )
75 44 74 anbi12d ( ( 𝐴𝐵 ) = ∅ → ( ( ∀ 𝑧𝐴𝑤 ∈ ( 𝐴𝐵 ) ( 𝑧 = 𝑤 ∨ ( 𝑧 / 𝑥 𝐶 𝑤 / 𝑥 𝐶 ) = ∅ ) ∧ ∀ 𝑧𝐵𝑤 ∈ ( 𝐴𝐵 ) ( 𝑧 = 𝑤 ∨ ( 𝑧 / 𝑥 𝐶 𝑤 / 𝑥 𝐶 ) = ∅ ) ) ↔ ( ( Disj 𝑥𝐴 𝐶 ∧ ∀ 𝑥𝐴𝑦𝐵 ( 𝐶𝐷 ) = ∅ ) ∧ ( Disj 𝑥𝐵 𝐶 ∧ ∀ 𝑥𝐴𝑦𝐵 ( 𝐶𝐷 ) = ∅ ) ) ) )
76 disjors ( Disj 𝑥 ∈ ( 𝐴𝐵 ) 𝐶 ↔ ∀ 𝑧 ∈ ( 𝐴𝐵 ) ∀ 𝑤 ∈ ( 𝐴𝐵 ) ( 𝑧 = 𝑤 ∨ ( 𝑧 / 𝑥 𝐶 𝑤 / 𝑥 𝐶 ) = ∅ ) )
77 ralunb ( ∀ 𝑧 ∈ ( 𝐴𝐵 ) ∀ 𝑤 ∈ ( 𝐴𝐵 ) ( 𝑧 = 𝑤 ∨ ( 𝑧 / 𝑥 𝐶 𝑤 / 𝑥 𝐶 ) = ∅ ) ↔ ( ∀ 𝑧𝐴𝑤 ∈ ( 𝐴𝐵 ) ( 𝑧 = 𝑤 ∨ ( 𝑧 / 𝑥 𝐶 𝑤 / 𝑥 𝐶 ) = ∅ ) ∧ ∀ 𝑧𝐵𝑤 ∈ ( 𝐴𝐵 ) ( 𝑧 = 𝑤 ∨ ( 𝑧 / 𝑥 𝐶 𝑤 / 𝑥 𝐶 ) = ∅ ) ) )
78 76 77 bitri ( Disj 𝑥 ∈ ( 𝐴𝐵 ) 𝐶 ↔ ( ∀ 𝑧𝐴𝑤 ∈ ( 𝐴𝐵 ) ( 𝑧 = 𝑤 ∨ ( 𝑧 / 𝑥 𝐶 𝑤 / 𝑥 𝐶 ) = ∅ ) ∧ ∀ 𝑧𝐵𝑤 ∈ ( 𝐴𝐵 ) ( 𝑧 = 𝑤 ∨ ( 𝑧 / 𝑥 𝐶 𝑤 / 𝑥 𝐶 ) = ∅ ) ) )
79 df-3an ( ( Disj 𝑥𝐴 𝐶Disj 𝑥𝐵 𝐶 ∧ ∀ 𝑥𝐴𝑦𝐵 ( 𝐶𝐷 ) = ∅ ) ↔ ( ( Disj 𝑥𝐴 𝐶Disj 𝑥𝐵 𝐶 ) ∧ ∀ 𝑥𝐴𝑦𝐵 ( 𝐶𝐷 ) = ∅ ) )
80 anandir ( ( ( Disj 𝑥𝐴 𝐶Disj 𝑥𝐵 𝐶 ) ∧ ∀ 𝑥𝐴𝑦𝐵 ( 𝐶𝐷 ) = ∅ ) ↔ ( ( Disj 𝑥𝐴 𝐶 ∧ ∀ 𝑥𝐴𝑦𝐵 ( 𝐶𝐷 ) = ∅ ) ∧ ( Disj 𝑥𝐵 𝐶 ∧ ∀ 𝑥𝐴𝑦𝐵 ( 𝐶𝐷 ) = ∅ ) ) )
81 79 80 bitri ( ( Disj 𝑥𝐴 𝐶Disj 𝑥𝐵 𝐶 ∧ ∀ 𝑥𝐴𝑦𝐵 ( 𝐶𝐷 ) = ∅ ) ↔ ( ( Disj 𝑥𝐴 𝐶 ∧ ∀ 𝑥𝐴𝑦𝐵 ( 𝐶𝐷 ) = ∅ ) ∧ ( Disj 𝑥𝐵 𝐶 ∧ ∀ 𝑥𝐴𝑦𝐵 ( 𝐶𝐷 ) = ∅ ) ) )
82 75 78 81 3bitr4g ( ( 𝐴𝐵 ) = ∅ → ( Disj 𝑥 ∈ ( 𝐴𝐵 ) 𝐶 ↔ ( Disj 𝑥𝐴 𝐶Disj 𝑥𝐵 𝐶 ∧ ∀ 𝑥𝐴𝑦𝐵 ( 𝐶𝐷 ) = ∅ ) ) )