Proof of Theorem uneqsn
Step | Hyp | Ref
| Expression |
1 | | eqss 3916 |
. . . 4
⊢ ((𝐴 ∪ 𝐵) = {𝐶} ↔ ((𝐴 ∪ 𝐵) ⊆ {𝐶} ∧ {𝐶} ⊆ (𝐴 ∪ 𝐵))) |
2 | 1 | a1i 11 |
. . 3
⊢ (𝐶 ∈ V → ((𝐴 ∪ 𝐵) = {𝐶} ↔ ((𝐴 ∪ 𝐵) ⊆ {𝐶} ∧ {𝐶} ⊆ (𝐴 ∪ 𝐵)))) |
3 | | unss 4098 |
. . . . . 6
⊢ ((𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}) ↔ (𝐴 ∪ 𝐵) ⊆ {𝐶}) |
4 | 3 | bicomi 227 |
. . . . 5
⊢ ((𝐴 ∪ 𝐵) ⊆ {𝐶} ↔ (𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶})) |
5 | 4 | a1i 11 |
. . . 4
⊢ (𝐶 ∈ V → ((𝐴 ∪ 𝐵) ⊆ {𝐶} ↔ (𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}))) |
6 | | elun 4063 |
. . . . . 6
⊢ (𝐶 ∈ (𝐴 ∪ 𝐵) ↔ (𝐶 ∈ 𝐴 ∨ 𝐶 ∈ 𝐵)) |
7 | | snssg 4698 |
. . . . . . 7
⊢ (𝐶 ∈ V → (𝐶 ∈ 𝐴 ↔ {𝐶} ⊆ 𝐴)) |
8 | | snssg 4698 |
. . . . . . 7
⊢ (𝐶 ∈ V → (𝐶 ∈ 𝐵 ↔ {𝐶} ⊆ 𝐵)) |
9 | 7, 8 | orbi12d 919 |
. . . . . 6
⊢ (𝐶 ∈ V → ((𝐶 ∈ 𝐴 ∨ 𝐶 ∈ 𝐵) ↔ ({𝐶} ⊆ 𝐴 ∨ {𝐶} ⊆ 𝐵))) |
10 | 6, 9 | bitr2id 287 |
. . . . 5
⊢ (𝐶 ∈ V → (({𝐶} ⊆ 𝐴 ∨ {𝐶} ⊆ 𝐵) ↔ 𝐶 ∈ (𝐴 ∪ 𝐵))) |
11 | | snssg 4698 |
. . . . 5
⊢ (𝐶 ∈ V → (𝐶 ∈ (𝐴 ∪ 𝐵) ↔ {𝐶} ⊆ (𝐴 ∪ 𝐵))) |
12 | 10, 11 | bitr2d 283 |
. . . 4
⊢ (𝐶 ∈ V → ({𝐶} ⊆ (𝐴 ∪ 𝐵) ↔ ({𝐶} ⊆ 𝐴 ∨ {𝐶} ⊆ 𝐵))) |
13 | 5, 12 | anbi12d 634 |
. . 3
⊢ (𝐶 ∈ V → (((𝐴 ∪ 𝐵) ⊆ {𝐶} ∧ {𝐶} ⊆ (𝐴 ∪ 𝐵)) ↔ ((𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}) ∧ ({𝐶} ⊆ 𝐴 ∨ {𝐶} ⊆ 𝐵)))) |
14 | | or3or 41308 |
. . . . . 6
⊢ (({𝐶} ⊆ 𝐴 ∨ {𝐶} ⊆ 𝐵) ↔ (({𝐶} ⊆ 𝐴 ∧ {𝐶} ⊆ 𝐵) ∨ ({𝐶} ⊆ 𝐴 ∧ ¬ {𝐶} ⊆ 𝐵) ∨ (¬ {𝐶} ⊆ 𝐴 ∧ {𝐶} ⊆ 𝐵))) |
15 | 14 | anbi2i 626 |
. . . . 5
⊢ (((𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}) ∧ ({𝐶} ⊆ 𝐴 ∨ {𝐶} ⊆ 𝐵)) ↔ ((𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}) ∧ (({𝐶} ⊆ 𝐴 ∧ {𝐶} ⊆ 𝐵) ∨ ({𝐶} ⊆ 𝐴 ∧ ¬ {𝐶} ⊆ 𝐵) ∨ (¬ {𝐶} ⊆ 𝐴 ∧ {𝐶} ⊆ 𝐵)))) |
16 | | andi3or 41309 |
. . . . 5
⊢ (((𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}) ∧ (({𝐶} ⊆ 𝐴 ∧ {𝐶} ⊆ 𝐵) ∨ ({𝐶} ⊆ 𝐴 ∧ ¬ {𝐶} ⊆ 𝐵) ∨ (¬ {𝐶} ⊆ 𝐴 ∧ {𝐶} ⊆ 𝐵))) ↔ (((𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}) ∧ ({𝐶} ⊆ 𝐴 ∧ {𝐶} ⊆ 𝐵)) ∨ ((𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}) ∧ ({𝐶} ⊆ 𝐴 ∧ ¬ {𝐶} ⊆ 𝐵)) ∨ ((𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}) ∧ (¬ {𝐶} ⊆ 𝐴 ∧ {𝐶} ⊆ 𝐵)))) |
17 | 15, 16 | bitri 278 |
. . . 4
⊢ (((𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}) ∧ ({𝐶} ⊆ 𝐴 ∨ {𝐶} ⊆ 𝐵)) ↔ (((𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}) ∧ ({𝐶} ⊆ 𝐴 ∧ {𝐶} ⊆ 𝐵)) ∨ ((𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}) ∧ ({𝐶} ⊆ 𝐴 ∧ ¬ {𝐶} ⊆ 𝐵)) ∨ ((𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}) ∧ (¬ {𝐶} ⊆ 𝐴 ∧ {𝐶} ⊆ 𝐵)))) |
18 | | an4 656 |
. . . . . . 7
⊢ (((𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}) ∧ ({𝐶} ⊆ 𝐴 ∧ {𝐶} ⊆ 𝐵)) ↔ ((𝐴 ⊆ {𝐶} ∧ {𝐶} ⊆ 𝐴) ∧ (𝐵 ⊆ {𝐶} ∧ {𝐶} ⊆ 𝐵))) |
19 | | eqss 3916 |
. . . . . . . . 9
⊢ (𝐴 = {𝐶} ↔ (𝐴 ⊆ {𝐶} ∧ {𝐶} ⊆ 𝐴)) |
20 | | eqss 3916 |
. . . . . . . . 9
⊢ (𝐵 = {𝐶} ↔ (𝐵 ⊆ {𝐶} ∧ {𝐶} ⊆ 𝐵)) |
21 | 19, 20 | anbi12i 630 |
. . . . . . . 8
⊢ ((𝐴 = {𝐶} ∧ 𝐵 = {𝐶}) ↔ ((𝐴 ⊆ {𝐶} ∧ {𝐶} ⊆ 𝐴) ∧ (𝐵 ⊆ {𝐶} ∧ {𝐶} ⊆ 𝐵))) |
22 | 21 | bicomi 227 |
. . . . . . 7
⊢ (((𝐴 ⊆ {𝐶} ∧ {𝐶} ⊆ 𝐴) ∧ (𝐵 ⊆ {𝐶} ∧ {𝐶} ⊆ 𝐵)) ↔ (𝐴 = {𝐶} ∧ 𝐵 = {𝐶})) |
23 | 18, 22 | bitri 278 |
. . . . . 6
⊢ (((𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}) ∧ ({𝐶} ⊆ 𝐴 ∧ {𝐶} ⊆ 𝐵)) ↔ (𝐴 = {𝐶} ∧ 𝐵 = {𝐶})) |
24 | 23 | a1i 11 |
. . . . 5
⊢ (𝐶 ∈ V → (((𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}) ∧ ({𝐶} ⊆ 𝐴 ∧ {𝐶} ⊆ 𝐵)) ↔ (𝐴 = {𝐶} ∧ 𝐵 = {𝐶}))) |
25 | | an4 656 |
. . . . . 6
⊢ (((𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}) ∧ ({𝐶} ⊆ 𝐴 ∧ ¬ {𝐶} ⊆ 𝐵)) ↔ ((𝐴 ⊆ {𝐶} ∧ {𝐶} ⊆ 𝐴) ∧ (𝐵 ⊆ {𝐶} ∧ ¬ {𝐶} ⊆ 𝐵))) |
26 | 19 | bicomi 227 |
. . . . . . . 8
⊢ ((𝐴 ⊆ {𝐶} ∧ {𝐶} ⊆ 𝐴) ↔ 𝐴 = {𝐶}) |
27 | 26 | a1i 11 |
. . . . . . 7
⊢ (𝐶 ∈ V → ((𝐴 ⊆ {𝐶} ∧ {𝐶} ⊆ 𝐴) ↔ 𝐴 = {𝐶})) |
28 | | sssn 4739 |
. . . . . . . . . 10
⊢ (𝐵 ⊆ {𝐶} ↔ (𝐵 = ∅ ∨ 𝐵 = {𝐶})) |
29 | 28 | a1i 11 |
. . . . . . . . 9
⊢ (𝐶 ∈ V → (𝐵 ⊆ {𝐶} ↔ (𝐵 = ∅ ∨ 𝐵 = {𝐶}))) |
30 | 29 | anbi1d 633 |
. . . . . . . 8
⊢ (𝐶 ∈ V → ((𝐵 ⊆ {𝐶} ∧ ¬ {𝐶} ⊆ 𝐵) ↔ ((𝐵 = ∅ ∨ 𝐵 = {𝐶}) ∧ ¬ {𝐶} ⊆ 𝐵))) |
31 | | andir 1009 |
. . . . . . . . 9
⊢ (((𝐵 = ∅ ∨ 𝐵 = {𝐶}) ∧ ¬ {𝐶} ⊆ 𝐵) ↔ ((𝐵 = ∅ ∧ ¬ {𝐶} ⊆ 𝐵) ∨ (𝐵 = {𝐶} ∧ ¬ {𝐶} ⊆ 𝐵))) |
32 | | n0i 4248 |
. . . . . . . . . . . . 13
⊢ (𝐶 ∈ 𝐵 → ¬ 𝐵 = ∅) |
33 | 8, 32 | syl6bir 257 |
. . . . . . . . . . . 12
⊢ (𝐶 ∈ V → ({𝐶} ⊆ 𝐵 → ¬ 𝐵 = ∅)) |
34 | 33 | con2d 136 |
. . . . . . . . . . 11
⊢ (𝐶 ∈ V → (𝐵 = ∅ → ¬ {𝐶} ⊆ 𝐵)) |
35 | 34 | pm4.71d 565 |
. . . . . . . . . 10
⊢ (𝐶 ∈ V → (𝐵 = ∅ ↔ (𝐵 = ∅ ∧ ¬ {𝐶} ⊆ 𝐵))) |
36 | | eqimss2 3958 |
. . . . . . . . . . . 12
⊢ (𝐵 = {𝐶} → {𝐶} ⊆ 𝐵) |
37 | | iman 405 |
. . . . . . . . . . . 12
⊢ ((𝐵 = {𝐶} → {𝐶} ⊆ 𝐵) ↔ ¬ (𝐵 = {𝐶} ∧ ¬ {𝐶} ⊆ 𝐵)) |
38 | 36, 37 | mpbi 233 |
. . . . . . . . . . 11
⊢ ¬
(𝐵 = {𝐶} ∧ ¬ {𝐶} ⊆ 𝐵) |
39 | 38 | biorfi 939 |
. . . . . . . . . 10
⊢ ((𝐵 = ∅ ∧ ¬ {𝐶} ⊆ 𝐵) ↔ ((𝐵 = ∅ ∧ ¬ {𝐶} ⊆ 𝐵) ∨ (𝐵 = {𝐶} ∧ ¬ {𝐶} ⊆ 𝐵))) |
40 | 35, 39 | bitr2di 291 |
. . . . . . . . 9
⊢ (𝐶 ∈ V → (((𝐵 = ∅ ∧ ¬ {𝐶} ⊆ 𝐵) ∨ (𝐵 = {𝐶} ∧ ¬ {𝐶} ⊆ 𝐵)) ↔ 𝐵 = ∅)) |
41 | 31, 40 | syl5bb 286 |
. . . . . . . 8
⊢ (𝐶 ∈ V → (((𝐵 = ∅ ∨ 𝐵 = {𝐶}) ∧ ¬ {𝐶} ⊆ 𝐵) ↔ 𝐵 = ∅)) |
42 | 30, 41 | bitrd 282 |
. . . . . . 7
⊢ (𝐶 ∈ V → ((𝐵 ⊆ {𝐶} ∧ ¬ {𝐶} ⊆ 𝐵) ↔ 𝐵 = ∅)) |
43 | 27, 42 | anbi12d 634 |
. . . . . 6
⊢ (𝐶 ∈ V → (((𝐴 ⊆ {𝐶} ∧ {𝐶} ⊆ 𝐴) ∧ (𝐵 ⊆ {𝐶} ∧ ¬ {𝐶} ⊆ 𝐵)) ↔ (𝐴 = {𝐶} ∧ 𝐵 = ∅))) |
44 | 25, 43 | syl5bb 286 |
. . . . 5
⊢ (𝐶 ∈ V → (((𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}) ∧ ({𝐶} ⊆ 𝐴 ∧ ¬ {𝐶} ⊆ 𝐵)) ↔ (𝐴 = {𝐶} ∧ 𝐵 = ∅))) |
45 | | an4 656 |
. . . . . 6
⊢ (((𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}) ∧ (¬ {𝐶} ⊆ 𝐴 ∧ {𝐶} ⊆ 𝐵)) ↔ ((𝐴 ⊆ {𝐶} ∧ ¬ {𝐶} ⊆ 𝐴) ∧ (𝐵 ⊆ {𝐶} ∧ {𝐶} ⊆ 𝐵))) |
46 | | sssn 4739 |
. . . . . . . . . 10
⊢ (𝐴 ⊆ {𝐶} ↔ (𝐴 = ∅ ∨ 𝐴 = {𝐶})) |
47 | 46 | a1i 11 |
. . . . . . . . 9
⊢ (𝐶 ∈ V → (𝐴 ⊆ {𝐶} ↔ (𝐴 = ∅ ∨ 𝐴 = {𝐶}))) |
48 | 47 | anbi1d 633 |
. . . . . . . 8
⊢ (𝐶 ∈ V → ((𝐴 ⊆ {𝐶} ∧ ¬ {𝐶} ⊆ 𝐴) ↔ ((𝐴 = ∅ ∨ 𝐴 = {𝐶}) ∧ ¬ {𝐶} ⊆ 𝐴))) |
49 | | andir 1009 |
. . . . . . . . 9
⊢ (((𝐴 = ∅ ∨ 𝐴 = {𝐶}) ∧ ¬ {𝐶} ⊆ 𝐴) ↔ ((𝐴 = ∅ ∧ ¬ {𝐶} ⊆ 𝐴) ∨ (𝐴 = {𝐶} ∧ ¬ {𝐶} ⊆ 𝐴))) |
50 | | n0i 4248 |
. . . . . . . . . . . . 13
⊢ (𝐶 ∈ 𝐴 → ¬ 𝐴 = ∅) |
51 | 7, 50 | syl6bir 257 |
. . . . . . . . . . . 12
⊢ (𝐶 ∈ V → ({𝐶} ⊆ 𝐴 → ¬ 𝐴 = ∅)) |
52 | 51 | con2d 136 |
. . . . . . . . . . 11
⊢ (𝐶 ∈ V → (𝐴 = ∅ → ¬ {𝐶} ⊆ 𝐴)) |
53 | 52 | pm4.71d 565 |
. . . . . . . . . 10
⊢ (𝐶 ∈ V → (𝐴 = ∅ ↔ (𝐴 = ∅ ∧ ¬ {𝐶} ⊆ 𝐴))) |
54 | | eqimss2 3958 |
. . . . . . . . . . . 12
⊢ (𝐴 = {𝐶} → {𝐶} ⊆ 𝐴) |
55 | | iman 405 |
. . . . . . . . . . . 12
⊢ ((𝐴 = {𝐶} → {𝐶} ⊆ 𝐴) ↔ ¬ (𝐴 = {𝐶} ∧ ¬ {𝐶} ⊆ 𝐴)) |
56 | 54, 55 | mpbi 233 |
. . . . . . . . . . 11
⊢ ¬
(𝐴 = {𝐶} ∧ ¬ {𝐶} ⊆ 𝐴) |
57 | 56 | biorfi 939 |
. . . . . . . . . 10
⊢ ((𝐴 = ∅ ∧ ¬ {𝐶} ⊆ 𝐴) ↔ ((𝐴 = ∅ ∧ ¬ {𝐶} ⊆ 𝐴) ∨ (𝐴 = {𝐶} ∧ ¬ {𝐶} ⊆ 𝐴))) |
58 | 53, 57 | bitr2di 291 |
. . . . . . . . 9
⊢ (𝐶 ∈ V → (((𝐴 = ∅ ∧ ¬ {𝐶} ⊆ 𝐴) ∨ (𝐴 = {𝐶} ∧ ¬ {𝐶} ⊆ 𝐴)) ↔ 𝐴 = ∅)) |
59 | 49, 58 | syl5bb 286 |
. . . . . . . 8
⊢ (𝐶 ∈ V → (((𝐴 = ∅ ∨ 𝐴 = {𝐶}) ∧ ¬ {𝐶} ⊆ 𝐴) ↔ 𝐴 = ∅)) |
60 | 48, 59 | bitrd 282 |
. . . . . . 7
⊢ (𝐶 ∈ V → ((𝐴 ⊆ {𝐶} ∧ ¬ {𝐶} ⊆ 𝐴) ↔ 𝐴 = ∅)) |
61 | 20 | bicomi 227 |
. . . . . . . 8
⊢ ((𝐵 ⊆ {𝐶} ∧ {𝐶} ⊆ 𝐵) ↔ 𝐵 = {𝐶}) |
62 | 61 | a1i 11 |
. . . . . . 7
⊢ (𝐶 ∈ V → ((𝐵 ⊆ {𝐶} ∧ {𝐶} ⊆ 𝐵) ↔ 𝐵 = {𝐶})) |
63 | 60, 62 | anbi12d 634 |
. . . . . 6
⊢ (𝐶 ∈ V → (((𝐴 ⊆ {𝐶} ∧ ¬ {𝐶} ⊆ 𝐴) ∧ (𝐵 ⊆ {𝐶} ∧ {𝐶} ⊆ 𝐵)) ↔ (𝐴 = ∅ ∧ 𝐵 = {𝐶}))) |
64 | 45, 63 | syl5bb 286 |
. . . . 5
⊢ (𝐶 ∈ V → (((𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}) ∧ (¬ {𝐶} ⊆ 𝐴 ∧ {𝐶} ⊆ 𝐵)) ↔ (𝐴 = ∅ ∧ 𝐵 = {𝐶}))) |
65 | 24, 44, 64 | 3orbi123d 1437 |
. . . 4
⊢ (𝐶 ∈ V → ((((𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}) ∧ ({𝐶} ⊆ 𝐴 ∧ {𝐶} ⊆ 𝐵)) ∨ ((𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}) ∧ ({𝐶} ⊆ 𝐴 ∧ ¬ {𝐶} ⊆ 𝐵)) ∨ ((𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}) ∧ (¬ {𝐶} ⊆ 𝐴 ∧ {𝐶} ⊆ 𝐵))) ↔ ((𝐴 = {𝐶} ∧ 𝐵 = {𝐶}) ∨ (𝐴 = {𝐶} ∧ 𝐵 = ∅) ∨ (𝐴 = ∅ ∧ 𝐵 = {𝐶})))) |
66 | 17, 65 | syl5bb 286 |
. . 3
⊢ (𝐶 ∈ V → (((𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}) ∧ ({𝐶} ⊆ 𝐴 ∨ {𝐶} ⊆ 𝐵)) ↔ ((𝐴 = {𝐶} ∧ 𝐵 = {𝐶}) ∨ (𝐴 = {𝐶} ∧ 𝐵 = ∅) ∨ (𝐴 = ∅ ∧ 𝐵 = {𝐶})))) |
67 | 2, 13, 66 | 3bitrd 308 |
. 2
⊢ (𝐶 ∈ V → ((𝐴 ∪ 𝐵) = {𝐶} ↔ ((𝐴 = {𝐶} ∧ 𝐵 = {𝐶}) ∨ (𝐴 = {𝐶} ∧ 𝐵 = ∅) ∨ (𝐴 = ∅ ∧ 𝐵 = {𝐶})))) |
68 | | snprc 4633 |
. . . . 5
⊢ (¬
𝐶 ∈ V ↔ {𝐶} = ∅) |
69 | 68 | biimpi 219 |
. . . 4
⊢ (¬
𝐶 ∈ V → {𝐶} = ∅) |
70 | 69 | eqeq2d 2748 |
. . 3
⊢ (¬
𝐶 ∈ V → ((𝐴 ∪ 𝐵) = {𝐶} ↔ (𝐴 ∪ 𝐵) = ∅)) |
71 | | pm4.25 906 |
. . . . . 6
⊢ ((𝐴 = ∅ ∧ 𝐵 = ∅) ↔ ((𝐴 = ∅ ∧ 𝐵 = ∅) ∨ (𝐴 = ∅ ∧ 𝐵 = ∅))) |
72 | 71 | orbi1i 914 |
. . . . . 6
⊢ (((𝐴 = ∅ ∧ 𝐵 = ∅) ∨ (𝐴 = ∅ ∧ 𝐵 = ∅)) ↔ (((𝐴 = ∅ ∧ 𝐵 = ∅) ∨ (𝐴 = ∅ ∧ 𝐵 = ∅)) ∨ (𝐴 = ∅ ∧ 𝐵 = ∅))) |
73 | 71, 72 | bitri 278 |
. . . . 5
⊢ ((𝐴 = ∅ ∧ 𝐵 = ∅) ↔ (((𝐴 = ∅ ∧ 𝐵 = ∅) ∨ (𝐴 = ∅ ∧ 𝐵 = ∅)) ∨ (𝐴 = ∅ ∧ 𝐵 = ∅))) |
74 | 69 | eqeq2d 2748 |
. . . . . . . 8
⊢ (¬
𝐶 ∈ V → (𝐴 = {𝐶} ↔ 𝐴 = ∅)) |
75 | 69 | eqeq2d 2748 |
. . . . . . . 8
⊢ (¬
𝐶 ∈ V → (𝐵 = {𝐶} ↔ 𝐵 = ∅)) |
76 | 74, 75 | anbi12d 634 |
. . . . . . 7
⊢ (¬
𝐶 ∈ V → ((𝐴 = {𝐶} ∧ 𝐵 = {𝐶}) ↔ (𝐴 = ∅ ∧ 𝐵 = ∅))) |
77 | 74 | anbi1d 633 |
. . . . . . 7
⊢ (¬
𝐶 ∈ V → ((𝐴 = {𝐶} ∧ 𝐵 = ∅) ↔ (𝐴 = ∅ ∧ 𝐵 = ∅))) |
78 | 76, 77 | orbi12d 919 |
. . . . . 6
⊢ (¬
𝐶 ∈ V → (((𝐴 = {𝐶} ∧ 𝐵 = {𝐶}) ∨ (𝐴 = {𝐶} ∧ 𝐵 = ∅)) ↔ ((𝐴 = ∅ ∧ 𝐵 = ∅) ∨ (𝐴 = ∅ ∧ 𝐵 = ∅)))) |
79 | 75 | anbi2d 632 |
. . . . . 6
⊢ (¬
𝐶 ∈ V → ((𝐴 = ∅ ∧ 𝐵 = {𝐶}) ↔ (𝐴 = ∅ ∧ 𝐵 = ∅))) |
80 | 78, 79 | orbi12d 919 |
. . . . 5
⊢ (¬
𝐶 ∈ V → ((((𝐴 = {𝐶} ∧ 𝐵 = {𝐶}) ∨ (𝐴 = {𝐶} ∧ 𝐵 = ∅)) ∨ (𝐴 = ∅ ∧ 𝐵 = {𝐶})) ↔ (((𝐴 = ∅ ∧ 𝐵 = ∅) ∨ (𝐴 = ∅ ∧ 𝐵 = ∅)) ∨ (𝐴 = ∅ ∧ 𝐵 = ∅)))) |
81 | 73, 80 | bitr4id 293 |
. . . 4
⊢ (¬
𝐶 ∈ V → ((𝐴 = ∅ ∧ 𝐵 = ∅) ↔ (((𝐴 = {𝐶} ∧ 𝐵 = {𝐶}) ∨ (𝐴 = {𝐶} ∧ 𝐵 = ∅)) ∨ (𝐴 = ∅ ∧ 𝐵 = {𝐶})))) |
82 | | un00 4357 |
. . . . 5
⊢ ((𝐴 = ∅ ∧ 𝐵 = ∅) ↔ (𝐴 ∪ 𝐵) = ∅) |
83 | 82 | bicomi 227 |
. . . 4
⊢ ((𝐴 ∪ 𝐵) = ∅ ↔ (𝐴 = ∅ ∧ 𝐵 = ∅)) |
84 | | df-3or 1090 |
. . . 4
⊢ (((𝐴 = {𝐶} ∧ 𝐵 = {𝐶}) ∨ (𝐴 = {𝐶} ∧ 𝐵 = ∅) ∨ (𝐴 = ∅ ∧ 𝐵 = {𝐶})) ↔ (((𝐴 = {𝐶} ∧ 𝐵 = {𝐶}) ∨ (𝐴 = {𝐶} ∧ 𝐵 = ∅)) ∨ (𝐴 = ∅ ∧ 𝐵 = {𝐶}))) |
85 | 81, 83, 84 | 3bitr4g 317 |
. . 3
⊢ (¬
𝐶 ∈ V → ((𝐴 ∪ 𝐵) = ∅ ↔ ((𝐴 = {𝐶} ∧ 𝐵 = {𝐶}) ∨ (𝐴 = {𝐶} ∧ 𝐵 = ∅) ∨ (𝐴 = ∅ ∧ 𝐵 = {𝐶})))) |
86 | 70, 85 | bitrd 282 |
. 2
⊢ (¬
𝐶 ∈ V → ((𝐴 ∪ 𝐵) = {𝐶} ↔ ((𝐴 = {𝐶} ∧ 𝐵 = {𝐶}) ∨ (𝐴 = {𝐶} ∧ 𝐵 = ∅) ∨ (𝐴 = ∅ ∧ 𝐵 = {𝐶})))) |
87 | 67, 86 | pm2.61i 185 |
1
⊢ ((𝐴 ∪ 𝐵) = {𝐶} ↔ ((𝐴 = {𝐶} ∧ 𝐵 = {𝐶}) ∨ (𝐴 = {𝐶} ∧ 𝐵 = ∅) ∨ (𝐴 = ∅ ∧ 𝐵 = {𝐶}))) |