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

Theorem disjxun 4683
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 4056 . . . . . . . . . . 11 (((𝐴𝐵) = ∅ ∧ 𝑥𝐴) → ¬ 𝑥𝐵)
2 eleq1 2718 . . . . . . . . . . . 12 (𝑥 = 𝑦 → (𝑥𝐵𝑦𝐵))
32notbid 307 . . . . . . . . . . 11 (𝑥 = 𝑦 → (¬ 𝑥𝐵 ↔ ¬ 𝑦𝐵))
41, 3syl5ibcom 235 . . . . . . . . . 10 (((𝐴𝐵) = ∅ ∧ 𝑥𝐴) → (𝑥 = 𝑦 → ¬ 𝑦𝐵))
54con2d 129 . . . . . . . . 9 (((𝐴𝐵) = ∅ ∧ 𝑥𝐴) → (𝑦𝐵 → ¬ 𝑥 = 𝑦))
65impr 648 . . . . . . . 8 (((𝐴𝐵) = ∅ ∧ (𝑥𝐴𝑦𝐵)) → ¬ 𝑥 = 𝑦)
7 biorf 419 . . . . . . . 8 𝑥 = 𝑦 → ((𝐶𝐷) = ∅ ↔ (𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅)))
86, 7syl 17 . . . . . . 7 (((𝐴𝐵) = ∅ ∧ (𝑥𝐴𝑦𝐵)) → ((𝐶𝐷) = ∅ ↔ (𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅)))
98bicomd 213 . . . . . 6 (((𝐴𝐵) = ∅ ∧ (𝑥𝐴𝑦𝐵)) → ((𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅) ↔ (𝐶𝐷) = ∅))
1092ralbidva 3017 . . . . 5 ((𝐴𝐵) = ∅ → (∀𝑥𝐴𝑦𝐵 (𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅) ↔ ∀𝑥𝐴𝑦𝐵 (𝐶𝐷) = ∅))
1110anbi2d 740 . . . 4 ((𝐴𝐵) = ∅ → ((∀𝑥𝐴𝑦𝐴 (𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅) ∧ ∀𝑥𝐴𝑦𝐵 (𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅)) ↔ (∀𝑥𝐴𝑦𝐴 (𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅) ∧ ∀𝑥𝐴𝑦𝐵 (𝐶𝐷) = ∅)))
12 ralunb 3827 . . . . . 6 (∀𝑦 ∈ (𝐴𝐵)(𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅) ↔ (∀𝑦𝐴 (𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅) ∧ ∀𝑦𝐵 (𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅)))
1312ralbii 3009 . . . . 5 (∀𝑥𝐴𝑦 ∈ (𝐴𝐵)(𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅) ↔ ∀𝑥𝐴 (∀𝑦𝐴 (𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅) ∧ ∀𝑦𝐵 (𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅)))
14 nfv 1883 . . . . . 6 𝑧𝑦 ∈ (𝐴𝐵)(𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅)
15 nfcv 2793 . . . . . . 7 𝑥(𝐴𝐵)
16 nfv 1883 . . . . . . . 8 𝑥 𝑧 = 𝑤
17 nfcsb1v 3582 . . . . . . . . . 10 𝑥𝑧 / 𝑥𝐶
18 nfcsb1v 3582 . . . . . . . . . 10 𝑥𝑤 / 𝑥𝐶
1917, 18nfin 3853 . . . . . . . . 9 𝑥(𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶)
2019nfeq1 2807 . . . . . . . 8 𝑥(𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅
2116, 20nfor 1874 . . . . . . 7 𝑥(𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅)
2215, 21nfral 2974 . . . . . 6 𝑥𝑤 ∈ (𝐴𝐵)(𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅)
23 equequ2 1999 . . . . . . . . 9 (𝑤 = 𝑦 → (𝑥 = 𝑤𝑥 = 𝑦))
24 nfcv 2793 . . . . . . . . . . . 12 𝑥𝑦
25 nfcv 2793 . . . . . . . . . . . 12 𝑥𝐷
26 disjxun.1 . . . . . . . . . . . 12 (𝑥 = 𝑦𝐶 = 𝐷)
2724, 25, 26csbhypf 3585 . . . . . . . . . . 11 (𝑤 = 𝑦𝑤 / 𝑥𝐶 = 𝐷)
2827ineq2d 3847 . . . . . . . . . 10 (𝑤 = 𝑦 → (𝐶𝑤 / 𝑥𝐶) = (𝐶𝐷))
2928eqeq1d 2653 . . . . . . . . 9 (𝑤 = 𝑦 → ((𝐶𝑤 / 𝑥𝐶) = ∅ ↔ (𝐶𝐷) = ∅))
3023, 29orbi12d 746 . . . . . . . 8 (𝑤 = 𝑦 → ((𝑥 = 𝑤 ∨ (𝐶𝑤 / 𝑥𝐶) = ∅) ↔ (𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅)))
3130cbvralv 3201 . . . . . . 7 (∀𝑤 ∈ (𝐴𝐵)(𝑥 = 𝑤 ∨ (𝐶𝑤 / 𝑥𝐶) = ∅) ↔ ∀𝑦 ∈ (𝐴𝐵)(𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅))
32 equequ1 1998 . . . . . . . . 9 (𝑥 = 𝑧 → (𝑥 = 𝑤𝑧 = 𝑤))
33 csbeq1a 3575 . . . . . . . . . . 11 (𝑥 = 𝑧𝐶 = 𝑧 / 𝑥𝐶)
3433ineq1d 3846 . . . . . . . . . 10 (𝑥 = 𝑧 → (𝐶𝑤 / 𝑥𝐶) = (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶))
3534eqeq1d 2653 . . . . . . . . 9 (𝑥 = 𝑧 → ((𝐶𝑤 / 𝑥𝐶) = ∅ ↔ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅))
3632, 35orbi12d 746 . . . . . . . 8 (𝑥 = 𝑧 → ((𝑥 = 𝑤 ∨ (𝐶𝑤 / 𝑥𝐶) = ∅) ↔ (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅)))
3736ralbidv 3015 . . . . . . 7 (𝑥 = 𝑧 → (∀𝑤 ∈ (𝐴𝐵)(𝑥 = 𝑤 ∨ (𝐶𝑤 / 𝑥𝐶) = ∅) ↔ ∀𝑤 ∈ (𝐴𝐵)(𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅)))
3831, 37syl5bbr 274 . . . . . 6 (𝑥 = 𝑧 → (∀𝑦 ∈ (𝐴𝐵)(𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅) ↔ ∀𝑤 ∈ (𝐴𝐵)(𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅)))
3914, 22, 38cbvral 3197 . . . . 5 (∀𝑥𝐴𝑦 ∈ (𝐴𝐵)(𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅) ↔ ∀𝑧𝐴𝑤 ∈ (𝐴𝐵)(𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅))
40 r19.26 3093 . . . . 5 (∀𝑥𝐴 (∀𝑦𝐴 (𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅) ∧ ∀𝑦𝐵 (𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅)) ↔ (∀𝑥𝐴𝑦𝐴 (𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅) ∧ ∀𝑥𝐴𝑦𝐵 (𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅)))
4113, 39, 403bitr3i 290 . . . 4 (∀𝑧𝐴𝑤 ∈ (𝐴𝐵)(𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅) ↔ (∀𝑥𝐴𝑦𝐴 (𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅) ∧ ∀𝑥𝐴𝑦𝐵 (𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅)))
4226disjor 4666 . . . . 5 (Disj 𝑥𝐴 𝐶 ↔ ∀𝑥𝐴𝑦𝐴 (𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅))
4342anbi1i 731 . . . 4 ((Disj 𝑥𝐴 𝐶 ∧ ∀𝑥𝐴𝑦𝐵 (𝐶𝐷) = ∅) ↔ (∀𝑥𝐴𝑦𝐴 (𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅) ∧ ∀𝑥𝐴𝑦𝐵 (𝐶𝐷) = ∅))
4411, 41, 433bitr4g 303 . . 3 ((𝐴𝐵) = ∅ → (∀𝑧𝐴𝑤 ∈ (𝐴𝐵)(𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅) ↔ (Disj 𝑥𝐴 𝐶 ∧ ∀𝑥𝐴𝑦𝐵 (𝐶𝐷) = ∅)))
45 nfv 1883 . . . . . . . . . 10 𝑤(𝑧 = 𝑥 ∨ (𝑧 / 𝑥𝐶𝐶) = ∅)
46 equequ2 1999 . . . . . . . . . . 11 (𝑥 = 𝑤 → (𝑧 = 𝑥𝑧 = 𝑤))
47 csbeq1a 3575 . . . . . . . . . . . . 13 (𝑥 = 𝑤𝐶 = 𝑤 / 𝑥𝐶)
4847ineq2d 3847 . . . . . . . . . . . 12 (𝑥 = 𝑤 → (𝑧 / 𝑥𝐶𝐶) = (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶))
4948eqeq1d 2653 . . . . . . . . . . 11 (𝑥 = 𝑤 → ((𝑧 / 𝑥𝐶𝐶) = ∅ ↔ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅))
5046, 49orbi12d 746 . . . . . . . . . 10 (𝑥 = 𝑤 → ((𝑧 = 𝑥 ∨ (𝑧 / 𝑥𝐶𝐶) = ∅) ↔ (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅)))
5145, 21, 50cbvral 3197 . . . . . . . . 9 (∀𝑥𝐴 (𝑧 = 𝑥 ∨ (𝑧 / 𝑥𝐶𝐶) = ∅) ↔ ∀𝑤𝐴 (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅))
52 equequ1 1998 . . . . . . . . . . . 12 (𝑧 = 𝑦 → (𝑧 = 𝑥𝑦 = 𝑥))
53 equcom 1991 . . . . . . . . . . . 12 (𝑦 = 𝑥𝑥 = 𝑦)
5452, 53syl6bb 276 . . . . . . . . . . 11 (𝑧 = 𝑦 → (𝑧 = 𝑥𝑥 = 𝑦))
5524, 25, 26csbhypf 3585 . . . . . . . . . . . . . 14 (𝑧 = 𝑦𝑧 / 𝑥𝐶 = 𝐷)
5655ineq1d 3846 . . . . . . . . . . . . 13 (𝑧 = 𝑦 → (𝑧 / 𝑥𝐶𝐶) = (𝐷𝐶))
57 incom 3838 . . . . . . . . . . . . 13 (𝐷𝐶) = (𝐶𝐷)
5856, 57syl6eq 2701 . . . . . . . . . . . 12 (𝑧 = 𝑦 → (𝑧 / 𝑥𝐶𝐶) = (𝐶𝐷))
5958eqeq1d 2653 . . . . . . . . . . 11 (𝑧 = 𝑦 → ((𝑧 / 𝑥𝐶𝐶) = ∅ ↔ (𝐶𝐷) = ∅))
6054, 59orbi12d 746 . . . . . . . . . 10 (𝑧 = 𝑦 → ((𝑧 = 𝑥 ∨ (𝑧 / 𝑥𝐶𝐶) = ∅) ↔ (𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅)))
6160ralbidv 3015 . . . . . . . . 9 (𝑧 = 𝑦 → (∀𝑥𝐴 (𝑧 = 𝑥 ∨ (𝑧 / 𝑥𝐶𝐶) = ∅) ↔ ∀𝑥𝐴 (𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅)))
6251, 61syl5bbr 274 . . . . . . . 8 (𝑧 = 𝑦 → (∀𝑤𝐴 (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅) ↔ ∀𝑥𝐴 (𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅)))
6362cbvralv 3201 . . . . . . 7 (∀𝑧𝐵𝑤𝐴 (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅) ↔ ∀𝑦𝐵𝑥𝐴 (𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅))
64 ralcom 3127 . . . . . . 7 (∀𝑦𝐵𝑥𝐴 (𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅) ↔ ∀𝑥𝐴𝑦𝐵 (𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅))
6563, 64bitri 264 . . . . . 6 (∀𝑧𝐵𝑤𝐴 (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅) ↔ ∀𝑥𝐴𝑦𝐵 (𝑥 = 𝑦 ∨ (𝐶𝐷) = ∅))
6665, 10syl5bb 272 . . . . 5 ((𝐴𝐵) = ∅ → (∀𝑧𝐵𝑤𝐴 (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅) ↔ ∀𝑥𝐴𝑦𝐵 (𝐶𝐷) = ∅))
6766anbi1d 741 . . . 4 ((𝐴𝐵) = ∅ → ((∀𝑧𝐵𝑤𝐴 (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅) ∧ ∀𝑧𝐵𝑤𝐵 (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅)) ↔ (∀𝑥𝐴𝑦𝐵 (𝐶𝐷) = ∅ ∧ ∀𝑧𝐵𝑤𝐵 (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅))))
68 ralunb 3827 . . . . . 6 (∀𝑤 ∈ (𝐴𝐵)(𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅) ↔ (∀𝑤𝐴 (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅) ∧ ∀𝑤𝐵 (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅)))
6968ralbii 3009 . . . . 5 (∀𝑧𝐵𝑤 ∈ (𝐴𝐵)(𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅) ↔ ∀𝑧𝐵 (∀𝑤𝐴 (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅) ∧ ∀𝑤𝐵 (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅)))
70 r19.26 3093 . . . . 5 (∀𝑧𝐵 (∀𝑤𝐴 (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅) ∧ ∀𝑤𝐵 (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅)) ↔ (∀𝑧𝐵𝑤𝐴 (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅) ∧ ∀𝑧𝐵𝑤𝐵 (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅)))
7169, 70bitri 264 . . . 4 (∀𝑧𝐵𝑤 ∈ (𝐴𝐵)(𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅) ↔ (∀𝑧𝐵𝑤𝐴 (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅) ∧ ∀𝑧𝐵𝑤𝐵 (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅)))
72 disjors 4667 . . . . 5 (Disj 𝑥𝐵 𝐶 ↔ ∀𝑧𝐵𝑤𝐵 (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅))
7372anbi2ci 732 . . . 4 ((Disj 𝑥𝐵 𝐶 ∧ ∀𝑥𝐴𝑦𝐵 (𝐶𝐷) = ∅) ↔ (∀𝑥𝐴𝑦𝐵 (𝐶𝐷) = ∅ ∧ ∀𝑧𝐵𝑤𝐵 (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅)))
7467, 71, 733bitr4g 303 . . 3 ((𝐴𝐵) = ∅ → (∀𝑧𝐵𝑤 ∈ (𝐴𝐵)(𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅) ↔ (Disj 𝑥𝐵 𝐶 ∧ ∀𝑥𝐴𝑦𝐵 (𝐶𝐷) = ∅)))
7544, 74anbi12d 747 . 2 ((𝐴𝐵) = ∅ → ((∀𝑧𝐴𝑤 ∈ (𝐴𝐵)(𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅) ∧ ∀𝑧𝐵𝑤 ∈ (𝐴𝐵)(𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅)) ↔ ((Disj 𝑥𝐴 𝐶 ∧ ∀𝑥𝐴𝑦𝐵 (𝐶𝐷) = ∅) ∧ (Disj 𝑥𝐵 𝐶 ∧ ∀𝑥𝐴𝑦𝐵 (𝐶𝐷) = ∅))))
76 disjors 4667 . . 3 (Disj 𝑥 ∈ (𝐴𝐵)𝐶 ↔ ∀𝑧 ∈ (𝐴𝐵)∀𝑤 ∈ (𝐴𝐵)(𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅))
77 ralunb 3827 . . 3 (∀𝑧 ∈ (𝐴𝐵)∀𝑤 ∈ (𝐴𝐵)(𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅) ↔ (∀𝑧𝐴𝑤 ∈ (𝐴𝐵)(𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅) ∧ ∀𝑧𝐵𝑤 ∈ (𝐴𝐵)(𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅)))
7876, 77bitri 264 . 2 (Disj 𝑥 ∈ (𝐴𝐵)𝐶 ↔ (∀𝑧𝐴𝑤 ∈ (𝐴𝐵)(𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅) ∧ ∀𝑧𝐵𝑤 ∈ (𝐴𝐵)(𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐶𝑤 / 𝑥𝐶) = ∅)))
79 df-3an 1056 . . 3 ((Disj 𝑥𝐴 𝐶Disj 𝑥𝐵 𝐶 ∧ ∀𝑥𝐴𝑦𝐵 (𝐶𝐷) = ∅) ↔ ((Disj 𝑥𝐴 𝐶Disj 𝑥𝐵 𝐶) ∧ ∀𝑥𝐴𝑦𝐵 (𝐶𝐷) = ∅))
80 anandir 889 . . 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 1054   = wceq 1523  wcel 2030  wral 2941  csb 3566  cun 3605  cin 3606  c0 3948  Disj wdisj 4652
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-nul 3949  df-disj 4653
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator