Metamath Proof Explorer

Theorem uneqsn

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)

Ref Expression
Assertion uneqsn ( ( 𝐴 ∪ 𝐵 ) = { 𝐶 } ↔ ( ( 𝐴 = { 𝐶 } ∧ 𝐵 = { 𝐶 } ) ∨ ( 𝐴 = { 𝐶 } ∧ 𝐵 = ∅ ) ∨ ( 𝐴 = ∅ ∧ 𝐵 = { 𝐶 } ) ) )

Proof

Step Hyp Ref Expression
1 eqss ⊢ ( ( 𝐴 ∪ 𝐵 ) = { 𝐶 } ↔ ( ( 𝐴 ∪ 𝐵 ) ⊆ { 𝐶 } ∧ { 𝐶 } ⊆ ( 𝐴 ∪ 𝐵 ) ) )
2 1 a1i ⊢ ( 𝐶 ∈ V → ( ( 𝐴 ∪ 𝐵 ) = { 𝐶 } ↔ ( ( 𝐴 ∪ 𝐵 ) ⊆ { 𝐶 } ∧ { 𝐶 } ⊆ ( 𝐴 ∪ 𝐵 ) ) ) )
3 unss ⊢ ( ( 𝐴 ⊆ { 𝐶 } ∧ 𝐵 ⊆ { 𝐶 } ) ↔ ( 𝐴 ∪ 𝐵 ) ⊆ { 𝐶 } )
4 3 bicomi ⊢ ( ( 𝐴 ∪ 𝐵 ) ⊆ { 𝐶 } ↔ ( 𝐴 ⊆ { 𝐶 } ∧ 𝐵 ⊆ { 𝐶 } ) )
5 4 a1i ⊢ ( 𝐶 ∈ V → ( ( 𝐴 ∪ 𝐵 ) ⊆ { 𝐶 } ↔ ( 𝐴 ⊆ { 𝐶 } ∧ 𝐵 ⊆ { 𝐶 } ) ) )
6 elun ⊢ ( 𝐶 ∈ ( 𝐴 ∪ 𝐵 ) ↔ ( 𝐶 ∈ 𝐴 ∨ 𝐶 ∈ 𝐵 ) )
7 snssg ⊢ ( 𝐶 ∈ V → ( 𝐶 ∈ 𝐴 ↔ { 𝐶 } ⊆ 𝐴 ) )
8 snssg ⊢ ( 𝐶 ∈ V → ( 𝐶 ∈ 𝐵 ↔ { 𝐶 } ⊆ 𝐵 ) )
9 7 8 orbi12d ⊢ ( 𝐶 ∈ V → ( ( 𝐶 ∈ 𝐴 ∨ 𝐶 ∈ 𝐵 ) ↔ ( { 𝐶 } ⊆ 𝐴 ∨ { 𝐶 } ⊆ 𝐵 ) ) )
10 6 9 bitr2id ⊢ ( 𝐶 ∈ V → ( ( { 𝐶 } ⊆ 𝐴 ∨ { 𝐶 } ⊆ 𝐵 ) ↔ 𝐶 ∈ ( 𝐴 ∪ 𝐵 ) ) )
11 snssg ⊢ ( 𝐶 ∈ V → ( 𝐶 ∈ ( 𝐴 ∪ 𝐵 ) ↔ { 𝐶 } ⊆ ( 𝐴 ∪ 𝐵 ) ) )
12 10 11 bitr2d ⊢ ( 𝐶 ∈ V → ( { 𝐶 } ⊆ ( 𝐴 ∪ 𝐵 ) ↔ ( { 𝐶 } ⊆ 𝐴 ∨ { 𝐶 } ⊆ 𝐵 ) ) )
13 5 12 anbi12d ⊢ ( 𝐶 ∈ V → ( ( ( 𝐴 ∪ 𝐵 ) ⊆ { 𝐶 } ∧ { 𝐶 } ⊆ ( 𝐴 ∪ 𝐵 ) ) ↔ ( ( 𝐴 ⊆ { 𝐶 } ∧ 𝐵 ⊆ { 𝐶 } ) ∧ ( { 𝐶 } ⊆ 𝐴 ∨ { 𝐶 } ⊆ 𝐵 ) ) ) )
14 or3or ⊢ ( ( { 𝐶 } ⊆ 𝐴 ∨ { 𝐶 } ⊆ 𝐵 ) ↔ ( ( { 𝐶 } ⊆ 𝐴 ∧ { 𝐶 } ⊆ 𝐵 ) ∨ ( { 𝐶 } ⊆ 𝐴 ∧ ¬ { 𝐶 } ⊆ 𝐵 ) ∨ ( ¬ { 𝐶 } ⊆ 𝐴 ∧ { 𝐶 } ⊆ 𝐵 ) ) )
15 14 anbi2i ⊢ ( ( ( 𝐴 ⊆ { 𝐶 } ∧ 𝐵 ⊆ { 𝐶 } ) ∧ ( { 𝐶 } ⊆ 𝐴 ∨ { 𝐶 } ⊆ 𝐵 ) ) ↔ ( ( 𝐴 ⊆ { 𝐶 } ∧ 𝐵 ⊆ { 𝐶 } ) ∧ ( ( { 𝐶 } ⊆ 𝐴 ∧ { 𝐶 } ⊆ 𝐵 ) ∨ ( { 𝐶 } ⊆ 𝐴 ∧ ¬ { 𝐶 } ⊆ 𝐵 ) ∨ ( ¬ { 𝐶 } ⊆ 𝐴 ∧ { 𝐶 } ⊆ 𝐵 ) ) ) )
16 andi3or ⊢ ( ( ( 𝐴 ⊆ { 𝐶 } ∧ 𝐵 ⊆ { 𝐶 } ) ∧ ( ( { 𝐶 } ⊆ 𝐴 ∧ { 𝐶 } ⊆ 𝐵 ) ∨ ( { 𝐶 } ⊆ 𝐴 ∧ ¬ { 𝐶 } ⊆ 𝐵 ) ∨ ( ¬ { 𝐶 } ⊆ 𝐴 ∧ { 𝐶 } ⊆ 𝐵 ) ) ) ↔ ( ( ( 𝐴 ⊆ { 𝐶 } ∧ 𝐵 ⊆ { 𝐶 } ) ∧ ( { 𝐶 } ⊆ 𝐴 ∧ { 𝐶 } ⊆ 𝐵 ) ) ∨ ( ( 𝐴 ⊆ { 𝐶 } ∧ 𝐵 ⊆ { 𝐶 } ) ∧ ( { 𝐶 } ⊆ 𝐴 ∧ ¬ { 𝐶 } ⊆ 𝐵 ) ) ∨ ( ( 𝐴 ⊆ { 𝐶 } ∧ 𝐵 ⊆ { 𝐶 } ) ∧ ( ¬ { 𝐶 } ⊆ 𝐴 ∧ { 𝐶 } ⊆ 𝐵 ) ) ) )
17 15 16 bitri ⊢ ( ( ( 𝐴 ⊆ { 𝐶 } ∧ 𝐵 ⊆ { 𝐶 } ) ∧ ( { 𝐶 } ⊆ 𝐴 ∨ { 𝐶 } ⊆ 𝐵 ) ) ↔ ( ( ( 𝐴 ⊆ { 𝐶 } ∧ 𝐵 ⊆ { 𝐶 } ) ∧ ( { 𝐶 } ⊆ 𝐴 ∧ { 𝐶 } ⊆ 𝐵 ) ) ∨ ( ( 𝐴 ⊆ { 𝐶 } ∧ 𝐵 ⊆ { 𝐶 } ) ∧ ( { 𝐶 } ⊆ 𝐴 ∧ ¬ { 𝐶 } ⊆ 𝐵 ) ) ∨ ( ( 𝐴 ⊆ { 𝐶 } ∧ 𝐵 ⊆ { 𝐶 } ) ∧ ( ¬ { 𝐶 } ⊆ 𝐴 ∧ { 𝐶 } ⊆ 𝐵 ) ) ) )
18 an4 ⊢ ( ( ( 𝐴 ⊆ { 𝐶 } ∧ 𝐵 ⊆ { 𝐶 } ) ∧ ( { 𝐶 } ⊆ 𝐴 ∧ { 𝐶 } ⊆ 𝐵 ) ) ↔ ( ( 𝐴 ⊆ { 𝐶 } ∧ { 𝐶 } ⊆ 𝐴 ) ∧ ( 𝐵 ⊆ { 𝐶 } ∧ { 𝐶 } ⊆ 𝐵 ) ) )
19 eqss ⊢ ( 𝐴 = { 𝐶 } ↔ ( 𝐴 ⊆ { 𝐶 } ∧ { 𝐶 } ⊆ 𝐴 ) )
20 eqss ⊢ ( 𝐵 = { 𝐶 } ↔ ( 𝐵 ⊆ { 𝐶 } ∧ { 𝐶 } ⊆ 𝐵 ) )
21 19 20 anbi12i ⊢ ( ( 𝐴 = { 𝐶 } ∧ 𝐵 = { 𝐶 } ) ↔ ( ( 𝐴 ⊆ { 𝐶 } ∧ { 𝐶 } ⊆ 𝐴 ) ∧ ( 𝐵 ⊆ { 𝐶 } ∧ { 𝐶 } ⊆ 𝐵 ) ) )
22 21 bicomi ⊢ ( ( ( 𝐴 ⊆ { 𝐶 } ∧ { 𝐶 } ⊆ 𝐴 ) ∧ ( 𝐵 ⊆ { 𝐶 } ∧ { 𝐶 } ⊆ 𝐵 ) ) ↔ ( 𝐴 = { 𝐶 } ∧ 𝐵 = { 𝐶 } ) )
23 18 22 bitri ⊢ ( ( ( 𝐴 ⊆ { 𝐶 } ∧ 𝐵 ⊆ { 𝐶 } ) ∧ ( { 𝐶 } ⊆ 𝐴 ∧ { 𝐶 } ⊆ 𝐵 ) ) ↔ ( 𝐴 = { 𝐶 } ∧ 𝐵 = { 𝐶 } ) )
24 23 a1i ⊢ ( 𝐶 ∈ V → ( ( ( 𝐴 ⊆ { 𝐶 } ∧ 𝐵 ⊆ { 𝐶 } ) ∧ ( { 𝐶 } ⊆ 𝐴 ∧ { 𝐶 } ⊆ 𝐵 ) ) ↔ ( 𝐴 = { 𝐶 } ∧ 𝐵 = { 𝐶 } ) ) )
25 an4 ⊢ ( ( ( 𝐴 ⊆ { 𝐶 } ∧ 𝐵 ⊆ { 𝐶 } ) ∧ ( { 𝐶 } ⊆ 𝐴 ∧ ¬ { 𝐶 } ⊆ 𝐵 ) ) ↔ ( ( 𝐴 ⊆ { 𝐶 } ∧ { 𝐶 } ⊆ 𝐴 ) ∧ ( 𝐵 ⊆ { 𝐶 } ∧ ¬ { 𝐶 } ⊆ 𝐵 ) ) )
26 19 bicomi ⊢ ( ( 𝐴 ⊆ { 𝐶 } ∧ { 𝐶 } ⊆ 𝐴 ) ↔ 𝐴 = { 𝐶 } )
27 26 a1i ⊢ ( 𝐶 ∈ V → ( ( 𝐴 ⊆ { 𝐶 } ∧ { 𝐶 } ⊆ 𝐴 ) ↔ 𝐴 = { 𝐶 } ) )
28 sssn ⊢ ( 𝐵 ⊆ { 𝐶 } ↔ ( 𝐵 = ∅ ∨ 𝐵 = { 𝐶 } ) )
29 28 a1i ⊢ ( 𝐶 ∈ V → ( 𝐵 ⊆ { 𝐶 } ↔ ( 𝐵 = ∅ ∨ 𝐵 = { 𝐶 } ) ) )
30 29 anbi1d ⊢ ( 𝐶 ∈ V → ( ( 𝐵 ⊆ { 𝐶 } ∧ ¬ { 𝐶 } ⊆ 𝐵 ) ↔ ( ( 𝐵 = ∅ ∨ 𝐵 = { 𝐶 } ) ∧ ¬ { 𝐶 } ⊆ 𝐵 ) ) )
31 andir ⊢ ( ( ( 𝐵 = ∅ ∨ 𝐵 = { 𝐶 } ) ∧ ¬ { 𝐶 } ⊆ 𝐵 ) ↔ ( ( 𝐵 = ∅ ∧ ¬ { 𝐶 } ⊆ 𝐵 ) ∨ ( 𝐵 = { 𝐶 } ∧ ¬ { 𝐶 } ⊆ 𝐵 ) ) )
32 n0i ⊢ ( 𝐶 ∈ 𝐵 → ¬ 𝐵 = ∅ )
33 8 32 biimtrrdi ⊢ ( 𝐶 ∈ V → ( { 𝐶 } ⊆ 𝐵 → ¬ 𝐵 = ∅ ) )
34 33 con2d ⊢ ( 𝐶 ∈ V → ( 𝐵 = ∅ → ¬ { 𝐶 } ⊆ 𝐵 ) )
35 34 pm4.71d ⊢ ( 𝐶 ∈ V → ( 𝐵 = ∅ ↔ ( 𝐵 = ∅ ∧ ¬ { 𝐶 } ⊆ 𝐵 ) ) )
36 eqimss2 ⊢ ( 𝐵 = { 𝐶 } → { 𝐶 } ⊆ 𝐵 )
37 iman ⊢ ( ( 𝐵 = { 𝐶 } → { 𝐶 } ⊆ 𝐵 ) ↔ ¬ ( 𝐵 = { 𝐶 } ∧ ¬ { 𝐶 } ⊆ 𝐵 ) )
38 36 37 mpbi ⊢ ¬ ( 𝐵 = { 𝐶 } ∧ ¬ { 𝐶 } ⊆ 𝐵 )
39 38 biorfri ⊢ ( ( 𝐵 = ∅ ∧ ¬ { 𝐶 } ⊆ 𝐵 ) ↔ ( ( 𝐵 = ∅ ∧ ¬ { 𝐶 } ⊆ 𝐵 ) ∨ ( 𝐵 = { 𝐶 } ∧ ¬ { 𝐶 } ⊆ 𝐵 ) ) )
40 35 39 bitr2di ⊢ ( 𝐶 ∈ V → ( ( ( 𝐵 = ∅ ∧ ¬ { 𝐶 } ⊆ 𝐵 ) ∨ ( 𝐵 = { 𝐶 } ∧ ¬ { 𝐶 } ⊆ 𝐵 ) ) ↔ 𝐵 = ∅ ) )
41 31 40 bitrid ⊢ ( 𝐶 ∈ V → ( ( ( 𝐵 = ∅ ∨ 𝐵 = { 𝐶 } ) ∧ ¬ { 𝐶 } ⊆ 𝐵 ) ↔ 𝐵 = ∅ ) )
42 30 41 bitrd ⊢ ( 𝐶 ∈ V → ( ( 𝐵 ⊆ { 𝐶 } ∧ ¬ { 𝐶 } ⊆ 𝐵 ) ↔ 𝐵 = ∅ ) )
43 27 42 anbi12d ⊢ ( 𝐶 ∈ V → ( ( ( 𝐴 ⊆ { 𝐶 } ∧ { 𝐶 } ⊆ 𝐴 ) ∧ ( 𝐵 ⊆ { 𝐶 } ∧ ¬ { 𝐶 } ⊆ 𝐵 ) ) ↔ ( 𝐴 = { 𝐶 } ∧ 𝐵 = ∅ ) ) )
44 25 43 bitrid ⊢ ( 𝐶 ∈ V → ( ( ( 𝐴 ⊆ { 𝐶 } ∧ 𝐵 ⊆ { 𝐶 } ) ∧ ( { 𝐶 } ⊆ 𝐴 ∧ ¬ { 𝐶 } ⊆ 𝐵 ) ) ↔ ( 𝐴 = { 𝐶 } ∧ 𝐵 = ∅ ) ) )
45 an4 ⊢ ( ( ( 𝐴 ⊆ { 𝐶 } ∧ 𝐵 ⊆ { 𝐶 } ) ∧ ( ¬ { 𝐶 } ⊆ 𝐴 ∧ { 𝐶 } ⊆ 𝐵 ) ) ↔ ( ( 𝐴 ⊆ { 𝐶 } ∧ ¬ { 𝐶 } ⊆ 𝐴 ) ∧ ( 𝐵 ⊆ { 𝐶 } ∧ { 𝐶 } ⊆ 𝐵 ) ) )
46 sssn ⊢ ( 𝐴 ⊆ { 𝐶 } ↔ ( 𝐴 = ∅ ∨ 𝐴 = { 𝐶 } ) )
47 46 a1i ⊢ ( 𝐶 ∈ V → ( 𝐴 ⊆ { 𝐶 } ↔ ( 𝐴 = ∅ ∨ 𝐴 = { 𝐶 } ) ) )
48 47 anbi1d ⊢ ( 𝐶 ∈ V → ( ( 𝐴 ⊆ { 𝐶 } ∧ ¬ { 𝐶 } ⊆ 𝐴 ) ↔ ( ( 𝐴 = ∅ ∨ 𝐴 = { 𝐶 } ) ∧ ¬ { 𝐶 } ⊆ 𝐴 ) ) )
49 andir ⊢ ( ( ( 𝐴 = ∅ ∨ 𝐴 = { 𝐶 } ) ∧ ¬ { 𝐶 } ⊆ 𝐴 ) ↔ ( ( 𝐴 = ∅ ∧ ¬ { 𝐶 } ⊆ 𝐴 ) ∨ ( 𝐴 = { 𝐶 } ∧ ¬ { 𝐶 } ⊆ 𝐴 ) ) )
50 n0i ⊢ ( 𝐶 ∈ 𝐴 → ¬ 𝐴 = ∅ )
51 7 50 biimtrrdi ⊢ ( 𝐶 ∈ V → ( { 𝐶 } ⊆ 𝐴 → ¬ 𝐴 = ∅ ) )
52 51 con2d ⊢ ( 𝐶 ∈ V → ( 𝐴 = ∅ → ¬ { 𝐶 } ⊆ 𝐴 ) )
53 52 pm4.71d ⊢ ( 𝐶 ∈ V → ( 𝐴 = ∅ ↔ ( 𝐴 = ∅ ∧ ¬ { 𝐶 } ⊆ 𝐴 ) ) )
54 eqimss2 ⊢ ( 𝐴 = { 𝐶 } → { 𝐶 } ⊆ 𝐴 )
55 iman ⊢ ( ( 𝐴 = { 𝐶 } → { 𝐶 } ⊆ 𝐴 ) ↔ ¬ ( 𝐴 = { 𝐶 } ∧ ¬ { 𝐶 } ⊆ 𝐴 ) )
56 54 55 mpbi ⊢ ¬ ( 𝐴 = { 𝐶 } ∧ ¬ { 𝐶 } ⊆ 𝐴 )
57 56 biorfri ⊢ ( ( 𝐴 = ∅ ∧ ¬ { 𝐶 } ⊆ 𝐴 ) ↔ ( ( 𝐴 = ∅ ∧ ¬ { 𝐶 } ⊆ 𝐴 ) ∨ ( 𝐴 = { 𝐶 } ∧ ¬ { 𝐶 } ⊆ 𝐴 ) ) )
58 53 57 bitr2di ⊢ ( 𝐶 ∈ V → ( ( ( 𝐴 = ∅ ∧ ¬ { 𝐶 } ⊆ 𝐴 ) ∨ ( 𝐴 = { 𝐶 } ∧ ¬ { 𝐶 } ⊆ 𝐴 ) ) ↔ 𝐴 = ∅ ) )
59 49 58 bitrid ⊢ ( 𝐶 ∈ V → ( ( ( 𝐴 = ∅ ∨ 𝐴 = { 𝐶 } ) ∧ ¬ { 𝐶 } ⊆ 𝐴 ) ↔ 𝐴 = ∅ ) )
60 48 59 bitrd ⊢ ( 𝐶 ∈ V → ( ( 𝐴 ⊆ { 𝐶 } ∧ ¬ { 𝐶 } ⊆ 𝐴 ) ↔ 𝐴 = ∅ ) )
61 20 bicomi ⊢ ( ( 𝐵 ⊆ { 𝐶 } ∧ { 𝐶 } ⊆ 𝐵 ) ↔ 𝐵 = { 𝐶 } )
62 61 a1i ⊢ ( 𝐶 ∈ V → ( ( 𝐵 ⊆ { 𝐶 } ∧ { 𝐶 } ⊆ 𝐵 ) ↔ 𝐵 = { 𝐶 } ) )
63 60 62 anbi12d ⊢ ( 𝐶 ∈ V → ( ( ( 𝐴 ⊆ { 𝐶 } ∧ ¬ { 𝐶 } ⊆ 𝐴 ) ∧ ( 𝐵 ⊆ { 𝐶 } ∧ { 𝐶 } ⊆ 𝐵 ) ) ↔ ( 𝐴 = ∅ ∧ 𝐵 = { 𝐶 } ) ) )
64 45 63 bitrid ⊢ ( 𝐶 ∈ V → ( ( ( 𝐴 ⊆ { 𝐶 } ∧ 𝐵 ⊆ { 𝐶 } ) ∧ ( ¬ { 𝐶 } ⊆ 𝐴 ∧ { 𝐶 } ⊆ 𝐵 ) ) ↔ ( 𝐴 = ∅ ∧ 𝐵 = { 𝐶 } ) ) )
65 24 44 64 3orbi123d ⊢ ( 𝐶 ∈ V → ( ( ( ( 𝐴 ⊆ { 𝐶 } ∧ 𝐵 ⊆ { 𝐶 } ) ∧ ( { 𝐶 } ⊆ 𝐴 ∧ { 𝐶 } ⊆ 𝐵 ) ) ∨ ( ( 𝐴 ⊆ { 𝐶 } ∧ 𝐵 ⊆ { 𝐶 } ) ∧ ( { 𝐶 } ⊆ 𝐴 ∧ ¬ { 𝐶 } ⊆ 𝐵 ) ) ∨ ( ( 𝐴 ⊆ { 𝐶 } ∧ 𝐵 ⊆ { 𝐶 } ) ∧ ( ¬ { 𝐶 } ⊆ 𝐴 ∧ { 𝐶 } ⊆ 𝐵 ) ) ) ↔ ( ( 𝐴 = { 𝐶 } ∧ 𝐵 = { 𝐶 } ) ∨ ( 𝐴 = { 𝐶 } ∧ 𝐵 = ∅ ) ∨ ( 𝐴 = ∅ ∧ 𝐵 = { 𝐶 } ) ) ) )
66 17 65 bitrid ⊢ ( 𝐶 ∈ V → ( ( ( 𝐴 ⊆ { 𝐶 } ∧ 𝐵 ⊆ { 𝐶 } ) ∧ ( { 𝐶 } ⊆ 𝐴 ∨ { 𝐶 } ⊆ 𝐵 ) ) ↔ ( ( 𝐴 = { 𝐶 } ∧ 𝐵 = { 𝐶 } ) ∨ ( 𝐴 = { 𝐶 } ∧ 𝐵 = ∅ ) ∨ ( 𝐴 = ∅ ∧ 𝐵 = { 𝐶 } ) ) ) )
67 2 13 66 3bitrd ⊢ ( 𝐶 ∈ V → ( ( 𝐴 ∪ 𝐵 ) = { 𝐶 } ↔ ( ( 𝐴 = { 𝐶 } ∧ 𝐵 = { 𝐶 } ) ∨ ( 𝐴 = { 𝐶 } ∧ 𝐵 = ∅ ) ∨ ( 𝐴 = ∅ ∧ 𝐵 = { 𝐶 } ) ) ) )
68 snprc ⊢ ( ¬ 𝐶 ∈ V ↔ { 𝐶 } = ∅ )
69 68 biimpi ⊢ ( ¬ 𝐶 ∈ V → { 𝐶 } = ∅ )
70 69 eqeq2d ⊢ ( ¬ 𝐶 ∈ V → ( ( 𝐴 ∪ 𝐵 ) = { 𝐶 } ↔ ( 𝐴 ∪ 𝐵 ) = ∅ ) )
71 pm4.25 ⊢ ( ( 𝐴 = ∅ ∧ 𝐵 = ∅ ) ↔ ( ( 𝐴 = ∅ ∧ 𝐵 = ∅ ) ∨ ( 𝐴 = ∅ ∧ 𝐵 = ∅ ) ) )
72 71 orbi1i ⊢ ( ( ( 𝐴 = ∅ ∧ 𝐵 = ∅ ) ∨ ( 𝐴 = ∅ ∧ 𝐵 = ∅ ) ) ↔ ( ( ( 𝐴 = ∅ ∧ 𝐵 = ∅ ) ∨ ( 𝐴 = ∅ ∧ 𝐵 = ∅ ) ) ∨ ( 𝐴 = ∅ ∧ 𝐵 = ∅ ) ) )
73 71 72 bitri ⊢ ( ( 𝐴 = ∅ ∧ 𝐵 = ∅ ) ↔ ( ( ( 𝐴 = ∅ ∧ 𝐵 = ∅ ) ∨ ( 𝐴 = ∅ ∧ 𝐵 = ∅ ) ) ∨ ( 𝐴 = ∅ ∧ 𝐵 = ∅ ) ) )
74 69 eqeq2d ⊢ ( ¬ 𝐶 ∈ V → ( 𝐴 = { 𝐶 } ↔ 𝐴 = ∅ ) )
75 69 eqeq2d ⊢ ( ¬ 𝐶 ∈ V → ( 𝐵 = { 𝐶 } ↔ 𝐵 = ∅ ) )
76 74 75 anbi12d ⊢ ( ¬ 𝐶 ∈ V → ( ( 𝐴 = { 𝐶 } ∧ 𝐵 = { 𝐶 } ) ↔ ( 𝐴 = ∅ ∧ 𝐵 = ∅ ) ) )
77 74 anbi1d ⊢ ( ¬ 𝐶 ∈ V → ( ( 𝐴 = { 𝐶 } ∧ 𝐵 = ∅ ) ↔ ( 𝐴 = ∅ ∧ 𝐵 = ∅ ) ) )
78 76 77 orbi12d ⊢ ( ¬ 𝐶 ∈ V → ( ( ( 𝐴 = { 𝐶 } ∧ 𝐵 = { 𝐶 } ) ∨ ( 𝐴 = { 𝐶 } ∧ 𝐵 = ∅ ) ) ↔ ( ( 𝐴 = ∅ ∧ 𝐵 = ∅ ) ∨ ( 𝐴 = ∅ ∧ 𝐵 = ∅ ) ) ) )
79 75 anbi2d ⊢ ( ¬ 𝐶 ∈ V → ( ( 𝐴 = ∅ ∧ 𝐵 = { 𝐶 } ) ↔ ( 𝐴 = ∅ ∧ 𝐵 = ∅ ) ) )
80 78 79 orbi12d ⊢ ( ¬ 𝐶 ∈ V → ( ( ( ( 𝐴 = { 𝐶 } ∧ 𝐵 = { 𝐶 } ) ∨ ( 𝐴 = { 𝐶 } ∧ 𝐵 = ∅ ) ) ∨ ( 𝐴 = ∅ ∧ 𝐵 = { 𝐶 } ) ) ↔ ( ( ( 𝐴 = ∅ ∧ 𝐵 = ∅ ) ∨ ( 𝐴 = ∅ ∧ 𝐵 = ∅ ) ) ∨ ( 𝐴 = ∅ ∧ 𝐵 = ∅ ) ) ) )
81 73 80 bitr4id ⊢ ( ¬ 𝐶 ∈ V → ( ( 𝐴 = ∅ ∧ 𝐵 = ∅ ) ↔ ( ( ( 𝐴 = { 𝐶 } ∧ 𝐵 = { 𝐶 } ) ∨ ( 𝐴 = { 𝐶 } ∧ 𝐵 = ∅ ) ) ∨ ( 𝐴 = ∅ ∧ 𝐵 = { 𝐶 } ) ) ) )
82 un00 ⊢ ( ( 𝐴 = ∅ ∧ 𝐵 = ∅ ) ↔ ( 𝐴 ∪ 𝐵 ) = ∅ )
83 82 bicomi ⊢ ( ( 𝐴 ∪ 𝐵 ) = ∅ ↔ ( 𝐴 = ∅ ∧ 𝐵 = ∅ ) )
84 df-3or ⊢ ( ( ( 𝐴 = { 𝐶 } ∧ 𝐵 = { 𝐶 } ) ∨ ( 𝐴 = { 𝐶 } ∧ 𝐵 = ∅ ) ∨ ( 𝐴 = ∅ ∧ 𝐵 = { 𝐶 } ) ) ↔ ( ( ( 𝐴 = { 𝐶 } ∧ 𝐵 = { 𝐶 } ) ∨ ( 𝐴 = { 𝐶 } ∧ 𝐵 = ∅ ) ) ∨ ( 𝐴 = ∅ ∧ 𝐵 = { 𝐶 } ) ) )
85 81 83 84 3bitr4g ⊢ ( ¬ 𝐶 ∈ V → ( ( 𝐴 ∪ 𝐵 ) = ∅ ↔ ( ( 𝐴 = { 𝐶 } ∧ 𝐵 = { 𝐶 } ) ∨ ( 𝐴 = { 𝐶 } ∧ 𝐵 = ∅ ) ∨ ( 𝐴 = ∅ ∧ 𝐵 = { 𝐶 } ) ) ) )
86 70 85 bitrd ⊢ ( ¬ 𝐶 ∈ V → ( ( 𝐴 ∪ 𝐵 ) = { 𝐶 } ↔ ( ( 𝐴 = { 𝐶 } ∧ 𝐵 = { 𝐶 } ) ∨ ( 𝐴 = { 𝐶 } ∧ 𝐵 = ∅ ) ∨ ( 𝐴 = ∅ ∧ 𝐵 = { 𝐶 } ) ) ) )
87 67 86 pm2.61i ⊢ ( ( 𝐴 ∪ 𝐵 ) = { 𝐶 } ↔ ( ( 𝐴 = { 𝐶 } ∧ 𝐵 = { 𝐶 } ) ∨ ( 𝐴 = { 𝐶 } ∧ 𝐵 = ∅ ) ∨ ( 𝐴 = ∅ ∧ 𝐵 = { 𝐶 } ) ) )