Mathbox for Richard Penner < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  uneqsn Structured version   Visualization version   GIF version

Theorem uneqsn 37341
 Description: If a union of classes is equal to a singleton then at least one class is equal to the singleton while the other may be equal to the empty set. (Contributed by RP, 5-Jul-2021.)
Assertion
Ref Expression
uneqsn ((𝐴𝐵) = {𝐶} ↔ ((𝐴 = {𝐶} ∧ 𝐵 = {𝐶}) ∨ (𝐴 = {𝐶} ∧ 𝐵 = ∅) ∨ (𝐴 = ∅ ∧ 𝐵 = {𝐶})))

Proof of Theorem uneqsn
StepHypRef Expression
1 eqss 3583 . . . 4 ((𝐴𝐵) = {𝐶} ↔ ((𝐴𝐵) ⊆ {𝐶} ∧ {𝐶} ⊆ (𝐴𝐵)))
21a1i 11 . . 3 (𝐶 ∈ V → ((𝐴𝐵) = {𝐶} ↔ ((𝐴𝐵) ⊆ {𝐶} ∧ {𝐶} ⊆ (𝐴𝐵))))
3 unss 3749 . . . . . 6 ((𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}) ↔ (𝐴𝐵) ⊆ {𝐶})
43bicomi 213 . . . . 5 ((𝐴𝐵) ⊆ {𝐶} ↔ (𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}))
54a1i 11 . . . 4 (𝐶 ∈ V → ((𝐴𝐵) ⊆ {𝐶} ↔ (𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶})))
6 elun 3715 . . . . . 6 (𝐶 ∈ (𝐴𝐵) ↔ (𝐶𝐴𝐶𝐵))
7 snssg 4268 . . . . . . 7 (𝐶 ∈ V → (𝐶𝐴 ↔ {𝐶} ⊆ 𝐴))
8 snssg 4268 . . . . . . 7 (𝐶 ∈ V → (𝐶𝐵 ↔ {𝐶} ⊆ 𝐵))
97, 8orbi12d 742 . . . . . 6 (𝐶 ∈ V → ((𝐶𝐴𝐶𝐵) ↔ ({𝐶} ⊆ 𝐴 ∨ {𝐶} ⊆ 𝐵)))
106, 9syl5rbb 272 . . . . 5 (𝐶 ∈ V → (({𝐶} ⊆ 𝐴 ∨ {𝐶} ⊆ 𝐵) ↔ 𝐶 ∈ (𝐴𝐵)))
11 snssg 4268 . . . . 5 (𝐶 ∈ V → (𝐶 ∈ (𝐴𝐵) ↔ {𝐶} ⊆ (𝐴𝐵)))
1210, 11bitr2d 268 . . . 4 (𝐶 ∈ V → ({𝐶} ⊆ (𝐴𝐵) ↔ ({𝐶} ⊆ 𝐴 ∨ {𝐶} ⊆ 𝐵)))
135, 12anbi12d 743 . . 3 (𝐶 ∈ V → (((𝐴𝐵) ⊆ {𝐶} ∧ {𝐶} ⊆ (𝐴𝐵)) ↔ ((𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}) ∧ ({𝐶} ⊆ 𝐴 ∨ {𝐶} ⊆ 𝐵))))
14 or3or 37339 . . . . . 6 (({𝐶} ⊆ 𝐴 ∨ {𝐶} ⊆ 𝐵) ↔ (({𝐶} ⊆ 𝐴 ∧ {𝐶} ⊆ 𝐵) ∨ ({𝐶} ⊆ 𝐴 ∧ ¬ {𝐶} ⊆ 𝐵) ∨ (¬ {𝐶} ⊆ 𝐴 ∧ {𝐶} ⊆ 𝐵)))
1514anbi2i 726 . . . . 5 (((𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}) ∧ ({𝐶} ⊆ 𝐴 ∨ {𝐶} ⊆ 𝐵)) ↔ ((𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}) ∧ (({𝐶} ⊆ 𝐴 ∧ {𝐶} ⊆ 𝐵) ∨ ({𝐶} ⊆ 𝐴 ∧ ¬ {𝐶} ⊆ 𝐵) ∨ (¬ {𝐶} ⊆ 𝐴 ∧ {𝐶} ⊆ 𝐵))))
16 andi3or 37340 . . . . 5 (((𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}) ∧ (({𝐶} ⊆ 𝐴 ∧ {𝐶} ⊆ 𝐵) ∨ ({𝐶} ⊆ 𝐴 ∧ ¬ {𝐶} ⊆ 𝐵) ∨ (¬ {𝐶} ⊆ 𝐴 ∧ {𝐶} ⊆ 𝐵))) ↔ (((𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}) ∧ ({𝐶} ⊆ 𝐴 ∧ {𝐶} ⊆ 𝐵)) ∨ ((𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}) ∧ ({𝐶} ⊆ 𝐴 ∧ ¬ {𝐶} ⊆ 𝐵)) ∨ ((𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}) ∧ (¬ {𝐶} ⊆ 𝐴 ∧ {𝐶} ⊆ 𝐵))))
1715, 16bitri 263 . . . 4 (((𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}) ∧ ({𝐶} ⊆ 𝐴 ∨ {𝐶} ⊆ 𝐵)) ↔ (((𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}) ∧ ({𝐶} ⊆ 𝐴 ∧ {𝐶} ⊆ 𝐵)) ∨ ((𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}) ∧ ({𝐶} ⊆ 𝐴 ∧ ¬ {𝐶} ⊆ 𝐵)) ∨ ((𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}) ∧ (¬ {𝐶} ⊆ 𝐴 ∧ {𝐶} ⊆ 𝐵))))
18 an4 861 . . . . . . 7 (((𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}) ∧ ({𝐶} ⊆ 𝐴 ∧ {𝐶} ⊆ 𝐵)) ↔ ((𝐴 ⊆ {𝐶} ∧ {𝐶} ⊆ 𝐴) ∧ (𝐵 ⊆ {𝐶} ∧ {𝐶} ⊆ 𝐵)))
19 eqss 3583 . . . . . . . . 9 (𝐴 = {𝐶} ↔ (𝐴 ⊆ {𝐶} ∧ {𝐶} ⊆ 𝐴))
20 eqss 3583 . . . . . . . . 9 (𝐵 = {𝐶} ↔ (𝐵 ⊆ {𝐶} ∧ {𝐶} ⊆ 𝐵))
2119, 20anbi12i 729 . . . . . . . 8 ((𝐴 = {𝐶} ∧ 𝐵 = {𝐶}) ↔ ((𝐴 ⊆ {𝐶} ∧ {𝐶} ⊆ 𝐴) ∧ (𝐵 ⊆ {𝐶} ∧ {𝐶} ⊆ 𝐵)))
2221bicomi 213 . . . . . . 7 (((𝐴 ⊆ {𝐶} ∧ {𝐶} ⊆ 𝐴) ∧ (𝐵 ⊆ {𝐶} ∧ {𝐶} ⊆ 𝐵)) ↔ (𝐴 = {𝐶} ∧ 𝐵 = {𝐶}))
2318, 22bitri 263 . . . . . 6 (((𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}) ∧ ({𝐶} ⊆ 𝐴 ∧ {𝐶} ⊆ 𝐵)) ↔ (𝐴 = {𝐶} ∧ 𝐵 = {𝐶}))
2423a1i 11 . . . . 5 (𝐶 ∈ V → (((𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}) ∧ ({𝐶} ⊆ 𝐴 ∧ {𝐶} ⊆ 𝐵)) ↔ (𝐴 = {𝐶} ∧ 𝐵 = {𝐶})))
25 an4 861 . . . . . 6 (((𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}) ∧ ({𝐶} ⊆ 𝐴 ∧ ¬ {𝐶} ⊆ 𝐵)) ↔ ((𝐴 ⊆ {𝐶} ∧ {𝐶} ⊆ 𝐴) ∧ (𝐵 ⊆ {𝐶} ∧ ¬ {𝐶} ⊆ 𝐵)))
2619bicomi 213 . . . . . . . 8 ((𝐴 ⊆ {𝐶} ∧ {𝐶} ⊆ 𝐴) ↔ 𝐴 = {𝐶})
2726a1i 11 . . . . . . 7 (𝐶 ∈ V → ((𝐴 ⊆ {𝐶} ∧ {𝐶} ⊆ 𝐴) ↔ 𝐴 = {𝐶}))
28 sssn 4298 . . . . . . . . . 10 (𝐵 ⊆ {𝐶} ↔ (𝐵 = ∅ ∨ 𝐵 = {𝐶}))
2928a1i 11 . . . . . . . . 9 (𝐶 ∈ V → (𝐵 ⊆ {𝐶} ↔ (𝐵 = ∅ ∨ 𝐵 = {𝐶})))
3029anbi1d 737 . . . . . . . 8 (𝐶 ∈ V → ((𝐵 ⊆ {𝐶} ∧ ¬ {𝐶} ⊆ 𝐵) ↔ ((𝐵 = ∅ ∨ 𝐵 = {𝐶}) ∧ ¬ {𝐶} ⊆ 𝐵)))
31 andir 908 . . . . . . . . 9 (((𝐵 = ∅ ∨ 𝐵 = {𝐶}) ∧ ¬ {𝐶} ⊆ 𝐵) ↔ ((𝐵 = ∅ ∧ ¬ {𝐶} ⊆ 𝐵) ∨ (𝐵 = {𝐶} ∧ ¬ {𝐶} ⊆ 𝐵)))
32 n0i 3879 . . . . . . . . . . . . 13 (𝐶𝐵 → ¬ 𝐵 = ∅)
338, 32syl6bir 243 . . . . . . . . . . . 12 (𝐶 ∈ V → ({𝐶} ⊆ 𝐵 → ¬ 𝐵 = ∅))
3433con2d 128 . . . . . . . . . . 11 (𝐶 ∈ V → (𝐵 = ∅ → ¬ {𝐶} ⊆ 𝐵))
3534pm4.71d 664 . . . . . . . . . 10 (𝐶 ∈ V → (𝐵 = ∅ ↔ (𝐵 = ∅ ∧ ¬ {𝐶} ⊆ 𝐵)))
36 eqimss2 3621 . . . . . . . . . . . 12 (𝐵 = {𝐶} → {𝐶} ⊆ 𝐵)
37 iman 439 . . . . . . . . . . . 12 ((𝐵 = {𝐶} → {𝐶} ⊆ 𝐵) ↔ ¬ (𝐵 = {𝐶} ∧ ¬ {𝐶} ⊆ 𝐵))
3836, 37mpbi 219 . . . . . . . . . . 11 ¬ (𝐵 = {𝐶} ∧ ¬ {𝐶} ⊆ 𝐵)
3938biorfi 421 . . . . . . . . . 10 ((𝐵 = ∅ ∧ ¬ {𝐶} ⊆ 𝐵) ↔ ((𝐵 = ∅ ∧ ¬ {𝐶} ⊆ 𝐵) ∨ (𝐵 = {𝐶} ∧ ¬ {𝐶} ⊆ 𝐵)))
4035, 39syl6rbb 276 . . . . . . . . 9 (𝐶 ∈ V → (((𝐵 = ∅ ∧ ¬ {𝐶} ⊆ 𝐵) ∨ (𝐵 = {𝐶} ∧ ¬ {𝐶} ⊆ 𝐵)) ↔ 𝐵 = ∅))
4131, 40syl5bb 271 . . . . . . . 8 (𝐶 ∈ V → (((𝐵 = ∅ ∨ 𝐵 = {𝐶}) ∧ ¬ {𝐶} ⊆ 𝐵) ↔ 𝐵 = ∅))
4230, 41bitrd 267 . . . . . . 7 (𝐶 ∈ V → ((𝐵 ⊆ {𝐶} ∧ ¬ {𝐶} ⊆ 𝐵) ↔ 𝐵 = ∅))
4327, 42anbi12d 743 . . . . . 6 (𝐶 ∈ V → (((𝐴 ⊆ {𝐶} ∧ {𝐶} ⊆ 𝐴) ∧ (𝐵 ⊆ {𝐶} ∧ ¬ {𝐶} ⊆ 𝐵)) ↔ (𝐴 = {𝐶} ∧ 𝐵 = ∅)))
4425, 43syl5bb 271 . . . . 5 (𝐶 ∈ V → (((𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}) ∧ ({𝐶} ⊆ 𝐴 ∧ ¬ {𝐶} ⊆ 𝐵)) ↔ (𝐴 = {𝐶} ∧ 𝐵 = ∅)))
45 an4 861 . . . . . 6 (((𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}) ∧ (¬ {𝐶} ⊆ 𝐴 ∧ {𝐶} ⊆ 𝐵)) ↔ ((𝐴 ⊆ {𝐶} ∧ ¬ {𝐶} ⊆ 𝐴) ∧ (𝐵 ⊆ {𝐶} ∧ {𝐶} ⊆ 𝐵)))
46 sssn 4298 . . . . . . . . . 10 (𝐴 ⊆ {𝐶} ↔ (𝐴 = ∅ ∨ 𝐴 = {𝐶}))
4746a1i 11 . . . . . . . . 9 (𝐶 ∈ V → (𝐴 ⊆ {𝐶} ↔ (𝐴 = ∅ ∨ 𝐴 = {𝐶})))
4847anbi1d 737 . . . . . . . 8 (𝐶 ∈ V → ((𝐴 ⊆ {𝐶} ∧ ¬ {𝐶} ⊆ 𝐴) ↔ ((𝐴 = ∅ ∨ 𝐴 = {𝐶}) ∧ ¬ {𝐶} ⊆ 𝐴)))
49 andir 908 . . . . . . . . 9 (((𝐴 = ∅ ∨ 𝐴 = {𝐶}) ∧ ¬ {𝐶} ⊆ 𝐴) ↔ ((𝐴 = ∅ ∧ ¬ {𝐶} ⊆ 𝐴) ∨ (𝐴 = {𝐶} ∧ ¬ {𝐶} ⊆ 𝐴)))
50 n0i 3879 . . . . . . . . . . . . 13 (𝐶𝐴 → ¬ 𝐴 = ∅)
517, 50syl6bir 243 . . . . . . . . . . . 12 (𝐶 ∈ V → ({𝐶} ⊆ 𝐴 → ¬ 𝐴 = ∅))
5251con2d 128 . . . . . . . . . . 11 (𝐶 ∈ V → (𝐴 = ∅ → ¬ {𝐶} ⊆ 𝐴))
5352pm4.71d 664 . . . . . . . . . 10 (𝐶 ∈ V → (𝐴 = ∅ ↔ (𝐴 = ∅ ∧ ¬ {𝐶} ⊆ 𝐴)))
54 eqimss2 3621 . . . . . . . . . . . 12 (𝐴 = {𝐶} → {𝐶} ⊆ 𝐴)
55 iman 439 . . . . . . . . . . . 12 ((𝐴 = {𝐶} → {𝐶} ⊆ 𝐴) ↔ ¬ (𝐴 = {𝐶} ∧ ¬ {𝐶} ⊆ 𝐴))
5654, 55mpbi 219 . . . . . . . . . . 11 ¬ (𝐴 = {𝐶} ∧ ¬ {𝐶} ⊆ 𝐴)
5756biorfi 421 . . . . . . . . . 10 ((𝐴 = ∅ ∧ ¬ {𝐶} ⊆ 𝐴) ↔ ((𝐴 = ∅ ∧ ¬ {𝐶} ⊆ 𝐴) ∨ (𝐴 = {𝐶} ∧ ¬ {𝐶} ⊆ 𝐴)))
5853, 57syl6rbb 276 . . . . . . . . 9 (𝐶 ∈ V → (((𝐴 = ∅ ∧ ¬ {𝐶} ⊆ 𝐴) ∨ (𝐴 = {𝐶} ∧ ¬ {𝐶} ⊆ 𝐴)) ↔ 𝐴 = ∅))
5949, 58syl5bb 271 . . . . . . . 8 (𝐶 ∈ V → (((𝐴 = ∅ ∨ 𝐴 = {𝐶}) ∧ ¬ {𝐶} ⊆ 𝐴) ↔ 𝐴 = ∅))
6048, 59bitrd 267 . . . . . . 7 (𝐶 ∈ V → ((𝐴 ⊆ {𝐶} ∧ ¬ {𝐶} ⊆ 𝐴) ↔ 𝐴 = ∅))
6120bicomi 213 . . . . . . . 8 ((𝐵 ⊆ {𝐶} ∧ {𝐶} ⊆ 𝐵) ↔ 𝐵 = {𝐶})
6261a1i 11 . . . . . . 7 (𝐶 ∈ V → ((𝐵 ⊆ {𝐶} ∧ {𝐶} ⊆ 𝐵) ↔ 𝐵 = {𝐶}))
6360, 62anbi12d 743 . . . . . 6 (𝐶 ∈ V → (((𝐴 ⊆ {𝐶} ∧ ¬ {𝐶} ⊆ 𝐴) ∧ (𝐵 ⊆ {𝐶} ∧ {𝐶} ⊆ 𝐵)) ↔ (𝐴 = ∅ ∧ 𝐵 = {𝐶})))
6445, 63syl5bb 271 . . . . 5 (𝐶 ∈ V → (((𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}) ∧ (¬ {𝐶} ⊆ 𝐴 ∧ {𝐶} ⊆ 𝐵)) ↔ (𝐴 = ∅ ∧ 𝐵 = {𝐶})))
6524, 44, 643orbi123d 1390 . . . 4 (𝐶 ∈ V → ((((𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}) ∧ ({𝐶} ⊆ 𝐴 ∧ {𝐶} ⊆ 𝐵)) ∨ ((𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}) ∧ ({𝐶} ⊆ 𝐴 ∧ ¬ {𝐶} ⊆ 𝐵)) ∨ ((𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}) ∧ (¬ {𝐶} ⊆ 𝐴 ∧ {𝐶} ⊆ 𝐵))) ↔ ((𝐴 = {𝐶} ∧ 𝐵 = {𝐶}) ∨ (𝐴 = {𝐶} ∧ 𝐵 = ∅) ∨ (𝐴 = ∅ ∧ 𝐵 = {𝐶}))))
6617, 65syl5bb 271 . . 3 (𝐶 ∈ V → (((𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}) ∧ ({𝐶} ⊆ 𝐴 ∨ {𝐶} ⊆ 𝐵)) ↔ ((𝐴 = {𝐶} ∧ 𝐵 = {𝐶}) ∨ (𝐴 = {𝐶} ∧ 𝐵 = ∅) ∨ (𝐴 = ∅ ∧ 𝐵 = {𝐶}))))
672, 13, 663bitrd 293 . 2 (𝐶 ∈ V → ((𝐴𝐵) = {𝐶} ↔ ((𝐴 = {𝐶} ∧ 𝐵 = {𝐶}) ∨ (𝐴 = {𝐶} ∧ 𝐵 = ∅) ∨ (𝐴 = ∅ ∧ 𝐵 = {𝐶}))))
68 snprc 4197 . . . . 5 𝐶 ∈ V ↔ {𝐶} = ∅)
6968biimpi 205 . . . 4 𝐶 ∈ V → {𝐶} = ∅)
7069eqeq2d 2620 . . 3 𝐶 ∈ V → ((𝐴𝐵) = {𝐶} ↔ (𝐴𝐵) = ∅))
7169eqeq2d 2620 . . . . . . . 8 𝐶 ∈ V → (𝐴 = {𝐶} ↔ 𝐴 = ∅))
7269eqeq2d 2620 . . . . . . . 8 𝐶 ∈ V → (𝐵 = {𝐶} ↔ 𝐵 = ∅))
7371, 72anbi12d 743 . . . . . . 7 𝐶 ∈ V → ((𝐴 = {𝐶} ∧ 𝐵 = {𝐶}) ↔ (𝐴 = ∅ ∧ 𝐵 = ∅)))
7471anbi1d 737 . . . . . . 7 𝐶 ∈ V → ((𝐴 = {𝐶} ∧ 𝐵 = ∅) ↔ (𝐴 = ∅ ∧ 𝐵 = ∅)))
7573, 74orbi12d 742 . . . . . 6 𝐶 ∈ V → (((𝐴 = {𝐶} ∧ 𝐵 = {𝐶}) ∨ (𝐴 = {𝐶} ∧ 𝐵 = ∅)) ↔ ((𝐴 = ∅ ∧ 𝐵 = ∅) ∨ (𝐴 = ∅ ∧ 𝐵 = ∅))))
7672anbi2d 736 . . . . . 6 𝐶 ∈ V → ((𝐴 = ∅ ∧ 𝐵 = {𝐶}) ↔ (𝐴 = ∅ ∧ 𝐵 = ∅)))
7775, 76orbi12d 742 . . . . 5 𝐶 ∈ V → ((((𝐴 = {𝐶} ∧ 𝐵 = {𝐶}) ∨ (𝐴 = {𝐶} ∧ 𝐵 = ∅)) ∨ (𝐴 = ∅ ∧ 𝐵 = {𝐶})) ↔ (((𝐴 = ∅ ∧ 𝐵 = ∅) ∨ (𝐴 = ∅ ∧ 𝐵 = ∅)) ∨ (𝐴 = ∅ ∧ 𝐵 = ∅))))
78 pm4.25 536 . . . . . 6 ((𝐴 = ∅ ∧ 𝐵 = ∅) ↔ ((𝐴 = ∅ ∧ 𝐵 = ∅) ∨ (𝐴 = ∅ ∧ 𝐵 = ∅)))
7978orbi1i 541 . . . . . 6 (((𝐴 = ∅ ∧ 𝐵 = ∅) ∨ (𝐴 = ∅ ∧ 𝐵 = ∅)) ↔ (((𝐴 = ∅ ∧ 𝐵 = ∅) ∨ (𝐴 = ∅ ∧ 𝐵 = ∅)) ∨ (𝐴 = ∅ ∧ 𝐵 = ∅)))
8078, 79bitri 263 . . . . 5 ((𝐴 = ∅ ∧ 𝐵 = ∅) ↔ (((𝐴 = ∅ ∧ 𝐵 = ∅) ∨ (𝐴 = ∅ ∧ 𝐵 = ∅)) ∨ (𝐴 = ∅ ∧ 𝐵 = ∅)))
8177, 80syl6rbbr 278 . . . 4 𝐶 ∈ V → ((𝐴 = ∅ ∧ 𝐵 = ∅) ↔ (((𝐴 = {𝐶} ∧ 𝐵 = {𝐶}) ∨ (𝐴 = {𝐶} ∧ 𝐵 = ∅)) ∨ (𝐴 = ∅ ∧ 𝐵 = {𝐶}))))
82 un00 3963 . . . . 5 ((𝐴 = ∅ ∧ 𝐵 = ∅) ↔ (𝐴𝐵) = ∅)
8382bicomi 213 . . . 4 ((𝐴𝐵) = ∅ ↔ (𝐴 = ∅ ∧ 𝐵 = ∅))
84 df-3or 1032 . . . 4 (((𝐴 = {𝐶} ∧ 𝐵 = {𝐶}) ∨ (𝐴 = {𝐶} ∧ 𝐵 = ∅) ∨ (𝐴 = ∅ ∧ 𝐵 = {𝐶})) ↔ (((𝐴 = {𝐶} ∧ 𝐵 = {𝐶}) ∨ (𝐴 = {𝐶} ∧ 𝐵 = ∅)) ∨ (𝐴 = ∅ ∧ 𝐵 = {𝐶})))
8581, 83, 843bitr4g 302 . . 3 𝐶 ∈ V → ((𝐴𝐵) = ∅ ↔ ((𝐴 = {𝐶} ∧ 𝐵 = {𝐶}) ∨ (𝐴 = {𝐶} ∧ 𝐵 = ∅) ∨ (𝐴 = ∅ ∧ 𝐵 = {𝐶}))))
8670, 85bitrd 267 . 2 𝐶 ∈ V → ((𝐴𝐵) = {𝐶} ↔ ((𝐴 = {𝐶} ∧ 𝐵 = {𝐶}) ∨ (𝐴 = {𝐶} ∧ 𝐵 = ∅) ∨ (𝐴 = ∅ ∧ 𝐵 = {𝐶}))))
8767, 86pm2.61i 175 1 ((𝐴𝐵) = {𝐶} ↔ ((𝐴 = {𝐶} ∧ 𝐵 = {𝐶}) ∨ (𝐴 = {𝐶} ∧ 𝐵 = ∅) ∨ (𝐴 = ∅ ∧ 𝐵 = {𝐶})))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∨ wo 382   ∧ wa 383   ∨ w3o 1030   = wceq 1475   ∈ wcel 1977  Vcvv 3173   ∪ cun 3538   ⊆ wss 3540  ∅c0 3874  {csn 4125 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-xor 1457  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-sn 4126 This theorem is referenced by:  clsk1indlem3  37361
 Copyright terms: Public domain W3C validator