Theorem uneqsn 41633

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

Step	Hyp	Ref	Expression
1		eqss 3936	. . . 4 ⊢ ((𝐴 ∪ 𝐵) = {𝐶} ↔ ((𝐴 ∪ 𝐵) ⊆ {𝐶} ∧ {𝐶} ⊆ (𝐴 ∪ 𝐵)))
2	1	a1i 11	. . 3 ⊢ (𝐶 ∈ V → ((𝐴 ∪ 𝐵) = {𝐶} ↔ ((𝐴 ∪ 𝐵) ⊆ {𝐶} ∧ {𝐶} ⊆ (𝐴 ∪ 𝐵))))
3		unss 4118	. . . . . 6 ⊢ ((𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}) ↔ (𝐴 ∪ 𝐵) ⊆ {𝐶})
4	3	bicomi 223	. . . . 5 ⊢ ((𝐴 ∪ 𝐵) ⊆ {𝐶} ↔ (𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}))
5	4	a1i 11	. . . 4 ⊢ (𝐶 ∈ V → ((𝐴 ∪ 𝐵) ⊆ {𝐶} ↔ (𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶})))
6		elun 4083	. . . . . 6 ⊢ (𝐶 ∈ (𝐴 ∪ 𝐵) ↔ (𝐶 ∈ 𝐴 ∨ 𝐶 ∈ 𝐵))
7		snssg 4718	. . . . . . 7 ⊢ (𝐶 ∈ V → (𝐶 ∈ 𝐴 ↔ {𝐶} ⊆ 𝐴))
8		snssg 4718	. . . . . . 7 ⊢ (𝐶 ∈ V → (𝐶 ∈ 𝐵 ↔ {𝐶} ⊆ 𝐵))
9	7, 8	orbi12d 916	. . . . . 6 ⊢ (𝐶 ∈ V → ((𝐶 ∈ 𝐴 ∨ 𝐶 ∈ 𝐵) ↔ ({𝐶} ⊆ 𝐴 ∨ {𝐶} ⊆ 𝐵)))
10	6, 9	bitr2id 284	. . . . 5 ⊢ (𝐶 ∈ V → (({𝐶} ⊆ 𝐴 ∨ {𝐶} ⊆ 𝐵) ↔ 𝐶 ∈ (𝐴 ∪ 𝐵)))
11		snssg 4718	. . . . 5 ⊢ (𝐶 ∈ V → (𝐶 ∈ (𝐴 ∪ 𝐵) ↔ {𝐶} ⊆ (𝐴 ∪ 𝐵)))
12	10, 11	bitr2d 279	. . . 4 ⊢ (𝐶 ∈ V → ({𝐶} ⊆ (𝐴 ∪ 𝐵) ↔ ({𝐶} ⊆ 𝐴 ∨ {𝐶} ⊆ 𝐵)))
13	5, 12	anbi12d 631	. . 3 ⊢ (𝐶 ∈ V → (((𝐴 ∪ 𝐵) ⊆ {𝐶} ∧ {𝐶} ⊆ (𝐴 ∪ 𝐵)) ↔ ((𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}) ∧ ({𝐶} ⊆ 𝐴 ∨ {𝐶} ⊆ 𝐵))))
14		or3or 41631	. . . . . 6 ⊢ (({𝐶} ⊆ 𝐴 ∨ {𝐶} ⊆ 𝐵) ↔ (({𝐶} ⊆ 𝐴 ∧ {𝐶} ⊆ 𝐵) ∨ ({𝐶} ⊆ 𝐴 ∧ ¬ {𝐶} ⊆ 𝐵) ∨ (¬ {𝐶} ⊆ 𝐴 ∧ {𝐶} ⊆ 𝐵)))
15	14	anbi2i 623	. . . . 5 ⊢ (((𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}) ∧ ({𝐶} ⊆ 𝐴 ∨ {𝐶} ⊆ 𝐵)) ↔ ((𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}) ∧ (({𝐶} ⊆ 𝐴 ∧ {𝐶} ⊆ 𝐵) ∨ ({𝐶} ⊆ 𝐴 ∧ ¬ {𝐶} ⊆ 𝐵) ∨ (¬ {𝐶} ⊆ 𝐴 ∧ {𝐶} ⊆ 𝐵))))
16		andi3or 41632	. . . . 5 ⊢ (((𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}) ∧ (({𝐶} ⊆ 𝐴 ∧ {𝐶} ⊆ 𝐵) ∨ ({𝐶} ⊆ 𝐴 ∧ ¬ {𝐶} ⊆ 𝐵) ∨ (¬ {𝐶} ⊆ 𝐴 ∧ {𝐶} ⊆ 𝐵))) ↔ (((𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}) ∧ ({𝐶} ⊆ 𝐴 ∧ {𝐶} ⊆ 𝐵)) ∨ ((𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}) ∧ ({𝐶} ⊆ 𝐴 ∧ ¬ {𝐶} ⊆ 𝐵)) ∨ ((𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}) ∧ (¬ {𝐶} ⊆ 𝐴 ∧ {𝐶} ⊆ 𝐵))))
17	15, 16	bitri 274	. . . 4 ⊢ (((𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}) ∧ ({𝐶} ⊆ 𝐴 ∨ {𝐶} ⊆ 𝐵)) ↔ (((𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}) ∧ ({𝐶} ⊆ 𝐴 ∧ {𝐶} ⊆ 𝐵)) ∨ ((𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}) ∧ ({𝐶} ⊆ 𝐴 ∧ ¬ {𝐶} ⊆ 𝐵)) ∨ ((𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}) ∧ (¬ {𝐶} ⊆ 𝐴 ∧ {𝐶} ⊆ 𝐵))))
18		an4 653	. . . . . . 7 ⊢ (((𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}) ∧ ({𝐶} ⊆ 𝐴 ∧ {𝐶} ⊆ 𝐵)) ↔ ((𝐴 ⊆ {𝐶} ∧ {𝐶} ⊆ 𝐴) ∧ (𝐵 ⊆ {𝐶} ∧ {𝐶} ⊆ 𝐵)))
19		eqss 3936	. . . . . . . . 9 ⊢ (𝐴 = {𝐶} ↔ (𝐴 ⊆ {𝐶} ∧ {𝐶} ⊆ 𝐴))
20		eqss 3936	. . . . . . . . 9 ⊢ (𝐵 = {𝐶} ↔ (𝐵 ⊆ {𝐶} ∧ {𝐶} ⊆ 𝐵))
21	19, 20	anbi12i 627	. . . . . . . 8 ⊢ ((𝐴 = {𝐶} ∧ 𝐵 = {𝐶}) ↔ ((𝐴 ⊆ {𝐶} ∧ {𝐶} ⊆ 𝐴) ∧ (𝐵 ⊆ {𝐶} ∧ {𝐶} ⊆ 𝐵)))
22	21	bicomi 223	. . . . . . 7 ⊢ (((𝐴 ⊆ {𝐶} ∧ {𝐶} ⊆ 𝐴) ∧ (𝐵 ⊆ {𝐶} ∧ {𝐶} ⊆ 𝐵)) ↔ (𝐴 = {𝐶} ∧ 𝐵 = {𝐶}))
23	18, 22	bitri 274	. . . . . 6 ⊢ (((𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}) ∧ ({𝐶} ⊆ 𝐴 ∧ {𝐶} ⊆ 𝐵)) ↔ (𝐴 = {𝐶} ∧ 𝐵 = {𝐶}))
24	23	a1i 11	. . . . 5 ⊢ (𝐶 ∈ V → (((𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}) ∧ ({𝐶} ⊆ 𝐴 ∧ {𝐶} ⊆ 𝐵)) ↔ (𝐴 = {𝐶} ∧ 𝐵 = {𝐶})))
25		an4 653	. . . . . 6 ⊢ (((𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}) ∧ ({𝐶} ⊆ 𝐴 ∧ ¬ {𝐶} ⊆ 𝐵)) ↔ ((𝐴 ⊆ {𝐶} ∧ {𝐶} ⊆ 𝐴) ∧ (𝐵 ⊆ {𝐶} ∧ ¬ {𝐶} ⊆ 𝐵)))
26	19	bicomi 223	. . . . . . . 8 ⊢ ((𝐴 ⊆ {𝐶} ∧ {𝐶} ⊆ 𝐴) ↔ 𝐴 = {𝐶})
27	26	a1i 11	. . . . . . 7 ⊢ (𝐶 ∈ V → ((𝐴 ⊆ {𝐶} ∧ {𝐶} ⊆ 𝐴) ↔ 𝐴 = {𝐶}))
28		sssn 4759	. . . . . . . . . 10 ⊢ (𝐵 ⊆ {𝐶} ↔ (𝐵 = ∅ ∨ 𝐵 = {𝐶}))
29	28	a1i 11	. . . . . . . . 9 ⊢ (𝐶 ∈ V → (𝐵 ⊆ {𝐶} ↔ (𝐵 = ∅ ∨ 𝐵 = {𝐶})))
30	29	anbi1d 630	. . . . . . . 8 ⊢ (𝐶 ∈ V → ((𝐵 ⊆ {𝐶} ∧ ¬ {𝐶} ⊆ 𝐵) ↔ ((𝐵 = ∅ ∨ 𝐵 = {𝐶}) ∧ ¬ {𝐶} ⊆ 𝐵)))
31		andir 1006	. . . . . . . . 9 ⊢ (((𝐵 = ∅ ∨ 𝐵 = {𝐶}) ∧ ¬ {𝐶} ⊆ 𝐵) ↔ ((𝐵 = ∅ ∧ ¬ {𝐶} ⊆ 𝐵) ∨ (𝐵 = {𝐶} ∧ ¬ {𝐶} ⊆ 𝐵)))
32		n0i 4267	. . . . . . . . . . . . 13 ⊢ (𝐶 ∈ 𝐵 → ¬ 𝐵 = ∅)
33	8, 32	syl6bir 253	. . . . . . . . . . . 12 ⊢ (𝐶 ∈ V → ({𝐶} ⊆ 𝐵 → ¬ 𝐵 = ∅))
34	33	con2d 134	. . . . . . . . . . 11 ⊢ (𝐶 ∈ V → (𝐵 = ∅ → ¬ {𝐶} ⊆ 𝐵))
35	34	pm4.71d 562	. . . . . . . . . 10 ⊢ (𝐶 ∈ V → (𝐵 = ∅ ↔ (𝐵 = ∅ ∧ ¬ {𝐶} ⊆ 𝐵)))
36		eqimss2 3978	. . . . . . . . . . . 12 ⊢ (𝐵 = {𝐶} → {𝐶} ⊆ 𝐵)
37		iman 402	. . . . . . . . . . . 12 ⊢ ((𝐵 = {𝐶} → {𝐶} ⊆ 𝐵) ↔ ¬ (𝐵 = {𝐶} ∧ ¬ {𝐶} ⊆ 𝐵))
38	36, 37	mpbi 229	. . . . . . . . . . 11 ⊢ ¬ (𝐵 = {𝐶} ∧ ¬ {𝐶} ⊆ 𝐵)
39	38	biorfi 936	. . . . . . . . . 10 ⊢ ((𝐵 = ∅ ∧ ¬ {𝐶} ⊆ 𝐵) ↔ ((𝐵 = ∅ ∧ ¬ {𝐶} ⊆ 𝐵) ∨ (𝐵 = {𝐶} ∧ ¬ {𝐶} ⊆ 𝐵)))
40	35, 39	bitr2di 288	. . . . . . . . 9 ⊢ (𝐶 ∈ V → (((𝐵 = ∅ ∧ ¬ {𝐶} ⊆ 𝐵) ∨ (𝐵 = {𝐶} ∧ ¬ {𝐶} ⊆ 𝐵)) ↔ 𝐵 = ∅))
41	31, 40	bitrid 282	. . . . . . . 8 ⊢ (𝐶 ∈ V → (((𝐵 = ∅ ∨ 𝐵 = {𝐶}) ∧ ¬ {𝐶} ⊆ 𝐵) ↔ 𝐵 = ∅))
42	30, 41	bitrd 278	. . . . . . 7 ⊢ (𝐶 ∈ V → ((𝐵 ⊆ {𝐶} ∧ ¬ {𝐶} ⊆ 𝐵) ↔ 𝐵 = ∅))
43	27, 42	anbi12d 631	. . . . . 6 ⊢ (𝐶 ∈ V → (((𝐴 ⊆ {𝐶} ∧ {𝐶} ⊆ 𝐴) ∧ (𝐵 ⊆ {𝐶} ∧ ¬ {𝐶} ⊆ 𝐵)) ↔ (𝐴 = {𝐶} ∧ 𝐵 = ∅)))
44	25, 43	bitrid 282	. . . . 5 ⊢ (𝐶 ∈ V → (((𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}) ∧ ({𝐶} ⊆ 𝐴 ∧ ¬ {𝐶} ⊆ 𝐵)) ↔ (𝐴 = {𝐶} ∧ 𝐵 = ∅)))
45		an4 653	. . . . . 6 ⊢ (((𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}) ∧ (¬ {𝐶} ⊆ 𝐴 ∧ {𝐶} ⊆ 𝐵)) ↔ ((𝐴 ⊆ {𝐶} ∧ ¬ {𝐶} ⊆ 𝐴) ∧ (𝐵 ⊆ {𝐶} ∧ {𝐶} ⊆ 𝐵)))
46		sssn 4759	. . . . . . . . . 10 ⊢ (𝐴 ⊆ {𝐶} ↔ (𝐴 = ∅ ∨ 𝐴 = {𝐶}))
47	46	a1i 11	. . . . . . . . 9 ⊢ (𝐶 ∈ V → (𝐴 ⊆ {𝐶} ↔ (𝐴 = ∅ ∨ 𝐴 = {𝐶})))
48	47	anbi1d 630	. . . . . . . 8 ⊢ (𝐶 ∈ V → ((𝐴 ⊆ {𝐶} ∧ ¬ {𝐶} ⊆ 𝐴) ↔ ((𝐴 = ∅ ∨ 𝐴 = {𝐶}) ∧ ¬ {𝐶} ⊆ 𝐴)))
49		andir 1006	. . . . . . . . 9 ⊢ (((𝐴 = ∅ ∨ 𝐴 = {𝐶}) ∧ ¬ {𝐶} ⊆ 𝐴) ↔ ((𝐴 = ∅ ∧ ¬ {𝐶} ⊆ 𝐴) ∨ (𝐴 = {𝐶} ∧ ¬ {𝐶} ⊆ 𝐴)))
50		n0i 4267	. . . . . . . . . . . . 13 ⊢ (𝐶 ∈ 𝐴 → ¬ 𝐴 = ∅)
51	7, 50	syl6bir 253	. . . . . . . . . . . 12 ⊢ (𝐶 ∈ V → ({𝐶} ⊆ 𝐴 → ¬ 𝐴 = ∅))
52	51	con2d 134	. . . . . . . . . . 11 ⊢ (𝐶 ∈ V → (𝐴 = ∅ → ¬ {𝐶} ⊆ 𝐴))
53	52	pm4.71d 562	. . . . . . . . . 10 ⊢ (𝐶 ∈ V → (𝐴 = ∅ ↔ (𝐴 = ∅ ∧ ¬ {𝐶} ⊆ 𝐴)))
54		eqimss2 3978	. . . . . . . . . . . 12 ⊢ (𝐴 = {𝐶} → {𝐶} ⊆ 𝐴)
55		iman 402	. . . . . . . . . . . 12 ⊢ ((𝐴 = {𝐶} → {𝐶} ⊆ 𝐴) ↔ ¬ (𝐴 = {𝐶} ∧ ¬ {𝐶} ⊆ 𝐴))
56	54, 55	mpbi 229	. . . . . . . . . . 11 ⊢ ¬ (𝐴 = {𝐶} ∧ ¬ {𝐶} ⊆ 𝐴)
57	56	biorfi 936	. . . . . . . . . 10 ⊢ ((𝐴 = ∅ ∧ ¬ {𝐶} ⊆ 𝐴) ↔ ((𝐴 = ∅ ∧ ¬ {𝐶} ⊆ 𝐴) ∨ (𝐴 = {𝐶} ∧ ¬ {𝐶} ⊆ 𝐴)))
58	53, 57	bitr2di 288	. . . . . . . . 9 ⊢ (𝐶 ∈ V → (((𝐴 = ∅ ∧ ¬ {𝐶} ⊆ 𝐴) ∨ (𝐴 = {𝐶} ∧ ¬ {𝐶} ⊆ 𝐴)) ↔ 𝐴 = ∅))
59	49, 58	bitrid 282	. . . . . . . 8 ⊢ (𝐶 ∈ V → (((𝐴 = ∅ ∨ 𝐴 = {𝐶}) ∧ ¬ {𝐶} ⊆ 𝐴) ↔ 𝐴 = ∅))
60	48, 59	bitrd 278	. . . . . . 7 ⊢ (𝐶 ∈ V → ((𝐴 ⊆ {𝐶} ∧ ¬ {𝐶} ⊆ 𝐴) ↔ 𝐴 = ∅))
61	20	bicomi 223	. . . . . . . 8 ⊢ ((𝐵 ⊆ {𝐶} ∧ {𝐶} ⊆ 𝐵) ↔ 𝐵 = {𝐶})
62	61	a1i 11	. . . . . . 7 ⊢ (𝐶 ∈ V → ((𝐵 ⊆ {𝐶} ∧ {𝐶} ⊆ 𝐵) ↔ 𝐵 = {𝐶}))
63	60, 62	anbi12d 631	. . . . . 6 ⊢ (𝐶 ∈ V → (((𝐴 ⊆ {𝐶} ∧ ¬ {𝐶} ⊆ 𝐴) ∧ (𝐵 ⊆ {𝐶} ∧ {𝐶} ⊆ 𝐵)) ↔ (𝐴 = ∅ ∧ 𝐵 = {𝐶})))
64	45, 63	bitrid 282	. . . . 5 ⊢ (𝐶 ∈ V → (((𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}) ∧ (¬ {𝐶} ⊆ 𝐴 ∧ {𝐶} ⊆ 𝐵)) ↔ (𝐴 = ∅ ∧ 𝐵 = {𝐶})))
65	24, 44, 64	3orbi123d 1434	. . . 4 ⊢ (𝐶 ∈ V → ((((𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}) ∧ ({𝐶} ⊆ 𝐴 ∧ {𝐶} ⊆ 𝐵)) ∨ ((𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}) ∧ ({𝐶} ⊆ 𝐴 ∧ ¬ {𝐶} ⊆ 𝐵)) ∨ ((𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}) ∧ (¬ {𝐶} ⊆ 𝐴 ∧ {𝐶} ⊆ 𝐵))) ↔ ((𝐴 = {𝐶} ∧ 𝐵 = {𝐶}) ∨ (𝐴 = {𝐶} ∧ 𝐵 = ∅) ∨ (𝐴 = ∅ ∧ 𝐵 = {𝐶}))))
66	17, 65	bitrid 282	. . 3 ⊢ (𝐶 ∈ V → (((𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}) ∧ ({𝐶} ⊆ 𝐴 ∨ {𝐶} ⊆ 𝐵)) ↔ ((𝐴 = {𝐶} ∧ 𝐵 = {𝐶}) ∨ (𝐴 = {𝐶} ∧ 𝐵 = ∅) ∨ (𝐴 = ∅ ∧ 𝐵 = {𝐶}))))
67	2, 13, 66	3bitrd 305	. 2 ⊢ (𝐶 ∈ V → ((𝐴 ∪ 𝐵) = {𝐶} ↔ ((𝐴 = {𝐶} ∧ 𝐵 = {𝐶}) ∨ (𝐴 = {𝐶} ∧ 𝐵 = ∅) ∨ (𝐴 = ∅ ∧ 𝐵 = {𝐶}))))
68		snprc 4653	. . . . 5 ⊢ (¬ 𝐶 ∈ V ↔ {𝐶} = ∅)
69	68	biimpi 215	. . . 4 ⊢ (¬ 𝐶 ∈ V → {𝐶} = ∅)
70	69	eqeq2d 2749	. . 3 ⊢ (¬ 𝐶 ∈ V → ((𝐴 ∪ 𝐵) = {𝐶} ↔ (𝐴 ∪ 𝐵) = ∅))
71		pm4.25 903	. . . . . 6 ⊢ ((𝐴 = ∅ ∧ 𝐵 = ∅) ↔ ((𝐴 = ∅ ∧ 𝐵 = ∅) ∨ (𝐴 = ∅ ∧ 𝐵 = ∅)))
72	71	orbi1i 911	. . . . . 6 ⊢ (((𝐴 = ∅ ∧ 𝐵 = ∅) ∨ (𝐴 = ∅ ∧ 𝐵 = ∅)) ↔ (((𝐴 = ∅ ∧ 𝐵 = ∅) ∨ (𝐴 = ∅ ∧ 𝐵 = ∅)) ∨ (𝐴 = ∅ ∧ 𝐵 = ∅)))
73	71, 72	bitri 274	. . . . 5 ⊢ ((𝐴 = ∅ ∧ 𝐵 = ∅) ↔ (((𝐴 = ∅ ∧ 𝐵 = ∅) ∨ (𝐴 = ∅ ∧ 𝐵 = ∅)) ∨ (𝐴 = ∅ ∧ 𝐵 = ∅)))
74	69	eqeq2d 2749	. . . . . . . 8 ⊢ (¬ 𝐶 ∈ V → (𝐴 = {𝐶} ↔ 𝐴 = ∅))
75	69	eqeq2d 2749	. . . . . . . 8 ⊢ (¬ 𝐶 ∈ V → (𝐵 = {𝐶} ↔ 𝐵 = ∅))
76	74, 75	anbi12d 631	. . . . . . 7 ⊢ (¬ 𝐶 ∈ V → ((𝐴 = {𝐶} ∧ 𝐵 = {𝐶}) ↔ (𝐴 = ∅ ∧ 𝐵 = ∅)))
77	74	anbi1d 630	. . . . . . 7 ⊢ (¬ 𝐶 ∈ V → ((𝐴 = {𝐶} ∧ 𝐵 = ∅) ↔ (𝐴 = ∅ ∧ 𝐵 = ∅)))
78	76, 77	orbi12d 916	. . . . . 6 ⊢ (¬ 𝐶 ∈ V → (((𝐴 = {𝐶} ∧ 𝐵 = {𝐶}) ∨ (𝐴 = {𝐶} ∧ 𝐵 = ∅)) ↔ ((𝐴 = ∅ ∧ 𝐵 = ∅) ∨ (𝐴 = ∅ ∧ 𝐵 = ∅))))
79	75	anbi2d 629	. . . . . 6 ⊢ (¬ 𝐶 ∈ V → ((𝐴 = ∅ ∧ 𝐵 = {𝐶}) ↔ (𝐴 = ∅ ∧ 𝐵 = ∅)))
80	78, 79	orbi12d 916	. . . . 5 ⊢ (¬ 𝐶 ∈ V → ((((𝐴 = {𝐶} ∧ 𝐵 = {𝐶}) ∨ (𝐴 = {𝐶} ∧ 𝐵 = ∅)) ∨ (𝐴 = ∅ ∧ 𝐵 = {𝐶})) ↔ (((𝐴 = ∅ ∧ 𝐵 = ∅) ∨ (𝐴 = ∅ ∧ 𝐵 = ∅)) ∨ (𝐴 = ∅ ∧ 𝐵 = ∅))))
81	73, 80	bitr4id 290	. . . 4 ⊢ (¬ 𝐶 ∈ V → ((𝐴 = ∅ ∧ 𝐵 = ∅) ↔ (((𝐴 = {𝐶} ∧ 𝐵 = {𝐶}) ∨ (𝐴 = {𝐶} ∧ 𝐵 = ∅)) ∨ (𝐴 = ∅ ∧ 𝐵 = {𝐶}))))
82		un00 4376	. . . . 5 ⊢ ((𝐴 = ∅ ∧ 𝐵 = ∅) ↔ (𝐴 ∪ 𝐵) = ∅)
83	82	bicomi 223	. . . 4 ⊢ ((𝐴 ∪ 𝐵) = ∅ ↔ (𝐴 = ∅ ∧ 𝐵 = ∅))
84		df-3or 1087	. . . 4 ⊢ (((𝐴 = {𝐶} ∧ 𝐵 = {𝐶}) ∨ (𝐴 = {𝐶} ∧ 𝐵 = ∅) ∨ (𝐴 = ∅ ∧ 𝐵 = {𝐶})) ↔ (((𝐴 = {𝐶} ∧ 𝐵 = {𝐶}) ∨ (𝐴 = {𝐶} ∧ 𝐵 = ∅)) ∨ (𝐴 = ∅ ∧ 𝐵 = {𝐶})))
85	81, 83, 84	3bitr4g 314	. . 3 ⊢ (¬ 𝐶 ∈ V → ((𝐴 ∪ 𝐵) = ∅ ↔ ((𝐴 = {𝐶} ∧ 𝐵 = {𝐶}) ∨ (𝐴 = {𝐶} ∧ 𝐵 = ∅) ∨ (𝐴 = ∅ ∧ 𝐵 = {𝐶}))))
86	70, 85	bitrd 278	. 2 ⊢ (¬ 𝐶 ∈ V → ((𝐴 ∪ 𝐵) = {𝐶} ↔ ((𝐴 = {𝐶} ∧ 𝐵 = {𝐶}) ∨ (𝐴 = {𝐶} ∧ 𝐵 = ∅) ∨ (𝐴 = ∅ ∧ 𝐵 = {𝐶}))))
87	67, 86	pm2.61i 182	1 ⊢ ((𝐴 ∪ 𝐵) = {𝐶} ↔ ((𝐴 = {𝐶} ∧ 𝐵 = {𝐶}) ∨ (𝐴 = {𝐶} ∧ 𝐵 = ∅) ∨ (𝐴 = ∅ ∧ 𝐵 = {𝐶})))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 396   ∨ wo 844   ∨ w3o 1085   = wceq 1539   ∈ wcel 2106  Vcvv 3432   ∪ cun 3885   ⊆ wss 3887  ∅c0 4256  {csn 4561

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-xor 1507  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-sn 4562

This theorem is referenced by:  clsk1indlem3  41653