Theorem uneqsn 41522

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 3932	. . . 4 ⊢ ((𝐴 ∪ 𝐵) = {𝐶} ↔ ((𝐴 ∪ 𝐵) ⊆ {𝐶} ∧ {𝐶} ⊆ (𝐴 ∪ 𝐵)))
2	1	a1i 11	. . 3 ⊢ (𝐶 ∈ V → ((𝐴 ∪ 𝐵) = {𝐶} ↔ ((𝐴 ∪ 𝐵) ⊆ {𝐶} ∧ {𝐶} ⊆ (𝐴 ∪ 𝐵))))
3		unss 4114	. . . . . 6 ⊢ ((𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}) ↔ (𝐴 ∪ 𝐵) ⊆ {𝐶})
4	3	bicomi 223	. . . . 5 ⊢ ((𝐴 ∪ 𝐵) ⊆ {𝐶} ↔ (𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}))
5	4	a1i 11	. . . 4 ⊢ (𝐶 ∈ V → ((𝐴 ∪ 𝐵) ⊆ {𝐶} ↔ (𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶})))
6		elun 4079	. . . . . 6 ⊢ (𝐶 ∈ (𝐴 ∪ 𝐵) ↔ (𝐶 ∈ 𝐴 ∨ 𝐶 ∈ 𝐵))
7		snssg 4715	. . . . . . 7 ⊢ (𝐶 ∈ V → (𝐶 ∈ 𝐴 ↔ {𝐶} ⊆ 𝐴))
8		snssg 4715	. . . . . . 7 ⊢ (𝐶 ∈ V → (𝐶 ∈ 𝐵 ↔ {𝐶} ⊆ 𝐵))
9	7, 8	orbi12d 915	. . . . . 6 ⊢ (𝐶 ∈ V → ((𝐶 ∈ 𝐴 ∨ 𝐶 ∈ 𝐵) ↔ ({𝐶} ⊆ 𝐴 ∨ {𝐶} ⊆ 𝐵)))
10	6, 9	bitr2id 283	. . . . 5 ⊢ (𝐶 ∈ V → (({𝐶} ⊆ 𝐴 ∨ {𝐶} ⊆ 𝐵) ↔ 𝐶 ∈ (𝐴 ∪ 𝐵)))
11		snssg 4715	. . . . 5 ⊢ (𝐶 ∈ V → (𝐶 ∈ (𝐴 ∪ 𝐵) ↔ {𝐶} ⊆ (𝐴 ∪ 𝐵)))
12	10, 11	bitr2d 279	. . . 4 ⊢ (𝐶 ∈ V → ({𝐶} ⊆ (𝐴 ∪ 𝐵) ↔ ({𝐶} ⊆ 𝐴 ∨ {𝐶} ⊆ 𝐵)))
13	5, 12	anbi12d 630	. . 3 ⊢ (𝐶 ∈ V → (((𝐴 ∪ 𝐵) ⊆ {𝐶} ∧ {𝐶} ⊆ (𝐴 ∪ 𝐵)) ↔ ((𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}) ∧ ({𝐶} ⊆ 𝐴 ∨ {𝐶} ⊆ 𝐵))))
14		or3or 41520	. . . . . 6 ⊢ (({𝐶} ⊆ 𝐴 ∨ {𝐶} ⊆ 𝐵) ↔ (({𝐶} ⊆ 𝐴 ∧ {𝐶} ⊆ 𝐵) ∨ ({𝐶} ⊆ 𝐴 ∧ ¬ {𝐶} ⊆ 𝐵) ∨ (¬ {𝐶} ⊆ 𝐴 ∧ {𝐶} ⊆ 𝐵)))
15	14	anbi2i 622	. . . . 5 ⊢ (((𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}) ∧ ({𝐶} ⊆ 𝐴 ∨ {𝐶} ⊆ 𝐵)) ↔ ((𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}) ∧ (({𝐶} ⊆ 𝐴 ∧ {𝐶} ⊆ 𝐵) ∨ ({𝐶} ⊆ 𝐴 ∧ ¬ {𝐶} ⊆ 𝐵) ∨ (¬ {𝐶} ⊆ 𝐴 ∧ {𝐶} ⊆ 𝐵))))
16		andi3or 41521	. . . . 5 ⊢ (((𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}) ∧ (({𝐶} ⊆ 𝐴 ∧ {𝐶} ⊆ 𝐵) ∨ ({𝐶} ⊆ 𝐴 ∧ ¬ {𝐶} ⊆ 𝐵) ∨ (¬ {𝐶} ⊆ 𝐴 ∧ {𝐶} ⊆ 𝐵))) ↔ (((𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}) ∧ ({𝐶} ⊆ 𝐴 ∧ {𝐶} ⊆ 𝐵)) ∨ ((𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}) ∧ ({𝐶} ⊆ 𝐴 ∧ ¬ {𝐶} ⊆ 𝐵)) ∨ ((𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}) ∧ (¬ {𝐶} ⊆ 𝐴 ∧ {𝐶} ⊆ 𝐵))))
17	15, 16	bitri 274	. . . 4 ⊢ (((𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}) ∧ ({𝐶} ⊆ 𝐴 ∨ {𝐶} ⊆ 𝐵)) ↔ (((𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}) ∧ ({𝐶} ⊆ 𝐴 ∧ {𝐶} ⊆ 𝐵)) ∨ ((𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}) ∧ ({𝐶} ⊆ 𝐴 ∧ ¬ {𝐶} ⊆ 𝐵)) ∨ ((𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}) ∧ (¬ {𝐶} ⊆ 𝐴 ∧ {𝐶} ⊆ 𝐵))))
18		an4 652	. . . . . . 7 ⊢ (((𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}) ∧ ({𝐶} ⊆ 𝐴 ∧ {𝐶} ⊆ 𝐵)) ↔ ((𝐴 ⊆ {𝐶} ∧ {𝐶} ⊆ 𝐴) ∧ (𝐵 ⊆ {𝐶} ∧ {𝐶} ⊆ 𝐵)))
19		eqss 3932	. . . . . . . . 9 ⊢ (𝐴 = {𝐶} ↔ (𝐴 ⊆ {𝐶} ∧ {𝐶} ⊆ 𝐴))
20		eqss 3932	. . . . . . . . 9 ⊢ (𝐵 = {𝐶} ↔ (𝐵 ⊆ {𝐶} ∧ {𝐶} ⊆ 𝐵))
21	19, 20	anbi12i 626	. . . . . . . 8 ⊢ ((𝐴 = {𝐶} ∧ 𝐵 = {𝐶}) ↔ ((𝐴 ⊆ {𝐶} ∧ {𝐶} ⊆ 𝐴) ∧ (𝐵 ⊆ {𝐶} ∧ {𝐶} ⊆ 𝐵)))
22	21	bicomi 223	. . . . . . 7 ⊢ (((𝐴 ⊆ {𝐶} ∧ {𝐶} ⊆ 𝐴) ∧ (𝐵 ⊆ {𝐶} ∧ {𝐶} ⊆ 𝐵)) ↔ (𝐴 = {𝐶} ∧ 𝐵 = {𝐶}))
23	18, 22	bitri 274	. . . . . 6 ⊢ (((𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}) ∧ ({𝐶} ⊆ 𝐴 ∧ {𝐶} ⊆ 𝐵)) ↔ (𝐴 = {𝐶} ∧ 𝐵 = {𝐶}))
24	23	a1i 11	. . . . 5 ⊢ (𝐶 ∈ V → (((𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}) ∧ ({𝐶} ⊆ 𝐴 ∧ {𝐶} ⊆ 𝐵)) ↔ (𝐴 = {𝐶} ∧ 𝐵 = {𝐶})))
25		an4 652	. . . . . 6 ⊢ (((𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}) ∧ ({𝐶} ⊆ 𝐴 ∧ ¬ {𝐶} ⊆ 𝐵)) ↔ ((𝐴 ⊆ {𝐶} ∧ {𝐶} ⊆ 𝐴) ∧ (𝐵 ⊆ {𝐶} ∧ ¬ {𝐶} ⊆ 𝐵)))
26	19	bicomi 223	. . . . . . . 8 ⊢ ((𝐴 ⊆ {𝐶} ∧ {𝐶} ⊆ 𝐴) ↔ 𝐴 = {𝐶})
27	26	a1i 11	. . . . . . 7 ⊢ (𝐶 ∈ V → ((𝐴 ⊆ {𝐶} ∧ {𝐶} ⊆ 𝐴) ↔ 𝐴 = {𝐶}))
28		sssn 4756	. . . . . . . . . 10 ⊢ (𝐵 ⊆ {𝐶} ↔ (𝐵 = ∅ ∨ 𝐵 = {𝐶}))
29	28	a1i 11	. . . . . . . . 9 ⊢ (𝐶 ∈ V → (𝐵 ⊆ {𝐶} ↔ (𝐵 = ∅ ∨ 𝐵 = {𝐶})))
30	29	anbi1d 629	. . . . . . . 8 ⊢ (𝐶 ∈ V → ((𝐵 ⊆ {𝐶} ∧ ¬ {𝐶} ⊆ 𝐵) ↔ ((𝐵 = ∅ ∨ 𝐵 = {𝐶}) ∧ ¬ {𝐶} ⊆ 𝐵)))
31		andir 1005	. . . . . . . . 9 ⊢ (((𝐵 = ∅ ∨ 𝐵 = {𝐶}) ∧ ¬ {𝐶} ⊆ 𝐵) ↔ ((𝐵 = ∅ ∧ ¬ {𝐶} ⊆ 𝐵) ∨ (𝐵 = {𝐶} ∧ ¬ {𝐶} ⊆ 𝐵)))
32		n0i 4264	. . . . . . . . . . . . 13 ⊢ (𝐶 ∈ 𝐵 → ¬ 𝐵 = ∅)
33	8, 32	syl6bir 253	. . . . . . . . . . . 12 ⊢ (𝐶 ∈ V → ({𝐶} ⊆ 𝐵 → ¬ 𝐵 = ∅))
34	33	con2d 134	. . . . . . . . . . 11 ⊢ (𝐶 ∈ V → (𝐵 = ∅ → ¬ {𝐶} ⊆ 𝐵))
35	34	pm4.71d 561	. . . . . . . . . 10 ⊢ (𝐶 ∈ V → (𝐵 = ∅ ↔ (𝐵 = ∅ ∧ ¬ {𝐶} ⊆ 𝐵)))
36		eqimss2 3974	. . . . . . . . . . . 12 ⊢ (𝐵 = {𝐶} → {𝐶} ⊆ 𝐵)
37		iman 401	. . . . . . . . . . . 12 ⊢ ((𝐵 = {𝐶} → {𝐶} ⊆ 𝐵) ↔ ¬ (𝐵 = {𝐶} ∧ ¬ {𝐶} ⊆ 𝐵))
38	36, 37	mpbi 229	. . . . . . . . . . 11 ⊢ ¬ (𝐵 = {𝐶} ∧ ¬ {𝐶} ⊆ 𝐵)
39	38	biorfi 935	. . . . . . . . . 10 ⊢ ((𝐵 = ∅ ∧ ¬ {𝐶} ⊆ 𝐵) ↔ ((𝐵 = ∅ ∧ ¬ {𝐶} ⊆ 𝐵) ∨ (𝐵 = {𝐶} ∧ ¬ {𝐶} ⊆ 𝐵)))
40	35, 39	bitr2di 287	. . . . . . . . 9 ⊢ (𝐶 ∈ V → (((𝐵 = ∅ ∧ ¬ {𝐶} ⊆ 𝐵) ∨ (𝐵 = {𝐶} ∧ ¬ {𝐶} ⊆ 𝐵)) ↔ 𝐵 = ∅))
41	31, 40	syl5bb 282	. . . . . . . 8 ⊢ (𝐶 ∈ V → (((𝐵 = ∅ ∨ 𝐵 = {𝐶}) ∧ ¬ {𝐶} ⊆ 𝐵) ↔ 𝐵 = ∅))
42	30, 41	bitrd 278	. . . . . . 7 ⊢ (𝐶 ∈ V → ((𝐵 ⊆ {𝐶} ∧ ¬ {𝐶} ⊆ 𝐵) ↔ 𝐵 = ∅))
43	27, 42	anbi12d 630	. . . . . 6 ⊢ (𝐶 ∈ V → (((𝐴 ⊆ {𝐶} ∧ {𝐶} ⊆ 𝐴) ∧ (𝐵 ⊆ {𝐶} ∧ ¬ {𝐶} ⊆ 𝐵)) ↔ (𝐴 = {𝐶} ∧ 𝐵 = ∅)))
44	25, 43	syl5bb 282	. . . . 5 ⊢ (𝐶 ∈ V → (((𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}) ∧ ({𝐶} ⊆ 𝐴 ∧ ¬ {𝐶} ⊆ 𝐵)) ↔ (𝐴 = {𝐶} ∧ 𝐵 = ∅)))
45		an4 652	. . . . . 6 ⊢ (((𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}) ∧ (¬ {𝐶} ⊆ 𝐴 ∧ {𝐶} ⊆ 𝐵)) ↔ ((𝐴 ⊆ {𝐶} ∧ ¬ {𝐶} ⊆ 𝐴) ∧ (𝐵 ⊆ {𝐶} ∧ {𝐶} ⊆ 𝐵)))
46		sssn 4756	. . . . . . . . . 10 ⊢ (𝐴 ⊆ {𝐶} ↔ (𝐴 = ∅ ∨ 𝐴 = {𝐶}))
47	46	a1i 11	. . . . . . . . 9 ⊢ (𝐶 ∈ V → (𝐴 ⊆ {𝐶} ↔ (𝐴 = ∅ ∨ 𝐴 = {𝐶})))
48	47	anbi1d 629	. . . . . . . 8 ⊢ (𝐶 ∈ V → ((𝐴 ⊆ {𝐶} ∧ ¬ {𝐶} ⊆ 𝐴) ↔ ((𝐴 = ∅ ∨ 𝐴 = {𝐶}) ∧ ¬ {𝐶} ⊆ 𝐴)))
49		andir 1005	. . . . . . . . 9 ⊢ (((𝐴 = ∅ ∨ 𝐴 = {𝐶}) ∧ ¬ {𝐶} ⊆ 𝐴) ↔ ((𝐴 = ∅ ∧ ¬ {𝐶} ⊆ 𝐴) ∨ (𝐴 = {𝐶} ∧ ¬ {𝐶} ⊆ 𝐴)))
50		n0i 4264	. . . . . . . . . . . . 13 ⊢ (𝐶 ∈ 𝐴 → ¬ 𝐴 = ∅)
51	7, 50	syl6bir 253	. . . . . . . . . . . 12 ⊢ (𝐶 ∈ V → ({𝐶} ⊆ 𝐴 → ¬ 𝐴 = ∅))
52	51	con2d 134	. . . . . . . . . . 11 ⊢ (𝐶 ∈ V → (𝐴 = ∅ → ¬ {𝐶} ⊆ 𝐴))
53	52	pm4.71d 561	. . . . . . . . . 10 ⊢ (𝐶 ∈ V → (𝐴 = ∅ ↔ (𝐴 = ∅ ∧ ¬ {𝐶} ⊆ 𝐴)))
54		eqimss2 3974	. . . . . . . . . . . 12 ⊢ (𝐴 = {𝐶} → {𝐶} ⊆ 𝐴)
55		iman 401	. . . . . . . . . . . 12 ⊢ ((𝐴 = {𝐶} → {𝐶} ⊆ 𝐴) ↔ ¬ (𝐴 = {𝐶} ∧ ¬ {𝐶} ⊆ 𝐴))
56	54, 55	mpbi 229	. . . . . . . . . . 11 ⊢ ¬ (𝐴 = {𝐶} ∧ ¬ {𝐶} ⊆ 𝐴)
57	56	biorfi 935	. . . . . . . . . 10 ⊢ ((𝐴 = ∅ ∧ ¬ {𝐶} ⊆ 𝐴) ↔ ((𝐴 = ∅ ∧ ¬ {𝐶} ⊆ 𝐴) ∨ (𝐴 = {𝐶} ∧ ¬ {𝐶} ⊆ 𝐴)))
58	53, 57	bitr2di 287	. . . . . . . . 9 ⊢ (𝐶 ∈ V → (((𝐴 = ∅ ∧ ¬ {𝐶} ⊆ 𝐴) ∨ (𝐴 = {𝐶} ∧ ¬ {𝐶} ⊆ 𝐴)) ↔ 𝐴 = ∅))
59	49, 58	syl5bb 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 630	. . . . . 6 ⊢ (𝐶 ∈ V → (((𝐴 ⊆ {𝐶} ∧ ¬ {𝐶} ⊆ 𝐴) ∧ (𝐵 ⊆ {𝐶} ∧ {𝐶} ⊆ 𝐵)) ↔ (𝐴 = ∅ ∧ 𝐵 = {𝐶})))
64	45, 63	syl5bb 282	. . . . 5 ⊢ (𝐶 ∈ V → (((𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}) ∧ (¬ {𝐶} ⊆ 𝐴 ∧ {𝐶} ⊆ 𝐵)) ↔ (𝐴 = ∅ ∧ 𝐵 = {𝐶})))
65	24, 44, 64	3orbi123d 1433	. . . 4 ⊢ (𝐶 ∈ V → ((((𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}) ∧ ({𝐶} ⊆ 𝐴 ∧ {𝐶} ⊆ 𝐵)) ∨ ((𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}) ∧ ({𝐶} ⊆ 𝐴 ∧ ¬ {𝐶} ⊆ 𝐵)) ∨ ((𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}) ∧ (¬ {𝐶} ⊆ 𝐴 ∧ {𝐶} ⊆ 𝐵))) ↔ ((𝐴 = {𝐶} ∧ 𝐵 = {𝐶}) ∨ (𝐴 = {𝐶} ∧ 𝐵 = ∅) ∨ (𝐴 = ∅ ∧ 𝐵 = {𝐶}))))
66	17, 65	syl5bb 282	. . 3 ⊢ (𝐶 ∈ V → (((𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}) ∧ ({𝐶} ⊆ 𝐴 ∨ {𝐶} ⊆ 𝐵)) ↔ ((𝐴 = {𝐶} ∧ 𝐵 = {𝐶}) ∨ (𝐴 = {𝐶} ∧ 𝐵 = ∅) ∨ (𝐴 = ∅ ∧ 𝐵 = {𝐶}))))
67	2, 13, 66	3bitrd 304	. 2 ⊢ (𝐶 ∈ V → ((𝐴 ∪ 𝐵) = {𝐶} ↔ ((𝐴 = {𝐶} ∧ 𝐵 = {𝐶}) ∨ (𝐴 = {𝐶} ∧ 𝐵 = ∅) ∨ (𝐴 = ∅ ∧ 𝐵 = {𝐶}))))
68		snprc 4650	. . . . 5 ⊢ (¬ 𝐶 ∈ V ↔ {𝐶} = ∅)
69	68	biimpi 215	. . . 4 ⊢ (¬ 𝐶 ∈ V → {𝐶} = ∅)
70	69	eqeq2d 2749	. . 3 ⊢ (¬ 𝐶 ∈ V → ((𝐴 ∪ 𝐵) = {𝐶} ↔ (𝐴 ∪ 𝐵) = ∅))
71		pm4.25 902	. . . . . 6 ⊢ ((𝐴 = ∅ ∧ 𝐵 = ∅) ↔ ((𝐴 = ∅ ∧ 𝐵 = ∅) ∨ (𝐴 = ∅ ∧ 𝐵 = ∅)))
72	71	orbi1i 910	. . . . . 6 ⊢ (((𝐴 = ∅ ∧ 𝐵 = ∅) ∨ (𝐴 = ∅ ∧ 𝐵 = ∅)) ↔ (((𝐴 = ∅ ∧ 𝐵 = ∅) ∨ (𝐴 = ∅ ∧ 𝐵 = ∅)) ∨ (𝐴 = ∅ ∧ 𝐵 = ∅)))
73	71, 72	bitri 274	. . . . 5 ⊢ ((𝐴 = ∅ ∧ 𝐵 = ∅) ↔ (((𝐴 = ∅ ∧ 𝐵 = ∅) ∨ (𝐴 = ∅ ∧ 𝐵 = ∅)) ∨ (𝐴 = ∅ ∧ 𝐵 = ∅)))
74	69	eqeq2d 2749	. . . . . . . 8 ⊢ (¬ 𝐶 ∈ V → (𝐴 = {𝐶} ↔ 𝐴 = ∅))
75	69	eqeq2d 2749	. . . . . . . 8 ⊢ (¬ 𝐶 ∈ V → (𝐵 = {𝐶} ↔ 𝐵 = ∅))
76	74, 75	anbi12d 630	. . . . . . 7 ⊢ (¬ 𝐶 ∈ V → ((𝐴 = {𝐶} ∧ 𝐵 = {𝐶}) ↔ (𝐴 = ∅ ∧ 𝐵 = ∅)))
77	74	anbi1d 629	. . . . . . 7 ⊢ (¬ 𝐶 ∈ V → ((𝐴 = {𝐶} ∧ 𝐵 = ∅) ↔ (𝐴 = ∅ ∧ 𝐵 = ∅)))
78	76, 77	orbi12d 915	. . . . . 6 ⊢ (¬ 𝐶 ∈ V → (((𝐴 = {𝐶} ∧ 𝐵 = {𝐶}) ∨ (𝐴 = {𝐶} ∧ 𝐵 = ∅)) ↔ ((𝐴 = ∅ ∧ 𝐵 = ∅) ∨ (𝐴 = ∅ ∧ 𝐵 = ∅))))
79	75	anbi2d 628	. . . . . 6 ⊢ (¬ 𝐶 ∈ V → ((𝐴 = ∅ ∧ 𝐵 = {𝐶}) ↔ (𝐴 = ∅ ∧ 𝐵 = ∅)))
80	78, 79	orbi12d 915	. . . . 5 ⊢ (¬ 𝐶 ∈ V → ((((𝐴 = {𝐶} ∧ 𝐵 = {𝐶}) ∨ (𝐴 = {𝐶} ∧ 𝐵 = ∅)) ∨ (𝐴 = ∅ ∧ 𝐵 = {𝐶})) ↔ (((𝐴 = ∅ ∧ 𝐵 = ∅) ∨ (𝐴 = ∅ ∧ 𝐵 = ∅)) ∨ (𝐴 = ∅ ∧ 𝐵 = ∅))))
81	73, 80	bitr4id 289	. . . 4 ⊢ (¬ 𝐶 ∈ V → ((𝐴 = ∅ ∧ 𝐵 = ∅) ↔ (((𝐴 = {𝐶} ∧ 𝐵 = {𝐶}) ∨ (𝐴 = {𝐶} ∧ 𝐵 = ∅)) ∨ (𝐴 = ∅ ∧ 𝐵 = {𝐶}))))
82		un00 4373	. . . . 5 ⊢ ((𝐴 = ∅ ∧ 𝐵 = ∅) ↔ (𝐴 ∪ 𝐵) = ∅)
83	82	bicomi 223	. . . 4 ⊢ ((𝐴 ∪ 𝐵) = ∅ ↔ (𝐴 = ∅ ∧ 𝐵 = ∅))
84		df-3or 1086	. . . 4 ⊢ (((𝐴 = {𝐶} ∧ 𝐵 = {𝐶}) ∨ (𝐴 = {𝐶} ∧ 𝐵 = ∅) ∨ (𝐴 = ∅ ∧ 𝐵 = {𝐶})) ↔ (((𝐴 = {𝐶} ∧ 𝐵 = {𝐶}) ∨ (𝐴 = {𝐶} ∧ 𝐵 = ∅)) ∨ (𝐴 = ∅ ∧ 𝐵 = {𝐶})))
85	81, 83, 84	3bitr4g 313	. . 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 395   ∨ wo 843   ∨ w3o 1084   = wceq 1539   ∈ wcel 2108  Vcvv 3422   ∪ cun 3881   ⊆ wss 3883  ∅c0 4253  {csn 4558

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-xor 1504  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-sn 4559

This theorem is referenced by:  clsk1indlem3  41542