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

Theorem disjxun 5055
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 4402 . . . . . . . . . . 11 (((𝐴𝐵) = ∅ ∧ 𝑥𝐴) → ¬ 𝑥𝐵)
2 eleq1w 2892 . . . . . . . . . . . 12 (𝑥 = 𝑦 → (𝑥𝐵𝑦𝐵))
32notbid 319 . . . . . . . . . . 11 (𝑥 = 𝑦 → (¬ 𝑥𝐵 ↔ ¬ 𝑦𝐵))
41, 3syl5ibcom 246 . . . . . . . . . 10 (((𝐴𝐵) = ∅ ∧ 𝑥𝐴) → (𝑥 = 𝑦 → ¬ 𝑦𝐵))
54con2d 136 . . . . . . . . 9 (((𝐴𝐵) = ∅ ∧ 𝑥𝐴) → (𝑦𝐵 → ¬ 𝑥 = 𝑦))
65impr 455 . . . . . . . 8 (((𝐴𝐵) = ∅ ∧ (𝑥𝐴𝑦𝐵)) → ¬ 𝑥 = 𝑦)
7 biorf 930 . . . . . . . 8 𝑥 = 𝑦 → ((𝐶𝐷) = ∅ ↔ (𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅)))
86, 7syl 17 . . . . . . 7 (((𝐴𝐵) = ∅ ∧ (𝑥𝐴𝑦𝐵)) → ((𝐶𝐷) = ∅ ↔ (𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅)))
98bicomd 224 . . . . . 6 (((𝐴𝐵) = ∅ ∧ (𝑥𝐴𝑦𝐵)) → ((𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅) ↔ (𝐶𝐷) = ∅))
1092ralbidva 3195 . . . . 5 ((𝐴𝐵) = ∅ → (∀𝑥𝐴𝑦𝐵 (𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅) ↔ ∀𝑥𝐴𝑦𝐵 (𝐶𝐷) = ∅))
1110anbi2d 628 . . . 4 ((𝐴𝐵) = ∅ → ((∀𝑥𝐴𝑦𝐴 (𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅) ∧ ∀𝑥𝐴𝑦𝐵 (𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅)) ↔ (∀𝑥𝐴𝑦𝐴 (𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅) ∧ ∀𝑥𝐴𝑦𝐵 (𝐶𝐷) = ∅)))
12 ralunb 4164 . . . . . 6 (∀𝑦 ∈ (𝐴𝐵)(𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅) ↔ (∀𝑦𝐴 (𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅) ∧ ∀𝑦𝐵 (𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅)))
1312ralbii 3162 . . . . 5 (∀𝑥𝐴𝑦 ∈ (𝐴𝐵)(𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅) ↔ ∀𝑥𝐴 (∀𝑦𝐴 (𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅) ∧ ∀𝑦𝐵 (𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅)))
14 nfv 1906 . . . . . 6 𝑧𝑦 ∈ (𝐴𝐵)(𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅)
15 nfcv 2974 . . . . . . 7 𝑥(𝐴𝐵)
16 nfv 1906 . . . . . . . 8 𝑥 𝑧 = 𝑤
17 nfcsb1v 3904 . . . . . . . . . 10 𝑥𝑧 / 𝑥𝐶
18 nfcsb1v 3904 . . . . . . . . . 10 𝑥𝑤 / 𝑥𝐶
1917, 18nfin 4190 . . . . . . . . 9 𝑥(𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶)
2019nfeq1 2990 . . . . . . . 8 𝑥(𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅
2116, 20nfor 1896 . . . . . . 7 𝑥(𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅)
2215, 21nfral 3223 . . . . . 6 𝑥𝑤 ∈ (𝐴𝐵)(𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅)
23 equequ2 2024 . . . . . . . . 9 (𝑤 = 𝑦 → (𝑥 = 𝑤𝑥 = 𝑦))
24 nfcv 2974 . . . . . . . . . . . 12 𝑥𝑦
25 nfcv 2974 . . . . . . . . . . . 12 𝑥𝐷
26 disjxun.1 . . . . . . . . . . . 12 (𝑥 = 𝑦𝐶 = 𝐷)
2724, 25, 26csbhypf 3908 . . . . . . . . . . 11 (𝑤 = 𝑦𝑤 / 𝑥𝐶 = 𝐷)
2827ineq2d 4186 . . . . . . . . . 10 (𝑤 = 𝑦 → (𝐶𝑤 / 𝑥𝐶) = (𝐶𝐷))
2928eqeq1d 2820 . . . . . . . . 9 (𝑤 = 𝑦 → ((𝐶𝑤 / 𝑥𝐶) = ∅ ↔ (𝐶𝐷) = ∅))
3023, 29orbi12d 912 . . . . . . . 8 (𝑤 = 𝑦 → ((𝑥 = 𝑤 ∨ (𝐶𝑤 / 𝑥𝐶) = ∅) ↔ (𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅)))
3130cbvralv 3450 . . . . . . 7 (∀𝑤 ∈ (𝐴𝐵)(𝑥 = 𝑤 ∨ (𝐶𝑤 / 𝑥𝐶) = ∅) ↔ ∀𝑦 ∈ (𝐴𝐵)(𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅))
32 equequ1 2023 . . . . . . . . 9 (𝑥 = 𝑧 → (𝑥 = 𝑤𝑧 = 𝑤))
33 csbeq1a 3894 . . . . . . . . . . 11 (𝑥 = 𝑧𝐶 = 𝑧 / 𝑥𝐶)
3433ineq1d 4185 . . . . . . . . . 10 (𝑥 = 𝑧 → (𝐶𝑤 / 𝑥𝐶) = (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶))
3534eqeq1d 2820 . . . . . . . . 9 (𝑥 = 𝑧 → ((𝐶𝑤 / 𝑥𝐶) = ∅ ↔ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅))
3632, 35orbi12d 912 . . . . . . . 8 (𝑥 = 𝑧 → ((𝑥 = 𝑤 ∨ (𝐶𝑤 / 𝑥𝐶) = ∅) ↔ (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅)))
3736ralbidv 3194 . . . . . . 7 (𝑥 = 𝑧 → (∀𝑤 ∈ (𝐴𝐵)(𝑥 = 𝑤 ∨ (𝐶𝑤 / 𝑥𝐶) = ∅) ↔ ∀𝑤 ∈ (𝐴𝐵)(𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅)))
3831, 37syl5bbr 286 . . . . . 6 (𝑥 = 𝑧 → (∀𝑦 ∈ (𝐴𝐵)(𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅) ↔ ∀𝑤 ∈ (𝐴𝐵)(𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅)))
3914, 22, 38cbvral 3443 . . . . 5 (∀𝑥𝐴𝑦 ∈ (𝐴𝐵)(𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅) ↔ ∀𝑧𝐴𝑤 ∈ (𝐴𝐵)(𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅))
40 r19.26 3167 . . . . 5 (∀𝑥𝐴 (∀𝑦𝐴 (𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅) ∧ ∀𝑦𝐵 (𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅)) ↔ (∀𝑥𝐴𝑦𝐴 (𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅) ∧ ∀𝑥𝐴𝑦𝐵 (𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅)))
4113, 39, 403bitr3i 302 . . . 4 (∀𝑧𝐴𝑤 ∈ (𝐴𝐵)(𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅) ↔ (∀𝑥𝐴𝑦𝐴 (𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅) ∧ ∀𝑥𝐴𝑦𝐵 (𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅)))
4226disjor 5037 . . . . 5 (Disj 𝑥𝐴 𝐶 ↔ ∀𝑥𝐴𝑦𝐴 (𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅))
4342anbi1i 623 . . . 4 ((Disj 𝑥𝐴 𝐶 ∧ ∀𝑥𝐴𝑦𝐵 (𝐶𝐷) = ∅) ↔ (∀𝑥𝐴𝑦𝐴 (𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅) ∧ ∀𝑥𝐴𝑦𝐵 (𝐶𝐷) = ∅))
4411, 41, 433bitr4g 315 . . 3 ((𝐴𝐵) = ∅ → (∀𝑧𝐴𝑤 ∈ (𝐴𝐵)(𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅) ↔ (Disj 𝑥𝐴 𝐶 ∧ ∀𝑥𝐴𝑦𝐵 (𝐶𝐷) = ∅)))
45 nfv 1906 . . . . . . . . . 10 𝑤(𝑧 = 𝑥 ∨ (𝑧 / 𝑥𝐶𝐶) = ∅)
46 equequ2 2024 . . . . . . . . . . 11 (𝑥 = 𝑤 → (𝑧 = 𝑥𝑧 = 𝑤))
47 csbeq1a 3894 . . . . . . . . . . . . 13 (𝑥 = 𝑤𝐶 = 𝑤 / 𝑥𝐶)
4847ineq2d 4186 . . . . . . . . . . . 12 (𝑥 = 𝑤 → (𝑧 / 𝑥𝐶𝐶) = (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶))
4948eqeq1d 2820 . . . . . . . . . . 11 (𝑥 = 𝑤 → ((𝑧 / 𝑥𝐶𝐶) = ∅ ↔ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅))
5046, 49orbi12d 912 . . . . . . . . . 10 (𝑥 = 𝑤 → ((𝑧 = 𝑥 ∨ (𝑧 / 𝑥𝐶𝐶) = ∅) ↔ (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅)))
5145, 21, 50cbvral 3443 . . . . . . . . 9 (∀𝑥𝐴 (𝑧 = 𝑥 ∨ (𝑧 / 𝑥𝐶𝐶) = ∅) ↔ ∀𝑤𝐴 (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅))
52 equequ1 2023 . . . . . . . . . . . 12 (𝑧 = 𝑦 → (𝑧 = 𝑥𝑦 = 𝑥))
53 equcom 2016 . . . . . . . . . . . 12 (𝑦 = 𝑥𝑥 = 𝑦)
5452, 53syl6bb 288 . . . . . . . . . . 11 (𝑧 = 𝑦 → (𝑧 = 𝑥𝑥 = 𝑦))
5524, 25, 26csbhypf 3908 . . . . . . . . . . . . . 14 (𝑧 = 𝑦𝑧 / 𝑥𝐶 = 𝐷)
5655ineq1d 4185 . . . . . . . . . . . . 13 (𝑧 = 𝑦 → (𝑧 / 𝑥𝐶𝐶) = (𝐷𝐶))
57 incom 4175 . . . . . . . . . . . . 13 (𝐷𝐶) = (𝐶𝐷)
5856, 57syl6eq 2869 . . . . . . . . . . . 12 (𝑧 = 𝑦 → (𝑧 / 𝑥𝐶𝐶) = (𝐶𝐷))
5958eqeq1d 2820 . . . . . . . . . . 11 (𝑧 = 𝑦 → ((𝑧 / 𝑥𝐶𝐶) = ∅ ↔ (𝐶𝐷) = ∅))
6054, 59orbi12d 912 . . . . . . . . . 10 (𝑧 = 𝑦 → ((𝑧 = 𝑥 ∨ (𝑧 / 𝑥𝐶𝐶) = ∅) ↔ (𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅)))
6160ralbidv 3194 . . . . . . . . 9 (𝑧 = 𝑦 → (∀𝑥𝐴 (𝑧 = 𝑥 ∨ (𝑧 / 𝑥𝐶𝐶) = ∅) ↔ ∀𝑥𝐴 (𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅)))
6251, 61syl5bbr 286 . . . . . . . 8 (𝑧 = 𝑦 → (∀𝑤𝐴 (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅) ↔ ∀𝑥𝐴 (𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅)))
6362cbvralv 3450 . . . . . . 7 (∀𝑧𝐵𝑤𝐴 (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅) ↔ ∀𝑦𝐵𝑥𝐴 (𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅))
64 ralcom 3351 . . . . . . 7 (∀𝑦𝐵𝑥𝐴 (𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅) ↔ ∀𝑥𝐴𝑦𝐵 (𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅))
6563, 64bitri 276 . . . . . 6 (∀𝑧𝐵𝑤𝐴 (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅) ↔ ∀𝑥𝐴𝑦𝐵 (𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅))
6665, 10syl5bb 284 . . . . 5 ((𝐴𝐵) = ∅ → (∀𝑧𝐵𝑤𝐴 (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅) ↔ ∀𝑥𝐴𝑦𝐵 (𝐶𝐷) = ∅))
6766anbi1d 629 . . . 4 ((𝐴𝐵) = ∅ → ((∀𝑧𝐵𝑤𝐴 (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅) ∧ ∀𝑧𝐵𝑤𝐵 (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅)) ↔ (∀𝑥𝐴𝑦𝐵 (𝐶𝐷) = ∅ ∧ ∀𝑧𝐵𝑤𝐵 (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅))))
68 ralunb 4164 . . . . . 6 (∀𝑤 ∈ (𝐴𝐵)(𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅) ↔ (∀𝑤𝐴 (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅) ∧ ∀𝑤𝐵 (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅)))
6968ralbii 3162 . . . . 5 (∀𝑧𝐵𝑤 ∈ (𝐴𝐵)(𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅) ↔ ∀𝑧𝐵 (∀𝑤𝐴 (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅) ∧ ∀𝑤𝐵 (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅)))
70 r19.26 3167 . . . . 5 (∀𝑧𝐵 (∀𝑤𝐴 (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅) ∧ ∀𝑤𝐵 (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅)) ↔ (∀𝑧𝐵𝑤𝐴 (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅) ∧ ∀𝑧𝐵𝑤𝐵 (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅)))
7169, 70bitri 276 . . . 4 (∀𝑧𝐵𝑤 ∈ (𝐴𝐵)(𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅) ↔ (∀𝑧𝐵𝑤𝐴 (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅) ∧ ∀𝑧𝐵𝑤𝐵 (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅)))
72 disjors 5038 . . . . 5 (Disj 𝑥𝐵 𝐶 ↔ ∀𝑧𝐵𝑤𝐵 (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅))
7372anbi2ci 624 . . . 4 ((Disj 𝑥𝐵 𝐶 ∧ ∀𝑥𝐴𝑦𝐵 (𝐶𝐷) = ∅) ↔ (∀𝑥𝐴𝑦𝐵 (𝐶𝐷) = ∅ ∧ ∀𝑧𝐵𝑤𝐵 (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅)))
7467, 71, 733bitr4g 315 . . 3 ((𝐴𝐵) = ∅ → (∀𝑧𝐵𝑤 ∈ (𝐴𝐵)(𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅) ↔ (Disj 𝑥𝐵 𝐶 ∧ ∀𝑥𝐴𝑦𝐵 (𝐶𝐷) = ∅)))
7544, 74anbi12d 630 . 2 ((𝐴𝐵) = ∅ → ((∀𝑧𝐴𝑤 ∈ (𝐴𝐵)(𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅) ∧ ∀𝑧𝐵𝑤 ∈ (𝐴𝐵)(𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅)) ↔ ((Disj 𝑥𝐴 𝐶 ∧ ∀𝑥𝐴𝑦𝐵 (𝐶𝐷) = ∅) ∧ (Disj 𝑥𝐵 𝐶 ∧ ∀𝑥𝐴𝑦𝐵 (𝐶𝐷) = ∅))))
76 disjors 5038 . . 3 (Disj 𝑥 ∈ (𝐴𝐵)𝐶 ↔ ∀𝑧 ∈ (𝐴𝐵)∀𝑤 ∈ (𝐴𝐵)(𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅))
77 ralunb 4164 . . 3 (∀𝑧 ∈ (𝐴𝐵)∀𝑤 ∈ (𝐴𝐵)(𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅) ↔ (∀𝑧𝐴𝑤 ∈ (𝐴𝐵)(𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅) ∧ ∀𝑧𝐵𝑤 ∈ (𝐴𝐵)(𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅)))
7876, 77bitri 276 . 2 (Disj 𝑥 ∈ (𝐴𝐵)𝐶 ↔ (∀𝑧𝐴𝑤 ∈ (𝐴𝐵)(𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅) ∧ ∀𝑧𝐵𝑤 ∈ (𝐴𝐵)(𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅)))
79 df-3an 1081 . . 3 ((Disj 𝑥𝐴 𝐶Disj 𝑥𝐵 𝐶 ∧ ∀𝑥𝐴𝑦𝐵 (𝐶𝐷) = ∅) ↔ ((Disj 𝑥𝐴 𝐶Disj 𝑥𝐵 𝐶) ∧ ∀𝑥𝐴𝑦𝐵 (𝐶𝐷) = ∅))
80 anandir 673 . . 3 (((Disj 𝑥𝐴 𝐶Disj 𝑥𝐵 𝐶) ∧ ∀𝑥𝐴𝑦𝐵 (𝐶𝐷) = ∅) ↔ ((Disj 𝑥𝐴 𝐶 ∧ ∀𝑥𝐴𝑦𝐵 (𝐶𝐷) = ∅) ∧ (Disj 𝑥𝐵 𝐶 ∧ ∀𝑥𝐴𝑦𝐵 (𝐶𝐷) = ∅)))
8179, 80bitri 276 . 2 ((Disj 𝑥𝐴 𝐶Disj 𝑥𝐵 𝐶 ∧ ∀𝑥𝐴𝑦𝐵 (𝐶𝐷) = ∅) ↔ ((Disj 𝑥𝐴 𝐶 ∧ ∀𝑥𝐴𝑦𝐵 (𝐶𝐷) = ∅) ∧ (Disj 𝑥𝐵 𝐶 ∧ ∀𝑥𝐴𝑦𝐵 (𝐶𝐷) = ∅)))
8275, 78, 813bitr4g 315 1 ((𝐴𝐵) = ∅ → (Disj 𝑥 ∈ (𝐴𝐵)𝐶 ↔ (Disj 𝑥𝐴 𝐶Disj 𝑥𝐵 𝐶 ∧ ∀𝑥𝐴𝑦𝐵 (𝐶𝐷) = ∅)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207  wa 396  wo 841  w3a 1079   = wceq 1528  wcel 2105  wral 3135  csb 3880  cun 3931  cin 3932  c0 4288  Disj wdisj 5022
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-13 2381  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ral 3140  df-rex 3141  df-reu 3142  df-rmo 3143  df-rab 3144  df-v 3494  df-sbc 3770  df-csb 3881  df-dif 3936  df-un 3938  df-in 3940  df-nul 4289  df-disj 5023
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator