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

Theorem disjxun 4758
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 4131 . . . . . . . . . . 11 (((𝐴𝐵) = ∅ ∧ 𝑥𝐴) → ¬ 𝑥𝐵)
2 eleq1 2791 . . . . . . . . . . . 12 (𝑥 = 𝑦 → (𝑥𝐵𝑦𝐵))
32notbid 307 . . . . . . . . . . 11 (𝑥 = 𝑦 → (¬ 𝑥𝐵 ↔ ¬ 𝑦𝐵))
41, 3syl5ibcom 235 . . . . . . . . . 10 (((𝐴𝐵) = ∅ ∧ 𝑥𝐴) → (𝑥 = 𝑦 → ¬ 𝑦𝐵))
54con2d 129 . . . . . . . . 9 (((𝐴𝐵) = ∅ ∧ 𝑥𝐴) → (𝑦𝐵 → ¬ 𝑥 = 𝑦))
65impr 650 . . . . . . . 8 (((𝐴𝐵) = ∅ ∧ (𝑥𝐴𝑦𝐵)) → ¬ 𝑥 = 𝑦)
7 biorf 419 . . . . . . . 8 𝑥 = 𝑦 → ((𝐶𝐷) = ∅ ↔ (𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅)))
86, 7syl 17 . . . . . . 7 (((𝐴𝐵) = ∅ ∧ (𝑥𝐴𝑦𝐵)) → ((𝐶𝐷) = ∅ ↔ (𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅)))
98bicomd 213 . . . . . 6 (((𝐴𝐵) = ∅ ∧ (𝑥𝐴𝑦𝐵)) → ((𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅) ↔ (𝐶𝐷) = ∅))
1092ralbidva 3090 . . . . 5 ((𝐴𝐵) = ∅ → (∀𝑥𝐴𝑦𝐵 (𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅) ↔ ∀𝑥𝐴𝑦𝐵 (𝐶𝐷) = ∅))
1110anbi2d 742 . . . 4 ((𝐴𝐵) = ∅ → ((∀𝑥𝐴𝑦𝐴 (𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅) ∧ ∀𝑥𝐴𝑦𝐵 (𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅)) ↔ (∀𝑥𝐴𝑦𝐴 (𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅) ∧ ∀𝑥𝐴𝑦𝐵 (𝐶𝐷) = ∅)))
12 ralunb 3902 . . . . . 6 (∀𝑦 ∈ (𝐴𝐵)(𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅) ↔ (∀𝑦𝐴 (𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅) ∧ ∀𝑦𝐵 (𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅)))
1312ralbii 3082 . . . . 5 (∀𝑥𝐴𝑦 ∈ (𝐴𝐵)(𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅) ↔ ∀𝑥𝐴 (∀𝑦𝐴 (𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅) ∧ ∀𝑦𝐵 (𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅)))
14 nfv 1956 . . . . . 6 𝑧𝑦 ∈ (𝐴𝐵)(𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅)
15 nfcv 2866 . . . . . . 7 𝑥(𝐴𝐵)
16 nfv 1956 . . . . . . . 8 𝑥 𝑧 = 𝑤
17 nfcsb1v 3655 . . . . . . . . . 10 𝑥𝑧 / 𝑥𝐶
18 nfcsb1v 3655 . . . . . . . . . 10 𝑥𝑤 / 𝑥𝐶
1917, 18nfin 3928 . . . . . . . . 9 𝑥(𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶)
2019nfeq1 2880 . . . . . . . 8 𝑥(𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅
2116, 20nfor 1947 . . . . . . 7 𝑥(𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅)
2215, 21nfral 3047 . . . . . 6 𝑥𝑤 ∈ (𝐴𝐵)(𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅)
23 equequ2 2072 . . . . . . . . 9 (𝑤 = 𝑦 → (𝑥 = 𝑤𝑥 = 𝑦))
24 nfcv 2866 . . . . . . . . . . . 12 𝑥𝑦
25 nfcv 2866 . . . . . . . . . . . 12 𝑥𝐷
26 disjxun.1 . . . . . . . . . . . 12 (𝑥 = 𝑦𝐶 = 𝐷)
2724, 25, 26csbhypf 3658 . . . . . . . . . . 11 (𝑤 = 𝑦𝑤 / 𝑥𝐶 = 𝐷)
2827ineq2d 3922 . . . . . . . . . 10 (𝑤 = 𝑦 → (𝐶𝑤 / 𝑥𝐶) = (𝐶𝐷))
2928eqeq1d 2726 . . . . . . . . 9 (𝑤 = 𝑦 → ((𝐶𝑤 / 𝑥𝐶) = ∅ ↔ (𝐶𝐷) = ∅))
3023, 29orbi12d 748 . . . . . . . 8 (𝑤 = 𝑦 → ((𝑥 = 𝑤 ∨ (𝐶𝑤 / 𝑥𝐶) = ∅) ↔ (𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅)))
3130cbvralv 3274 . . . . . . 7 (∀𝑤 ∈ (𝐴𝐵)(𝑥 = 𝑤 ∨ (𝐶𝑤 / 𝑥𝐶) = ∅) ↔ ∀𝑦 ∈ (𝐴𝐵)(𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅))
32 equequ1 2071 . . . . . . . . 9 (𝑥 = 𝑧 → (𝑥 = 𝑤𝑧 = 𝑤))
33 csbeq1a 3648 . . . . . . . . . . 11 (𝑥 = 𝑧𝐶 = 𝑧 / 𝑥𝐶)
3433ineq1d 3921 . . . . . . . . . 10 (𝑥 = 𝑧 → (𝐶𝑤 / 𝑥𝐶) = (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶))
3534eqeq1d 2726 . . . . . . . . 9 (𝑥 = 𝑧 → ((𝐶𝑤 / 𝑥𝐶) = ∅ ↔ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅))
3632, 35orbi12d 748 . . . . . . . 8 (𝑥 = 𝑧 → ((𝑥 = 𝑤 ∨ (𝐶𝑤 / 𝑥𝐶) = ∅) ↔ (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅)))
3736ralbidv 3088 . . . . . . 7 (𝑥 = 𝑧 → (∀𝑤 ∈ (𝐴𝐵)(𝑥 = 𝑤 ∨ (𝐶𝑤 / 𝑥𝐶) = ∅) ↔ ∀𝑤 ∈ (𝐴𝐵)(𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅)))
3831, 37syl5bbr 274 . . . . . 6 (𝑥 = 𝑧 → (∀𝑦 ∈ (𝐴𝐵)(𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅) ↔ ∀𝑤 ∈ (𝐴𝐵)(𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅)))
3914, 22, 38cbvral 3270 . . . . 5 (∀𝑥𝐴𝑦 ∈ (𝐴𝐵)(𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅) ↔ ∀𝑧𝐴𝑤 ∈ (𝐴𝐵)(𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅))
40 r19.26 3166 . . . . 5 (∀𝑥𝐴 (∀𝑦𝐴 (𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅) ∧ ∀𝑦𝐵 (𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅)) ↔ (∀𝑥𝐴𝑦𝐴 (𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅) ∧ ∀𝑥𝐴𝑦𝐵 (𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅)))
4113, 39, 403bitr3i 290 . . . 4 (∀𝑧𝐴𝑤 ∈ (𝐴𝐵)(𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅) ↔ (∀𝑥𝐴𝑦𝐴 (𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅) ∧ ∀𝑥𝐴𝑦𝐵 (𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅)))
4226disjor 4742 . . . . 5 (Disj 𝑥𝐴 𝐶 ↔ ∀𝑥𝐴𝑦𝐴 (𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅))
4342anbi1i 733 . . . 4 ((Disj 𝑥𝐴 𝐶 ∧ ∀𝑥𝐴𝑦𝐵 (𝐶𝐷) = ∅) ↔ (∀𝑥𝐴𝑦𝐴 (𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅) ∧ ∀𝑥𝐴𝑦𝐵 (𝐶𝐷) = ∅))
4411, 41, 433bitr4g 303 . . 3 ((𝐴𝐵) = ∅ → (∀𝑧𝐴𝑤 ∈ (𝐴𝐵)(𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅) ↔ (Disj 𝑥𝐴 𝐶 ∧ ∀𝑥𝐴𝑦𝐵 (𝐶𝐷) = ∅)))
45 nfv 1956 . . . . . . . . . 10 𝑤(𝑧 = 𝑥 ∨ (𝑧 / 𝑥𝐶𝐶) = ∅)
46 equequ2 2072 . . . . . . . . . . 11 (𝑥 = 𝑤 → (𝑧 = 𝑥𝑧 = 𝑤))
47 csbeq1a 3648 . . . . . . . . . . . . 13 (𝑥 = 𝑤𝐶 = 𝑤 / 𝑥𝐶)
4847ineq2d 3922 . . . . . . . . . . . 12 (𝑥 = 𝑤 → (𝑧 / 𝑥𝐶𝐶) = (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶))
4948eqeq1d 2726 . . . . . . . . . . 11 (𝑥 = 𝑤 → ((𝑧 / 𝑥𝐶𝐶) = ∅ ↔ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅))
5046, 49orbi12d 748 . . . . . . . . . 10 (𝑥 = 𝑤 → ((𝑧 = 𝑥 ∨ (𝑧 / 𝑥𝐶𝐶) = ∅) ↔ (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅)))
5145, 21, 50cbvral 3270 . . . . . . . . 9 (∀𝑥𝐴 (𝑧 = 𝑥 ∨ (𝑧 / 𝑥𝐶𝐶) = ∅) ↔ ∀𝑤𝐴 (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅))
52 equequ1 2071 . . . . . . . . . . . 12 (𝑧 = 𝑦 → (𝑧 = 𝑥𝑦 = 𝑥))
53 equcom 2064 . . . . . . . . . . . 12 (𝑦 = 𝑥𝑥 = 𝑦)
5452, 53syl6bb 276 . . . . . . . . . . 11 (𝑧 = 𝑦 → (𝑧 = 𝑥𝑥 = 𝑦))
5524, 25, 26csbhypf 3658 . . . . . . . . . . . . . 14 (𝑧 = 𝑦𝑧 / 𝑥𝐶 = 𝐷)
5655ineq1d 3921 . . . . . . . . . . . . 13 (𝑧 = 𝑦 → (𝑧 / 𝑥𝐶𝐶) = (𝐷𝐶))
57 incom 3913 . . . . . . . . . . . . 13 (𝐷𝐶) = (𝐶𝐷)
5856, 57syl6eq 2774 . . . . . . . . . . . 12 (𝑧 = 𝑦 → (𝑧 / 𝑥𝐶𝐶) = (𝐶𝐷))
5958eqeq1d 2726 . . . . . . . . . . 11 (𝑧 = 𝑦 → ((𝑧 / 𝑥𝐶𝐶) = ∅ ↔ (𝐶𝐷) = ∅))
6054, 59orbi12d 748 . . . . . . . . . 10 (𝑧 = 𝑦 → ((𝑧 = 𝑥 ∨ (𝑧 / 𝑥𝐶𝐶) = ∅) ↔ (𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅)))
6160ralbidv 3088 . . . . . . . . 9 (𝑧 = 𝑦 → (∀𝑥𝐴 (𝑧 = 𝑥 ∨ (𝑧 / 𝑥𝐶𝐶) = ∅) ↔ ∀𝑥𝐴 (𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅)))
6251, 61syl5bbr 274 . . . . . . . 8 (𝑧 = 𝑦 → (∀𝑤𝐴 (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅) ↔ ∀𝑥𝐴 (𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅)))
6362cbvralv 3274 . . . . . . 7 (∀𝑧𝐵𝑤𝐴 (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅) ↔ ∀𝑦𝐵𝑥𝐴 (𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅))
64 ralcom 3200 . . . . . . 7 (∀𝑦𝐵𝑥𝐴 (𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅) ↔ ∀𝑥𝐴𝑦𝐵 (𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅))
6563, 64bitri 264 . . . . . 6 (∀𝑧𝐵𝑤𝐴 (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅) ↔ ∀𝑥𝐴𝑦𝐵 (𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅))
6665, 10syl5bb 272 . . . . 5 ((𝐴𝐵) = ∅ → (∀𝑧𝐵𝑤𝐴 (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅) ↔ ∀𝑥𝐴𝑦𝐵 (𝐶𝐷) = ∅))
6766anbi1d 743 . . . 4 ((𝐴𝐵) = ∅ → ((∀𝑧𝐵𝑤𝐴 (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅) ∧ ∀𝑧𝐵𝑤𝐵 (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅)) ↔ (∀𝑥𝐴𝑦𝐵 (𝐶𝐷) = ∅ ∧ ∀𝑧𝐵𝑤𝐵 (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅))))
68 ralunb 3902 . . . . . 6 (∀𝑤 ∈ (𝐴𝐵)(𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅) ↔ (∀𝑤𝐴 (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅) ∧ ∀𝑤𝐵 (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅)))
6968ralbii 3082 . . . . 5 (∀𝑧𝐵𝑤 ∈ (𝐴𝐵)(𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅) ↔ ∀𝑧𝐵 (∀𝑤𝐴 (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅) ∧ ∀𝑤𝐵 (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅)))
70 r19.26 3166 . . . . 5 (∀𝑧𝐵 (∀𝑤𝐴 (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅) ∧ ∀𝑤𝐵 (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅)) ↔ (∀𝑧𝐵𝑤𝐴 (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅) ∧ ∀𝑧𝐵𝑤𝐵 (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅)))
7169, 70bitri 264 . . . 4 (∀𝑧𝐵𝑤 ∈ (𝐴𝐵)(𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅) ↔ (∀𝑧𝐵𝑤𝐴 (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅) ∧ ∀𝑧𝐵𝑤𝐵 (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅)))
72 disjors 4743 . . . . 5 (Disj 𝑥𝐵 𝐶 ↔ ∀𝑧𝐵𝑤𝐵 (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅))
7372anbi2ci 734 . . . 4 ((Disj 𝑥𝐵 𝐶 ∧ ∀𝑥𝐴𝑦𝐵 (𝐶𝐷) = ∅) ↔ (∀𝑥𝐴𝑦𝐵 (𝐶𝐷) = ∅ ∧ ∀𝑧𝐵𝑤𝐵 (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅)))
7467, 71, 733bitr4g 303 . . 3 ((𝐴𝐵) = ∅ → (∀𝑧𝐵𝑤 ∈ (𝐴𝐵)(𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅) ↔ (Disj 𝑥𝐵 𝐶 ∧ ∀𝑥𝐴𝑦𝐵 (𝐶𝐷) = ∅)))
7544, 74anbi12d 749 . 2 ((𝐴𝐵) = ∅ → ((∀𝑧𝐴𝑤 ∈ (𝐴𝐵)(𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅) ∧ ∀𝑧𝐵𝑤 ∈ (𝐴𝐵)(𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅)) ↔ ((Disj 𝑥𝐴 𝐶 ∧ ∀𝑥𝐴𝑦𝐵 (𝐶𝐷) = ∅) ∧ (Disj 𝑥𝐵 𝐶 ∧ ∀𝑥𝐴𝑦𝐵 (𝐶𝐷) = ∅))))
76 disjors 4743 . . 3 (Disj 𝑥 ∈ (𝐴𝐵)𝐶 ↔ ∀𝑧 ∈ (𝐴𝐵)∀𝑤 ∈ (𝐴𝐵)(𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅))
77 ralunb 3902 . . 3 (∀𝑧 ∈ (𝐴𝐵)∀𝑤 ∈ (𝐴𝐵)(𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅) ↔ (∀𝑧𝐴𝑤 ∈ (𝐴𝐵)(𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅) ∧ ∀𝑧𝐵𝑤 ∈ (𝐴𝐵)(𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅)))
7876, 77bitri 264 . 2 (Disj 𝑥 ∈ (𝐴𝐵)𝐶 ↔ (∀𝑧𝐴𝑤 ∈ (𝐴𝐵)(𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅) ∧ ∀𝑧𝐵𝑤 ∈ (𝐴𝐵)(𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅)))
79 df-3an 1074 . . 3 ((Disj 𝑥𝐴 𝐶Disj 𝑥𝐵 𝐶 ∧ ∀𝑥𝐴𝑦𝐵 (𝐶𝐷) = ∅) ↔ ((Disj 𝑥𝐴 𝐶Disj 𝑥𝐵 𝐶) ∧ ∀𝑥𝐴𝑦𝐵 (𝐶𝐷) = ∅))
80 anandir 907 . . 3 (((Disj 𝑥𝐴 𝐶Disj 𝑥𝐵 𝐶) ∧ ∀𝑥𝐴𝑦𝐵 (𝐶𝐷) = ∅) ↔ ((Disj 𝑥𝐴 𝐶 ∧ ∀𝑥𝐴𝑦𝐵 (𝐶𝐷) = ∅) ∧ (Disj 𝑥𝐵 𝐶 ∧ ∀𝑥𝐴𝑦𝐵 (𝐶𝐷) = ∅)))
8179, 80bitri 264 . 2 ((Disj 𝑥𝐴 𝐶Disj 𝑥𝐵 𝐶 ∧ ∀𝑥𝐴𝑦𝐵 (𝐶𝐷) = ∅) ↔ ((Disj 𝑥𝐴 𝐶 ∧ ∀𝑥𝐴𝑦𝐵 (𝐶𝐷) = ∅) ∧ (Disj 𝑥𝐵 𝐶 ∧ ∀𝑥𝐴𝑦𝐵 (𝐶𝐷) = ∅)))
8275, 78, 813bitr4g 303 1 ((𝐴𝐵) = ∅ → (Disj 𝑥 ∈ (𝐴𝐵)𝐶 ↔ (Disj 𝑥𝐴 𝐶Disj 𝑥𝐵 𝐶 ∧ ∀𝑥𝐴𝑦𝐵 (𝐶𝐷) = ∅)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wo 382  wa 383  w3a 1072   = wceq 1596  wcel 2103  wral 3014  csb 3639  cun 3678  cin 3679  c0 4023  Disj wdisj 4728
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1835  ax-4 1850  ax-5 1952  ax-6 2018  ax-7 2054  ax-9 2112  ax-10 2132  ax-11 2147  ax-12 2160  ax-13 2355  ax-ext 2704
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1599  df-ex 1818  df-nf 1823  df-sb 2011  df-eu 2575  df-mo 2576  df-clab 2711  df-cleq 2717  df-clel 2720  df-nfc 2855  df-ral 3019  df-rex 3020  df-reu 3021  df-rmo 3022  df-rab 3023  df-v 3306  df-sbc 3542  df-csb 3640  df-dif 3683  df-un 3685  df-in 3687  df-nul 4024  df-disj 4729
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator