MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  disjxun Structured version   Visualization version   GIF version

Theorem disjxun 5076
Description: The union of two disjoint collections. (Contributed by Mario Carneiro, 14-Nov-2016.)
Hypothesis
Ref Expression
disjxun.1 (𝑥 = 𝑦𝐶 = 𝐷)
Assertion
Ref Expression
disjxun ((𝐴𝐵) = ∅ → (Disj 𝑥 ∈ (𝐴𝐵)𝐶 ↔ (Disj 𝑥𝐴 𝐶Disj 𝑥𝐵 𝐶 ∧ ∀𝑥𝐴𝑦𝐵 (𝐶𝐷) = ∅)))
Distinct variable groups:   𝑥,𝑦,𝐴   𝑥,𝐵,𝑦   𝑦,𝐶   𝑥,𝐷
Allowed substitution hints:   𝐶(𝑥)   𝐷(𝑦)

Proof of Theorem disjxun
Dummy variables 𝑤 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 disjel 4395 . . . . . . . . . . 11 (((𝐴𝐵) = ∅ ∧ 𝑥𝐴) → ¬ 𝑥𝐵)
2 eleq1w 2822 . . . . . . . . . . . 12 (𝑥 = 𝑦 → (𝑥𝐵𝑦𝐵))
32notbid 317 . . . . . . . . . . 11 (𝑥 = 𝑦 → (¬ 𝑥𝐵 ↔ ¬ 𝑦𝐵))
41, 3syl5ibcom 244 . . . . . . . . . 10 (((𝐴𝐵) = ∅ ∧ 𝑥𝐴) → (𝑥 = 𝑦 → ¬ 𝑦𝐵))
54con2d 134 . . . . . . . . 9 (((𝐴𝐵) = ∅ ∧ 𝑥𝐴) → (𝑦𝐵 → ¬ 𝑥 = 𝑦))
65impr 454 . . . . . . . 8 (((𝐴𝐵) = ∅ ∧ (𝑥𝐴𝑦𝐵)) → ¬ 𝑥 = 𝑦)
7 biorf 933 . . . . . . . 8 𝑥 = 𝑦 → ((𝐶𝐷) = ∅ ↔ (𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅)))
86, 7syl 17 . . . . . . 7 (((𝐴𝐵) = ∅ ∧ (𝑥𝐴𝑦𝐵)) → ((𝐶𝐷) = ∅ ↔ (𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅)))
98bicomd 222 . . . . . 6 (((𝐴𝐵) = ∅ ∧ (𝑥𝐴𝑦𝐵)) → ((𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅) ↔ (𝐶𝐷) = ∅))
1092ralbidva 3123 . . . . 5 ((𝐴𝐵) = ∅ → (∀𝑥𝐴𝑦𝐵 (𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅) ↔ ∀𝑥𝐴𝑦𝐵 (𝐶𝐷) = ∅))
1110anbi2d 628 . . . 4 ((𝐴𝐵) = ∅ → ((∀𝑥𝐴𝑦𝐴 (𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅) ∧ ∀𝑥𝐴𝑦𝐵 (𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅)) ↔ (∀𝑥𝐴𝑦𝐴 (𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅) ∧ ∀𝑥𝐴𝑦𝐵 (𝐶𝐷) = ∅)))
12 ralunb 4129 . . . . . 6 (∀𝑦 ∈ (𝐴𝐵)(𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅) ↔ (∀𝑦𝐴 (𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅) ∧ ∀𝑦𝐵 (𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅)))
1312ralbii 3092 . . . . 5 (∀𝑥𝐴𝑦 ∈ (𝐴𝐵)(𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅) ↔ ∀𝑥𝐴 (∀𝑦𝐴 (𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅) ∧ ∀𝑦𝐵 (𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅)))
14 nfv 1920 . . . . . 6 𝑧𝑦 ∈ (𝐴𝐵)(𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅)
15 nfcv 2908 . . . . . . 7 𝑥(𝐴𝐵)
16 nfv 1920 . . . . . . . 8 𝑥 𝑧 = 𝑤
17 nfcsb1v 3861 . . . . . . . . . 10 𝑥𝑧 / 𝑥𝐶
18 nfcsb1v 3861 . . . . . . . . . 10 𝑥𝑤 / 𝑥𝐶
1917, 18nfin 4155 . . . . . . . . 9 𝑥(𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶)
2019nfeq1 2923 . . . . . . . 8 𝑥(𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅
2116, 20nfor 1910 . . . . . . 7 𝑥(𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅)
2215, 21nfralw 3151 . . . . . 6 𝑥𝑤 ∈ (𝐴𝐵)(𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅)
23 equequ2 2032 . . . . . . . . 9 (𝑤 = 𝑦 → (𝑥 = 𝑤𝑥 = 𝑦))
24 nfcv 2908 . . . . . . . . . . . 12 𝑥𝑦
25 nfcv 2908 . . . . . . . . . . . 12 𝑥𝐷
26 disjxun.1 . . . . . . . . . . . 12 (𝑥 = 𝑦𝐶 = 𝐷)
2724, 25, 26csbhypf 3865 . . . . . . . . . . 11 (𝑤 = 𝑦𝑤 / 𝑥𝐶 = 𝐷)
2827ineq2d 4151 . . . . . . . . . 10 (𝑤 = 𝑦 → (𝐶𝑤 / 𝑥𝐶) = (𝐶𝐷))
2928eqeq1d 2741 . . . . . . . . 9 (𝑤 = 𝑦 → ((𝐶𝑤 / 𝑥𝐶) = ∅ ↔ (𝐶𝐷) = ∅))
3023, 29orbi12d 915 . . . . . . . 8 (𝑤 = 𝑦 → ((𝑥 = 𝑤 ∨ (𝐶𝑤 / 𝑥𝐶) = ∅) ↔ (𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅)))
3130cbvralvw 3380 . . . . . . 7 (∀𝑤 ∈ (𝐴𝐵)(𝑥 = 𝑤 ∨ (𝐶𝑤 / 𝑥𝐶) = ∅) ↔ ∀𝑦 ∈ (𝐴𝐵)(𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅))
32 equequ1 2031 . . . . . . . . 9 (𝑥 = 𝑧 → (𝑥 = 𝑤𝑧 = 𝑤))
33 csbeq1a 3850 . . . . . . . . . . 11 (𝑥 = 𝑧𝐶 = 𝑧 / 𝑥𝐶)
3433ineq1d 4150 . . . . . . . . . 10 (𝑥 = 𝑧 → (𝐶𝑤 / 𝑥𝐶) = (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶))
3534eqeq1d 2741 . . . . . . . . 9 (𝑥 = 𝑧 → ((𝐶𝑤 / 𝑥𝐶) = ∅ ↔ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅))
3632, 35orbi12d 915 . . . . . . . 8 (𝑥 = 𝑧 → ((𝑥 = 𝑤 ∨ (𝐶𝑤 / 𝑥𝐶) = ∅) ↔ (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅)))
3736ralbidv 3122 . . . . . . 7 (𝑥 = 𝑧 → (∀𝑤 ∈ (𝐴𝐵)(𝑥 = 𝑤 ∨ (𝐶𝑤 / 𝑥𝐶) = ∅) ↔ ∀𝑤 ∈ (𝐴𝐵)(𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅)))
3831, 37bitr3id 284 . . . . . 6 (𝑥 = 𝑧 → (∀𝑦 ∈ (𝐴𝐵)(𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅) ↔ ∀𝑤 ∈ (𝐴𝐵)(𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅)))
3914, 22, 38cbvralw 3371 . . . . 5 (∀𝑥𝐴𝑦 ∈ (𝐴𝐵)(𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅) ↔ ∀𝑧𝐴𝑤 ∈ (𝐴𝐵)(𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅))
40 r19.26 3096 . . . . 5 (∀𝑥𝐴 (∀𝑦𝐴 (𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅) ∧ ∀𝑦𝐵 (𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅)) ↔ (∀𝑥𝐴𝑦𝐴 (𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅) ∧ ∀𝑥𝐴𝑦𝐵 (𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅)))
4113, 39, 403bitr3i 300 . . . 4 (∀𝑧𝐴𝑤 ∈ (𝐴𝐵)(𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅) ↔ (∀𝑥𝐴𝑦𝐴 (𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅) ∧ ∀𝑥𝐴𝑦𝐵 (𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅)))
4226disjor 5058 . . . . 5 (Disj 𝑥𝐴 𝐶 ↔ ∀𝑥𝐴𝑦𝐴 (𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅))
4342anbi1i 623 . . . 4 ((Disj 𝑥𝐴 𝐶 ∧ ∀𝑥𝐴𝑦𝐵 (𝐶𝐷) = ∅) ↔ (∀𝑥𝐴𝑦𝐴 (𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅) ∧ ∀𝑥𝐴𝑦𝐵 (𝐶𝐷) = ∅))
4411, 41, 433bitr4g 313 . . 3 ((𝐴𝐵) = ∅ → (∀𝑧𝐴𝑤 ∈ (𝐴𝐵)(𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅) ↔ (Disj 𝑥𝐴 𝐶 ∧ ∀𝑥𝐴𝑦𝐵 (𝐶𝐷) = ∅)))
45 nfv 1920 . . . . . . . . . 10 𝑤(𝑧 = 𝑥 ∨ (𝑧 / 𝑥𝐶𝐶) = ∅)
46 equequ2 2032 . . . . . . . . . . 11 (𝑥 = 𝑤 → (𝑧 = 𝑥𝑧 = 𝑤))
47 csbeq1a 3850 . . . . . . . . . . . . 13 (𝑥 = 𝑤𝐶 = 𝑤 / 𝑥𝐶)
4847ineq2d 4151 . . . . . . . . . . . 12 (𝑥 = 𝑤 → (𝑧 / 𝑥𝐶𝐶) = (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶))
4948eqeq1d 2741 . . . . . . . . . . 11 (𝑥 = 𝑤 → ((𝑧 / 𝑥𝐶𝐶) = ∅ ↔ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅))
5046, 49orbi12d 915 . . . . . . . . . 10 (𝑥 = 𝑤 → ((𝑧 = 𝑥 ∨ (𝑧 / 𝑥𝐶𝐶) = ∅) ↔ (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅)))
5145, 21, 50cbvralw 3371 . . . . . . . . 9 (∀𝑥𝐴 (𝑧 = 𝑥 ∨ (𝑧 / 𝑥𝐶𝐶) = ∅) ↔ ∀𝑤𝐴 (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅))
52 equequ1 2031 . . . . . . . . . . . 12 (𝑧 = 𝑦 → (𝑧 = 𝑥𝑦 = 𝑥))
53 equcom 2024 . . . . . . . . . . . 12 (𝑦 = 𝑥𝑥 = 𝑦)
5452, 53bitrdi 286 . . . . . . . . . . 11 (𝑧 = 𝑦 → (𝑧 = 𝑥𝑥 = 𝑦))
5524, 25, 26csbhypf 3865 . . . . . . . . . . . . . 14 (𝑧 = 𝑦𝑧 / 𝑥𝐶 = 𝐷)
5655ineq1d 4150 . . . . . . . . . . . . 13 (𝑧 = 𝑦 → (𝑧 / 𝑥𝐶𝐶) = (𝐷𝐶))
57 incom 4139 . . . . . . . . . . . . 13 (𝐷𝐶) = (𝐶𝐷)
5856, 57eqtrdi 2795 . . . . . . . . . . . 12 (𝑧 = 𝑦 → (𝑧 / 𝑥𝐶𝐶) = (𝐶𝐷))
5958eqeq1d 2741 . . . . . . . . . . 11 (𝑧 = 𝑦 → ((𝑧 / 𝑥𝐶𝐶) = ∅ ↔ (𝐶𝐷) = ∅))
6054, 59orbi12d 915 . . . . . . . . . 10 (𝑧 = 𝑦 → ((𝑧 = 𝑥 ∨ (𝑧 / 𝑥𝐶𝐶) = ∅) ↔ (𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅)))
6160ralbidv 3122 . . . . . . . . 9 (𝑧 = 𝑦 → (∀𝑥𝐴 (𝑧 = 𝑥 ∨ (𝑧 / 𝑥𝐶𝐶) = ∅) ↔ ∀𝑥𝐴 (𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅)))
6251, 61bitr3id 284 . . . . . . . 8 (𝑧 = 𝑦 → (∀𝑤𝐴 (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅) ↔ ∀𝑥𝐴 (𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅)))
6362cbvralvw 3380 . . . . . . 7 (∀𝑧𝐵𝑤𝐴 (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅) ↔ ∀𝑦𝐵𝑥𝐴 (𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅))
64 ralcom 3282 . . . . . . 7 (∀𝑦𝐵𝑥𝐴 (𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅) ↔ ∀𝑥𝐴𝑦𝐵 (𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅))
6563, 64bitri 274 . . . . . 6 (∀𝑧𝐵𝑤𝐴 (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅) ↔ ∀𝑥𝐴𝑦𝐵 (𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅))
6665, 10syl5bb 282 . . . . 5 ((𝐴𝐵) = ∅ → (∀𝑧𝐵𝑤𝐴 (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅) ↔ ∀𝑥𝐴𝑦𝐵 (𝐶𝐷) = ∅))
6766anbi1d 629 . . . 4 ((𝐴𝐵) = ∅ → ((∀𝑧𝐵𝑤𝐴 (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅) ∧ ∀𝑧𝐵𝑤𝐵 (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅)) ↔ (∀𝑥𝐴𝑦𝐵 (𝐶𝐷) = ∅ ∧ ∀𝑧𝐵𝑤𝐵 (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅))))
68 ralunb 4129 . . . . . 6 (∀𝑤 ∈ (𝐴𝐵)(𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅) ↔ (∀𝑤𝐴 (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅) ∧ ∀𝑤𝐵 (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅)))
6968ralbii 3092 . . . . 5 (∀𝑧𝐵𝑤 ∈ (𝐴𝐵)(𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅) ↔ ∀𝑧𝐵 (∀𝑤𝐴 (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅) ∧ ∀𝑤𝐵 (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅)))
70 r19.26 3096 . . . . 5 (∀𝑧𝐵 (∀𝑤𝐴 (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅) ∧ ∀𝑤𝐵 (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅)) ↔ (∀𝑧𝐵𝑤𝐴 (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅) ∧ ∀𝑧𝐵𝑤𝐵 (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅)))
7169, 70bitri 274 . . . 4 (∀𝑧𝐵𝑤 ∈ (𝐴𝐵)(𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅) ↔ (∀𝑧𝐵𝑤𝐴 (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅) ∧ ∀𝑧𝐵𝑤𝐵 (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅)))
72 disjors 5059 . . . . 5 (Disj 𝑥𝐵 𝐶 ↔ ∀𝑧𝐵𝑤𝐵 (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅))
7372anbi2ci 624 . . . 4 ((Disj 𝑥𝐵 𝐶 ∧ ∀𝑥𝐴𝑦𝐵 (𝐶𝐷) = ∅) ↔ (∀𝑥𝐴𝑦𝐵 (𝐶𝐷) = ∅ ∧ ∀𝑧𝐵𝑤𝐵 (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅)))
7467, 71, 733bitr4g 313 . . 3 ((𝐴𝐵) = ∅ → (∀𝑧𝐵𝑤 ∈ (𝐴𝐵)(𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅) ↔ (Disj 𝑥𝐵 𝐶 ∧ ∀𝑥𝐴𝑦𝐵 (𝐶𝐷) = ∅)))
7544, 74anbi12d 630 . 2 ((𝐴𝐵) = ∅ → ((∀𝑧𝐴𝑤 ∈ (𝐴𝐵)(𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅) ∧ ∀𝑧𝐵𝑤 ∈ (𝐴𝐵)(𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅)) ↔ ((Disj 𝑥𝐴 𝐶 ∧ ∀𝑥𝐴𝑦𝐵 (𝐶𝐷) = ∅) ∧ (Disj 𝑥𝐵 𝐶 ∧ ∀𝑥𝐴𝑦𝐵 (𝐶𝐷) = ∅))))
76 disjors 5059 . . 3 (Disj 𝑥 ∈ (𝐴𝐵)𝐶 ↔ ∀𝑧 ∈ (𝐴𝐵)∀𝑤 ∈ (𝐴𝐵)(𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅))
77 ralunb 4129 . . 3 (∀𝑧 ∈ (𝐴𝐵)∀𝑤 ∈ (𝐴𝐵)(𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅) ↔ (∀𝑧𝐴𝑤 ∈ (𝐴𝐵)(𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅) ∧ ∀𝑧𝐵𝑤 ∈ (𝐴𝐵)(𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅)))
7876, 77bitri 274 . 2 (Disj 𝑥 ∈ (𝐴𝐵)𝐶 ↔ (∀𝑧𝐴𝑤 ∈ (𝐴𝐵)(𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅) ∧ ∀𝑧𝐵𝑤 ∈ (𝐴𝐵)(𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅)))
79 df-3an 1087 . . 3 ((Disj 𝑥𝐴 𝐶Disj 𝑥𝐵 𝐶 ∧ ∀𝑥𝐴𝑦𝐵 (𝐶𝐷) = ∅) ↔ ((Disj 𝑥𝐴 𝐶Disj 𝑥𝐵 𝐶) ∧ ∀𝑥𝐴𝑦𝐵 (𝐶𝐷) = ∅))
80 anandir 673 . . 3 (((Disj 𝑥𝐴 𝐶Disj 𝑥𝐵 𝐶) ∧ ∀𝑥𝐴𝑦𝐵 (𝐶𝐷) = ∅) ↔ ((Disj 𝑥𝐴 𝐶 ∧ ∀𝑥𝐴𝑦𝐵 (𝐶𝐷) = ∅) ∧ (Disj 𝑥𝐵 𝐶 ∧ ∀𝑥𝐴𝑦𝐵 (𝐶𝐷) = ∅)))
8179, 80bitri 274 . 2 ((Disj 𝑥𝐴 𝐶Disj 𝑥𝐵 𝐶 ∧ ∀𝑥𝐴𝑦𝐵 (𝐶𝐷) = ∅) ↔ ((Disj 𝑥𝐴 𝐶 ∧ ∀𝑥𝐴𝑦𝐵 (𝐶𝐷) = ∅) ∧ (Disj 𝑥𝐵 𝐶 ∧ ∀𝑥𝐴𝑦𝐵 (𝐶𝐷) = ∅)))
8275, 78, 813bitr4g 313 1 ((𝐴𝐵) = ∅ → (Disj 𝑥 ∈ (𝐴𝐵)𝐶 ↔ (Disj 𝑥𝐴 𝐶Disj 𝑥𝐵 𝐶 ∧ ∀𝑥𝐴𝑦𝐵 (𝐶𝐷) = ∅)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 395  wo 843  w3a 1085   = wceq 1541  wcel 2109  wral 3065  csb 3836  cun 3889  cin 3890  c0 4261  Disj wdisj 5043
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-10 2140  ax-11 2157  ax-12 2174  ax-ext 2710
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1544  df-fal 1554  df-ex 1786  df-nf 1790  df-sb 2071  df-mo 2541  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ral 3070  df-rmo 3073  df-rab 3074  df-v 3432  df-sbc 3720  df-csb 3837  df-dif 3894  df-un 3896  df-in 3898  df-nul 4262  df-disj 5044
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator