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

Theorem disjxun 5040
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 4378 . . . . . . . . . . 11 (((𝐴𝐵) = ∅ ∧ 𝑥𝐴) → ¬ 𝑥𝐵)
2 eleq1w 2896 . . . . . . . . . . . 12 (𝑥 = 𝑦 → (𝑥𝐵𝑦𝐵))
32notbid 321 . . . . . . . . . . 11 (𝑥 = 𝑦 → (¬ 𝑥𝐵 ↔ ¬ 𝑦𝐵))
41, 3syl5ibcom 248 . . . . . . . . . 10 (((𝐴𝐵) = ∅ ∧ 𝑥𝐴) → (𝑥 = 𝑦 → ¬ 𝑦𝐵))
54con2d 136 . . . . . . . . 9 (((𝐴𝐵) = ∅ ∧ 𝑥𝐴) → (𝑦𝐵 → ¬ 𝑥 = 𝑦))
65impr 458 . . . . . . . 8 (((𝐴𝐵) = ∅ ∧ (𝑥𝐴𝑦𝐵)) → ¬ 𝑥 = 𝑦)
7 biorf 934 . . . . . . . 8 𝑥 = 𝑦 → ((𝐶𝐷) = ∅ ↔ (𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅)))
86, 7syl 17 . . . . . . 7 (((𝐴𝐵) = ∅ ∧ (𝑥𝐴𝑦𝐵)) → ((𝐶𝐷) = ∅ ↔ (𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅)))
98bicomd 226 . . . . . 6 (((𝐴𝐵) = ∅ ∧ (𝑥𝐴𝑦𝐵)) → ((𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅) ↔ (𝐶𝐷) = ∅))
1092ralbidva 3188 . . . . 5 ((𝐴𝐵) = ∅ → (∀𝑥𝐴𝑦𝐵 (𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅) ↔ ∀𝑥𝐴𝑦𝐵 (𝐶𝐷) = ∅))
1110anbi2d 631 . . . 4 ((𝐴𝐵) = ∅ → ((∀𝑥𝐴𝑦𝐴 (𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅) ∧ ∀𝑥𝐴𝑦𝐵 (𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅)) ↔ (∀𝑥𝐴𝑦𝐴 (𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅) ∧ ∀𝑥𝐴𝑦𝐵 (𝐶𝐷) = ∅)))
12 ralunb 4142 . . . . . 6 (∀𝑦 ∈ (𝐴𝐵)(𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅) ↔ (∀𝑦𝐴 (𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅) ∧ ∀𝑦𝐵 (𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅)))
1312ralbii 3157 . . . . 5 (∀𝑥𝐴𝑦 ∈ (𝐴𝐵)(𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅) ↔ ∀𝑥𝐴 (∀𝑦𝐴 (𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅) ∧ ∀𝑦𝐵 (𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅)))
14 nfv 1915 . . . . . 6 𝑧𝑦 ∈ (𝐴𝐵)(𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅)
15 nfcv 2979 . . . . . . 7 𝑥(𝐴𝐵)
16 nfv 1915 . . . . . . . 8 𝑥 𝑧 = 𝑤
17 nfcsb1v 3879 . . . . . . . . . 10 𝑥𝑧 / 𝑥𝐶
18 nfcsb1v 3879 . . . . . . . . . 10 𝑥𝑤 / 𝑥𝐶
1917, 18nfin 4167 . . . . . . . . 9 𝑥(𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶)
2019nfeq1 2994 . . . . . . . 8 𝑥(𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅
2116, 20nfor 1905 . . . . . . 7 𝑥(𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅)
2215, 21nfralw 3214 . . . . . 6 𝑥𝑤 ∈ (𝐴𝐵)(𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅)
23 equequ2 2033 . . . . . . . . 9 (𝑤 = 𝑦 → (𝑥 = 𝑤𝑥 = 𝑦))
24 nfcv 2979 . . . . . . . . . . . 12 𝑥𝑦
25 nfcv 2979 . . . . . . . . . . . 12 𝑥𝐷
26 disjxun.1 . . . . . . . . . . . 12 (𝑥 = 𝑦𝐶 = 𝐷)
2724, 25, 26csbhypf 3883 . . . . . . . . . . 11 (𝑤 = 𝑦𝑤 / 𝑥𝐶 = 𝐷)
2827ineq2d 4163 . . . . . . . . . 10 (𝑤 = 𝑦 → (𝐶𝑤 / 𝑥𝐶) = (𝐶𝐷))
2928eqeq1d 2824 . . . . . . . . 9 (𝑤 = 𝑦 → ((𝐶𝑤 / 𝑥𝐶) = ∅ ↔ (𝐶𝐷) = ∅))
3023, 29orbi12d 916 . . . . . . . 8 (𝑤 = 𝑦 → ((𝑥 = 𝑤 ∨ (𝐶𝑤 / 𝑥𝐶) = ∅) ↔ (𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅)))
3130cbvralvw 3424 . . . . . . 7 (∀𝑤 ∈ (𝐴𝐵)(𝑥 = 𝑤 ∨ (𝐶𝑤 / 𝑥𝐶) = ∅) ↔ ∀𝑦 ∈ (𝐴𝐵)(𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅))
32 equequ1 2032 . . . . . . . . 9 (𝑥 = 𝑧 → (𝑥 = 𝑤𝑧 = 𝑤))
33 csbeq1a 3869 . . . . . . . . . . 11 (𝑥 = 𝑧𝐶 = 𝑧 / 𝑥𝐶)
3433ineq1d 4162 . . . . . . . . . 10 (𝑥 = 𝑧 → (𝐶𝑤 / 𝑥𝐶) = (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶))
3534eqeq1d 2824 . . . . . . . . 9 (𝑥 = 𝑧 → ((𝐶𝑤 / 𝑥𝐶) = ∅ ↔ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅))
3632, 35orbi12d 916 . . . . . . . 8 (𝑥 = 𝑧 → ((𝑥 = 𝑤 ∨ (𝐶𝑤 / 𝑥𝐶) = ∅) ↔ (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅)))
3736ralbidv 3187 . . . . . . 7 (𝑥 = 𝑧 → (∀𝑤 ∈ (𝐴𝐵)(𝑥 = 𝑤 ∨ (𝐶𝑤 / 𝑥𝐶) = ∅) ↔ ∀𝑤 ∈ (𝐴𝐵)(𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅)))
3831, 37bitr3id 288 . . . . . 6 (𝑥 = 𝑧 → (∀𝑦 ∈ (𝐴𝐵)(𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅) ↔ ∀𝑤 ∈ (𝐴𝐵)(𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅)))
3914, 22, 38cbvralw 3415 . . . . 5 (∀𝑥𝐴𝑦 ∈ (𝐴𝐵)(𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅) ↔ ∀𝑧𝐴𝑤 ∈ (𝐴𝐵)(𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅))
40 r19.26 3162 . . . . 5 (∀𝑥𝐴 (∀𝑦𝐴 (𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅) ∧ ∀𝑦𝐵 (𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅)) ↔ (∀𝑥𝐴𝑦𝐴 (𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅) ∧ ∀𝑥𝐴𝑦𝐵 (𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅)))
4113, 39, 403bitr3i 304 . . . 4 (∀𝑧𝐴𝑤 ∈ (𝐴𝐵)(𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅) ↔ (∀𝑥𝐴𝑦𝐴 (𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅) ∧ ∀𝑥𝐴𝑦𝐵 (𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅)))
4226disjor 5022 . . . . 5 (Disj 𝑥𝐴 𝐶 ↔ ∀𝑥𝐴𝑦𝐴 (𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅))
4342anbi1i 626 . . . 4 ((Disj 𝑥𝐴 𝐶 ∧ ∀𝑥𝐴𝑦𝐵 (𝐶𝐷) = ∅) ↔ (∀𝑥𝐴𝑦𝐴 (𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅) ∧ ∀𝑥𝐴𝑦𝐵 (𝐶𝐷) = ∅))
4411, 41, 433bitr4g 317 . . 3 ((𝐴𝐵) = ∅ → (∀𝑧𝐴𝑤 ∈ (𝐴𝐵)(𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅) ↔ (Disj 𝑥𝐴 𝐶 ∧ ∀𝑥𝐴𝑦𝐵 (𝐶𝐷) = ∅)))
45 nfv 1915 . . . . . . . . . 10 𝑤(𝑧 = 𝑥 ∨ (𝑧 / 𝑥𝐶𝐶) = ∅)
46 equequ2 2033 . . . . . . . . . . 11 (𝑥 = 𝑤 → (𝑧 = 𝑥𝑧 = 𝑤))
47 csbeq1a 3869 . . . . . . . . . . . . 13 (𝑥 = 𝑤𝐶 = 𝑤 / 𝑥𝐶)
4847ineq2d 4163 . . . . . . . . . . . 12 (𝑥 = 𝑤 → (𝑧 / 𝑥𝐶𝐶) = (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶))
4948eqeq1d 2824 . . . . . . . . . . 11 (𝑥 = 𝑤 → ((𝑧 / 𝑥𝐶𝐶) = ∅ ↔ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅))
5046, 49orbi12d 916 . . . . . . . . . 10 (𝑥 = 𝑤 → ((𝑧 = 𝑥 ∨ (𝑧 / 𝑥𝐶𝐶) = ∅) ↔ (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅)))
5145, 21, 50cbvralw 3415 . . . . . . . . 9 (∀𝑥𝐴 (𝑧 = 𝑥 ∨ (𝑧 / 𝑥𝐶𝐶) = ∅) ↔ ∀𝑤𝐴 (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅))
52 equequ1 2032 . . . . . . . . . . . 12 (𝑧 = 𝑦 → (𝑧 = 𝑥𝑦 = 𝑥))
53 equcom 2025 . . . . . . . . . . . 12 (𝑦 = 𝑥𝑥 = 𝑦)
5452, 53syl6bb 290 . . . . . . . . . . 11 (𝑧 = 𝑦 → (𝑧 = 𝑥𝑥 = 𝑦))
5524, 25, 26csbhypf 3883 . . . . . . . . . . . . . 14 (𝑧 = 𝑦𝑧 / 𝑥𝐶 = 𝐷)
5655ineq1d 4162 . . . . . . . . . . . . 13 (𝑧 = 𝑦 → (𝑧 / 𝑥𝐶𝐶) = (𝐷𝐶))
57 incom 4152 . . . . . . . . . . . . 13 (𝐷𝐶) = (𝐶𝐷)
5856, 57syl6eq 2873 . . . . . . . . . . . 12 (𝑧 = 𝑦 → (𝑧 / 𝑥𝐶𝐶) = (𝐶𝐷))
5958eqeq1d 2824 . . . . . . . . . . 11 (𝑧 = 𝑦 → ((𝑧 / 𝑥𝐶𝐶) = ∅ ↔ (𝐶𝐷) = ∅))
6054, 59orbi12d 916 . . . . . . . . . 10 (𝑧 = 𝑦 → ((𝑧 = 𝑥 ∨ (𝑧 / 𝑥𝐶𝐶) = ∅) ↔ (𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅)))
6160ralbidv 3187 . . . . . . . . 9 (𝑧 = 𝑦 → (∀𝑥𝐴 (𝑧 = 𝑥 ∨ (𝑧 / 𝑥𝐶𝐶) = ∅) ↔ ∀𝑥𝐴 (𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅)))
6251, 61bitr3id 288 . . . . . . . 8 (𝑧 = 𝑦 → (∀𝑤𝐴 (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅) ↔ ∀𝑥𝐴 (𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅)))
6362cbvralvw 3424 . . . . . . 7 (∀𝑧𝐵𝑤𝐴 (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅) ↔ ∀𝑦𝐵𝑥𝐴 (𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅))
64 ralcom 3335 . . . . . . 7 (∀𝑦𝐵𝑥𝐴 (𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅) ↔ ∀𝑥𝐴𝑦𝐵 (𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅))
6563, 64bitri 278 . . . . . 6 (∀𝑧𝐵𝑤𝐴 (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅) ↔ ∀𝑥𝐴𝑦𝐵 (𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅))
6665, 10syl5bb 286 . . . . 5 ((𝐴𝐵) = ∅ → (∀𝑧𝐵𝑤𝐴 (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅) ↔ ∀𝑥𝐴𝑦𝐵 (𝐶𝐷) = ∅))
6766anbi1d 632 . . . 4 ((𝐴𝐵) = ∅ → ((∀𝑧𝐵𝑤𝐴 (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅) ∧ ∀𝑧𝐵𝑤𝐵 (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅)) ↔ (∀𝑥𝐴𝑦𝐵 (𝐶𝐷) = ∅ ∧ ∀𝑧𝐵𝑤𝐵 (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅))))
68 ralunb 4142 . . . . . 6 (∀𝑤 ∈ (𝐴𝐵)(𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅) ↔ (∀𝑤𝐴 (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅) ∧ ∀𝑤𝐵 (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅)))
6968ralbii 3157 . . . . 5 (∀𝑧𝐵𝑤 ∈ (𝐴𝐵)(𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅) ↔ ∀𝑧𝐵 (∀𝑤𝐴 (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅) ∧ ∀𝑤𝐵 (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅)))
70 r19.26 3162 . . . . 5 (∀𝑧𝐵 (∀𝑤𝐴 (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅) ∧ ∀𝑤𝐵 (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅)) ↔ (∀𝑧𝐵𝑤𝐴 (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅) ∧ ∀𝑧𝐵𝑤𝐵 (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅)))
7169, 70bitri 278 . . . 4 (∀𝑧𝐵𝑤 ∈ (𝐴𝐵)(𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅) ↔ (∀𝑧𝐵𝑤𝐴 (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅) ∧ ∀𝑧𝐵𝑤𝐵 (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅)))
72 disjors 5023 . . . . 5 (Disj 𝑥𝐵 𝐶 ↔ ∀𝑧𝐵𝑤𝐵 (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅))
7372anbi2ci 627 . . . 4 ((Disj 𝑥𝐵 𝐶 ∧ ∀𝑥𝐴𝑦𝐵 (𝐶𝐷) = ∅) ↔ (∀𝑥𝐴𝑦𝐵 (𝐶𝐷) = ∅ ∧ ∀𝑧𝐵𝑤𝐵 (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅)))
7467, 71, 733bitr4g 317 . . 3 ((𝐴𝐵) = ∅ → (∀𝑧𝐵𝑤 ∈ (𝐴𝐵)(𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅) ↔ (Disj 𝑥𝐵 𝐶 ∧ ∀𝑥𝐴𝑦𝐵 (𝐶𝐷) = ∅)))
7544, 74anbi12d 633 . 2 ((𝐴𝐵) = ∅ → ((∀𝑧𝐴𝑤 ∈ (𝐴𝐵)(𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅) ∧ ∀𝑧𝐵𝑤 ∈ (𝐴𝐵)(𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅)) ↔ ((Disj 𝑥𝐴 𝐶 ∧ ∀𝑥𝐴𝑦𝐵 (𝐶𝐷) = ∅) ∧ (Disj 𝑥𝐵 𝐶 ∧ ∀𝑥𝐴𝑦𝐵 (𝐶𝐷) = ∅))))
76 disjors 5023 . . 3 (Disj 𝑥 ∈ (𝐴𝐵)𝐶 ↔ ∀𝑧 ∈ (𝐴𝐵)∀𝑤 ∈ (𝐴𝐵)(𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅))
77 ralunb 4142 . . 3 (∀𝑧 ∈ (𝐴𝐵)∀𝑤 ∈ (𝐴𝐵)(𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅) ↔ (∀𝑧𝐴𝑤 ∈ (𝐴𝐵)(𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅) ∧ ∀𝑧𝐵𝑤 ∈ (𝐴𝐵)(𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅)))
7876, 77bitri 278 . 2 (Disj 𝑥 ∈ (𝐴𝐵)𝐶 ↔ (∀𝑧𝐴𝑤 ∈ (𝐴𝐵)(𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅) ∧ ∀𝑧𝐵𝑤 ∈ (𝐴𝐵)(𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅)))
79 df-3an 1086 . . 3 ((Disj 𝑥𝐴 𝐶Disj 𝑥𝐵 𝐶 ∧ ∀𝑥𝐴𝑦𝐵 (𝐶𝐷) = ∅) ↔ ((Disj 𝑥𝐴 𝐶Disj 𝑥𝐵 𝐶) ∧ ∀𝑥𝐴𝑦𝐵 (𝐶𝐷) = ∅))
80 anandir 676 . . 3 (((Disj 𝑥𝐴 𝐶Disj 𝑥𝐵 𝐶) ∧ ∀𝑥𝐴𝑦𝐵 (𝐶𝐷) = ∅) ↔ ((Disj 𝑥𝐴 𝐶 ∧ ∀𝑥𝐴𝑦𝐵 (𝐶𝐷) = ∅) ∧ (Disj 𝑥𝐵 𝐶 ∧ ∀𝑥𝐴𝑦𝐵 (𝐶𝐷) = ∅)))
8179, 80bitri 278 . 2 ((Disj 𝑥𝐴 𝐶Disj 𝑥𝐵 𝐶 ∧ ∀𝑥𝐴𝑦𝐵 (𝐶𝐷) = ∅) ↔ ((Disj 𝑥𝐴 𝐶 ∧ ∀𝑥𝐴𝑦𝐵 (𝐶𝐷) = ∅) ∧ (Disj 𝑥𝐵 𝐶 ∧ ∀𝑥𝐴𝑦𝐵 (𝐶𝐷) = ∅)))
8275, 78, 813bitr4g 317 1 ((𝐴𝐵) = ∅ → (Disj 𝑥 ∈ (𝐴𝐵)𝐶 ↔ (Disj 𝑥𝐴 𝐶Disj 𝑥𝐵 𝐶 ∧ ∀𝑥𝐴𝑦𝐵 (𝐶𝐷) = ∅)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209  wa 399  wo 844  w3a 1084   = wceq 1538  wcel 2114  wral 3130  csb 3855  cun 3906  cin 3907  c0 4265  Disj wdisj 5007
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2178  ax-ext 2794
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2622  df-clab 2801  df-cleq 2815  df-clel 2894  df-nfc 2962  df-ral 3135  df-rmo 3138  df-rab 3139  df-v 3471  df-sbc 3748  df-csb 3856  df-dif 3911  df-un 3913  df-in 3915  df-nul 4266  df-disj 5008
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator