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

Step	Hyp	Ref	Expression
1		eqss 3583	. . . 4 ⊢ ((𝐴 ∪ 𝐵) = {𝐶} ↔ ((𝐴 ∪ 𝐵) ⊆ {𝐶} ∧ {𝐶} ⊆ (𝐴 ∪ 𝐵)))
2	1	a1i 11	. . 3 ⊢ (𝐶 ∈ V → ((𝐴 ∪ 𝐵) = {𝐶} ↔ ((𝐴 ∪ 𝐵) ⊆ {𝐶} ∧ {𝐶} ⊆ (𝐴 ∪ 𝐵))))
3		unss 3749	. . . . . 6 ⊢ ((𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}) ↔ (𝐴 ∪ 𝐵) ⊆ {𝐶})
4	3	bicomi 213	. . . . 5 ⊢ ((𝐴 ∪ 𝐵) ⊆ {𝐶} ↔ (𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}))
5	4	a1i 11	. . . 4 ⊢ (𝐶 ∈ V → ((𝐴 ∪ 𝐵) ⊆ {𝐶} ↔ (𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶})))
6		elun 3715	. . . . . 6 ⊢ (𝐶 ∈ (𝐴 ∪ 𝐵) ↔ (𝐶 ∈ 𝐴 ∨ 𝐶 ∈ 𝐵))
7		snssg 4268	. . . . . . 7 ⊢ (𝐶 ∈ V → (𝐶 ∈ 𝐴 ↔ {𝐶} ⊆ 𝐴))
8		snssg 4268	. . . . . . 7 ⊢ (𝐶 ∈ V → (𝐶 ∈ 𝐵 ↔ {𝐶} ⊆ 𝐵))
9	7, 8	orbi12d 742	. . . . . 6 ⊢ (𝐶 ∈ V → ((𝐶 ∈ 𝐴 ∨ 𝐶 ∈ 𝐵) ↔ ({𝐶} ⊆ 𝐴 ∨ {𝐶} ⊆ 𝐵)))
10	6, 9	syl5rbb 272	. . . . 5 ⊢ (𝐶 ∈ V → (({𝐶} ⊆ 𝐴 ∨ {𝐶} ⊆ 𝐵) ↔ 𝐶 ∈ (𝐴 ∪ 𝐵)))
11		snssg 4268	. . . . 5 ⊢ (𝐶 ∈ V → (𝐶 ∈ (𝐴 ∪ 𝐵) ↔ {𝐶} ⊆ (𝐴 ∪ 𝐵)))
12	10, 11	bitr2d 268	. . . 4 ⊢ (𝐶 ∈ V → ({𝐶} ⊆ (𝐴 ∪ 𝐵) ↔ ({𝐶} ⊆ 𝐴 ∨ {𝐶} ⊆ 𝐵)))
13	5, 12	anbi12d 743	. . 3 ⊢ (𝐶 ∈ V → (((𝐴 ∪ 𝐵) ⊆ {𝐶} ∧ {𝐶} ⊆ (𝐴 ∪ 𝐵)) ↔ ((𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}) ∧ ({𝐶} ⊆ 𝐴 ∨ {𝐶} ⊆ 𝐵))))
14		or3or 37339	. . . . . 6 ⊢ (({𝐶} ⊆ 𝐴 ∨ {𝐶} ⊆ 𝐵) ↔ (({𝐶} ⊆ 𝐴 ∧ {𝐶} ⊆ 𝐵) ∨ ({𝐶} ⊆ 𝐴 ∧ ¬ {𝐶} ⊆ 𝐵) ∨ (¬ {𝐶} ⊆ 𝐴 ∧ {𝐶} ⊆ 𝐵)))
15	14	anbi2i 726	. . . . 5 ⊢ (((𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}) ∧ ({𝐶} ⊆ 𝐴 ∨ {𝐶} ⊆ 𝐵)) ↔ ((𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}) ∧ (({𝐶} ⊆ 𝐴 ∧ {𝐶} ⊆ 𝐵) ∨ ({𝐶} ⊆ 𝐴 ∧ ¬ {𝐶} ⊆ 𝐵) ∨ (¬ {𝐶} ⊆ 𝐴 ∧ {𝐶} ⊆ 𝐵))))
16		andi3or 37340	. . . . 5 ⊢ (((𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}) ∧ (({𝐶} ⊆ 𝐴 ∧ {𝐶} ⊆ 𝐵) ∨ ({𝐶} ⊆ 𝐴 ∧ ¬ {𝐶} ⊆ 𝐵) ∨ (¬ {𝐶} ⊆ 𝐴 ∧ {𝐶} ⊆ 𝐵))) ↔ (((𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}) ∧ ({𝐶} ⊆ 𝐴 ∧ {𝐶} ⊆ 𝐵)) ∨ ((𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}) ∧ ({𝐶} ⊆ 𝐴 ∧ ¬ {𝐶} ⊆ 𝐵)) ∨ ((𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}) ∧ (¬ {𝐶} ⊆ 𝐴 ∧ {𝐶} ⊆ 𝐵))))
17	15, 16	bitri 263	. . . 4 ⊢ (((𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}) ∧ ({𝐶} ⊆ 𝐴 ∨ {𝐶} ⊆ 𝐵)) ↔ (((𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}) ∧ ({𝐶} ⊆ 𝐴 ∧ {𝐶} ⊆ 𝐵)) ∨ ((𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}) ∧ ({𝐶} ⊆ 𝐴 ∧ ¬ {𝐶} ⊆ 𝐵)) ∨ ((𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}) ∧ (¬ {𝐶} ⊆ 𝐴 ∧ {𝐶} ⊆ 𝐵))))
18		an4 861	. . . . . . 7 ⊢ (((𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}) ∧ ({𝐶} ⊆ 𝐴 ∧ {𝐶} ⊆ 𝐵)) ↔ ((𝐴 ⊆ {𝐶} ∧ {𝐶} ⊆ 𝐴) ∧ (𝐵 ⊆ {𝐶} ∧ {𝐶} ⊆ 𝐵)))
19		eqss 3583	. . . . . . . . 9 ⊢ (𝐴 = {𝐶} ↔ (𝐴 ⊆ {𝐶} ∧ {𝐶} ⊆ 𝐴))
20		eqss 3583	. . . . . . . . 9 ⊢ (𝐵 = {𝐶} ↔ (𝐵 ⊆ {𝐶} ∧ {𝐶} ⊆ 𝐵))
21	19, 20	anbi12i 729	. . . . . . . 8 ⊢ ((𝐴 = {𝐶} ∧ 𝐵 = {𝐶}) ↔ ((𝐴 ⊆ {𝐶} ∧ {𝐶} ⊆ 𝐴) ∧ (𝐵 ⊆ {𝐶} ∧ {𝐶} ⊆ 𝐵)))
22	21	bicomi 213	. . . . . . 7 ⊢ (((𝐴 ⊆ {𝐶} ∧ {𝐶} ⊆ 𝐴) ∧ (𝐵 ⊆ {𝐶} ∧ {𝐶} ⊆ 𝐵)) ↔ (𝐴 = {𝐶} ∧ 𝐵 = {𝐶}))
23	18, 22	bitri 263	. . . . . 6 ⊢ (((𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}) ∧ ({𝐶} ⊆ 𝐴 ∧ {𝐶} ⊆ 𝐵)) ↔ (𝐴 = {𝐶} ∧ 𝐵 = {𝐶}))
24	23	a1i 11	. . . . 5 ⊢ (𝐶 ∈ V → (((𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}) ∧ ({𝐶} ⊆ 𝐴 ∧ {𝐶} ⊆ 𝐵)) ↔ (𝐴 = {𝐶} ∧ 𝐵 = {𝐶})))
25		an4 861	. . . . . 6 ⊢ (((𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}) ∧ ({𝐶} ⊆ 𝐴 ∧ ¬ {𝐶} ⊆ 𝐵)) ↔ ((𝐴 ⊆ {𝐶} ∧ {𝐶} ⊆ 𝐴) ∧ (𝐵 ⊆ {𝐶} ∧ ¬ {𝐶} ⊆ 𝐵)))
26	19	bicomi 213	. . . . . . . 8 ⊢ ((𝐴 ⊆ {𝐶} ∧ {𝐶} ⊆ 𝐴) ↔ 𝐴 = {𝐶})
27	26	a1i 11	. . . . . . 7 ⊢ (𝐶 ∈ V → ((𝐴 ⊆ {𝐶} ∧ {𝐶} ⊆ 𝐴) ↔ 𝐴 = {𝐶}))
28		sssn 4298	. . . . . . . . . 10 ⊢ (𝐵 ⊆ {𝐶} ↔ (𝐵 = ∅ ∨ 𝐵 = {𝐶}))
29	28	a1i 11	. . . . . . . . 9 ⊢ (𝐶 ∈ V → (𝐵 ⊆ {𝐶} ↔ (𝐵 = ∅ ∨ 𝐵 = {𝐶})))
30	29	anbi1d 737	. . . . . . . 8 ⊢ (𝐶 ∈ V → ((𝐵 ⊆ {𝐶} ∧ ¬ {𝐶} ⊆ 𝐵) ↔ ((𝐵 = ∅ ∨ 𝐵 = {𝐶}) ∧ ¬ {𝐶} ⊆ 𝐵)))
31		andir 908	. . . . . . . . 9 ⊢ (((𝐵 = ∅ ∨ 𝐵 = {𝐶}) ∧ ¬ {𝐶} ⊆ 𝐵) ↔ ((𝐵 = ∅ ∧ ¬ {𝐶} ⊆ 𝐵) ∨ (𝐵 = {𝐶} ∧ ¬ {𝐶} ⊆ 𝐵)))
32		n0i 3879	. . . . . . . . . . . . 13 ⊢ (𝐶 ∈ 𝐵 → ¬ 𝐵 = ∅)
33	8, 32	syl6bir 243	. . . . . . . . . . . 12 ⊢ (𝐶 ∈ V → ({𝐶} ⊆ 𝐵 → ¬ 𝐵 = ∅))
34	33	con2d 128	. . . . . . . . . . 11 ⊢ (𝐶 ∈ V → (𝐵 = ∅ → ¬ {𝐶} ⊆ 𝐵))
35	34	pm4.71d 664	. . . . . . . . . 10 ⊢ (𝐶 ∈ V → (𝐵 = ∅ ↔ (𝐵 = ∅ ∧ ¬ {𝐶} ⊆ 𝐵)))
36		eqimss2 3621	. . . . . . . . . . . 12 ⊢ (𝐵 = {𝐶} → {𝐶} ⊆ 𝐵)
37		iman 439	. . . . . . . . . . . 12 ⊢ ((𝐵 = {𝐶} → {𝐶} ⊆ 𝐵) ↔ ¬ (𝐵 = {𝐶} ∧ ¬ {𝐶} ⊆ 𝐵))
38	36, 37	mpbi 219	. . . . . . . . . . 11 ⊢ ¬ (𝐵 = {𝐶} ∧ ¬ {𝐶} ⊆ 𝐵)
39	38	biorfi 421	. . . . . . . . . 10 ⊢ ((𝐵 = ∅ ∧ ¬ {𝐶} ⊆ 𝐵) ↔ ((𝐵 = ∅ ∧ ¬ {𝐶} ⊆ 𝐵) ∨ (𝐵 = {𝐶} ∧ ¬ {𝐶} ⊆ 𝐵)))
40	35, 39	syl6rbb 276	. . . . . . . . 9 ⊢ (𝐶 ∈ V → (((𝐵 = ∅ ∧ ¬ {𝐶} ⊆ 𝐵) ∨ (𝐵 = {𝐶} ∧ ¬ {𝐶} ⊆ 𝐵)) ↔ 𝐵 = ∅))
41	31, 40	syl5bb 271	. . . . . . . 8 ⊢ (𝐶 ∈ V → (((𝐵 = ∅ ∨ 𝐵 = {𝐶}) ∧ ¬ {𝐶} ⊆ 𝐵) ↔ 𝐵 = ∅))
42	30, 41	bitrd 267	. . . . . . 7 ⊢ (𝐶 ∈ V → ((𝐵 ⊆ {𝐶} ∧ ¬ {𝐶} ⊆ 𝐵) ↔ 𝐵 = ∅))
43	27, 42	anbi12d 743	. . . . . 6 ⊢ (𝐶 ∈ V → (((𝐴 ⊆ {𝐶} ∧ {𝐶} ⊆ 𝐴) ∧ (𝐵 ⊆ {𝐶} ∧ ¬ {𝐶} ⊆ 𝐵)) ↔ (𝐴 = {𝐶} ∧ 𝐵 = ∅)))
44	25, 43	syl5bb 271	. . . . 5 ⊢ (𝐶 ∈ V → (((𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}) ∧ ({𝐶} ⊆ 𝐴 ∧ ¬ {𝐶} ⊆ 𝐵)) ↔ (𝐴 = {𝐶} ∧ 𝐵 = ∅)))
45		an4 861	. . . . . 6 ⊢ (((𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}) ∧ (¬ {𝐶} ⊆ 𝐴 ∧ {𝐶} ⊆ 𝐵)) ↔ ((𝐴 ⊆ {𝐶} ∧ ¬ {𝐶} ⊆ 𝐴) ∧ (𝐵 ⊆ {𝐶} ∧ {𝐶} ⊆ 𝐵)))
46		sssn 4298	. . . . . . . . . 10 ⊢ (𝐴 ⊆ {𝐶} ↔ (𝐴 = ∅ ∨ 𝐴 = {𝐶}))
47	46	a1i 11	. . . . . . . . 9 ⊢ (𝐶 ∈ V → (𝐴 ⊆ {𝐶} ↔ (𝐴 = ∅ ∨ 𝐴 = {𝐶})))
48	47	anbi1d 737	. . . . . . . 8 ⊢ (𝐶 ∈ V → ((𝐴 ⊆ {𝐶} ∧ ¬ {𝐶} ⊆ 𝐴) ↔ ((𝐴 = ∅ ∨ 𝐴 = {𝐶}) ∧ ¬ {𝐶} ⊆ 𝐴)))
49		andir 908	. . . . . . . . 9 ⊢ (((𝐴 = ∅ ∨ 𝐴 = {𝐶}) ∧ ¬ {𝐶} ⊆ 𝐴) ↔ ((𝐴 = ∅ ∧ ¬ {𝐶} ⊆ 𝐴) ∨ (𝐴 = {𝐶} ∧ ¬ {𝐶} ⊆ 𝐴)))
50		n0i 3879	. . . . . . . . . . . . 13 ⊢ (𝐶 ∈ 𝐴 → ¬ 𝐴 = ∅)
51	7, 50	syl6bir 243	. . . . . . . . . . . 12 ⊢ (𝐶 ∈ V → ({𝐶} ⊆ 𝐴 → ¬ 𝐴 = ∅))
52	51	con2d 128	. . . . . . . . . . 11 ⊢ (𝐶 ∈ V → (𝐴 = ∅ → ¬ {𝐶} ⊆ 𝐴))
53	52	pm4.71d 664	. . . . . . . . . 10 ⊢ (𝐶 ∈ V → (𝐴 = ∅ ↔ (𝐴 = ∅ ∧ ¬ {𝐶} ⊆ 𝐴)))
54		eqimss2 3621	. . . . . . . . . . . 12 ⊢ (𝐴 = {𝐶} → {𝐶} ⊆ 𝐴)
55		iman 439	. . . . . . . . . . . 12 ⊢ ((𝐴 = {𝐶} → {𝐶} ⊆ 𝐴) ↔ ¬ (𝐴 = {𝐶} ∧ ¬ {𝐶} ⊆ 𝐴))
56	54, 55	mpbi 219	. . . . . . . . . . 11 ⊢ ¬ (𝐴 = {𝐶} ∧ ¬ {𝐶} ⊆ 𝐴)
57	56	biorfi 421	. . . . . . . . . 10 ⊢ ((𝐴 = ∅ ∧ ¬ {𝐶} ⊆ 𝐴) ↔ ((𝐴 = ∅ ∧ ¬ {𝐶} ⊆ 𝐴) ∨ (𝐴 = {𝐶} ∧ ¬ {𝐶} ⊆ 𝐴)))
58	53, 57	syl6rbb 276	. . . . . . . . 9 ⊢ (𝐶 ∈ V → (((𝐴 = ∅ ∧ ¬ {𝐶} ⊆ 𝐴) ∨ (𝐴 = {𝐶} ∧ ¬ {𝐶} ⊆ 𝐴)) ↔ 𝐴 = ∅))
59	49, 58	syl5bb 271	. . . . . . . 8 ⊢ (𝐶 ∈ V → (((𝐴 = ∅ ∨ 𝐴 = {𝐶}) ∧ ¬ {𝐶} ⊆ 𝐴) ↔ 𝐴 = ∅))
60	48, 59	bitrd 267	. . . . . . 7 ⊢ (𝐶 ∈ V → ((𝐴 ⊆ {𝐶} ∧ ¬ {𝐶} ⊆ 𝐴) ↔ 𝐴 = ∅))
61	20	bicomi 213	. . . . . . . 8 ⊢ ((𝐵 ⊆ {𝐶} ∧ {𝐶} ⊆ 𝐵) ↔ 𝐵 = {𝐶})
62	61	a1i 11	. . . . . . 7 ⊢ (𝐶 ∈ V → ((𝐵 ⊆ {𝐶} ∧ {𝐶} ⊆ 𝐵) ↔ 𝐵 = {𝐶}))
63	60, 62	anbi12d 743	. . . . . 6 ⊢ (𝐶 ∈ V → (((𝐴 ⊆ {𝐶} ∧ ¬ {𝐶} ⊆ 𝐴) ∧ (𝐵 ⊆ {𝐶} ∧ {𝐶} ⊆ 𝐵)) ↔ (𝐴 = ∅ ∧ 𝐵 = {𝐶})))
64	45, 63	syl5bb 271	. . . . 5 ⊢ (𝐶 ∈ V → (((𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}) ∧ (¬ {𝐶} ⊆ 𝐴 ∧ {𝐶} ⊆ 𝐵)) ↔ (𝐴 = ∅ ∧ 𝐵 = {𝐶})))
65	24, 44, 64	3orbi123d 1390	. . . 4 ⊢ (𝐶 ∈ V → ((((𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}) ∧ ({𝐶} ⊆ 𝐴 ∧ {𝐶} ⊆ 𝐵)) ∨ ((𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}) ∧ ({𝐶} ⊆ 𝐴 ∧ ¬ {𝐶} ⊆ 𝐵)) ∨ ((𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}) ∧ (¬ {𝐶} ⊆ 𝐴 ∧ {𝐶} ⊆ 𝐵))) ↔ ((𝐴 = {𝐶} ∧ 𝐵 = {𝐶}) ∨ (𝐴 = {𝐶} ∧ 𝐵 = ∅) ∨ (𝐴 = ∅ ∧ 𝐵 = {𝐶}))))
66	17, 65	syl5bb 271	. . 3 ⊢ (𝐶 ∈ V → (((𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}) ∧ ({𝐶} ⊆ 𝐴 ∨ {𝐶} ⊆ 𝐵)) ↔ ((𝐴 = {𝐶} ∧ 𝐵 = {𝐶}) ∨ (𝐴 = {𝐶} ∧ 𝐵 = ∅) ∨ (𝐴 = ∅ ∧ 𝐵 = {𝐶}))))
67	2, 13, 66	3bitrd 293	. 2 ⊢ (𝐶 ∈ V → ((𝐴 ∪ 𝐵) = {𝐶} ↔ ((𝐴 = {𝐶} ∧ 𝐵 = {𝐶}) ∨ (𝐴 = {𝐶} ∧ 𝐵 = ∅) ∨ (𝐴 = ∅ ∧ 𝐵 = {𝐶}))))
68		snprc 4197	. . . . 5 ⊢ (¬ 𝐶 ∈ V ↔ {𝐶} = ∅)
69	68	biimpi 205	. . . 4 ⊢ (¬ 𝐶 ∈ V → {𝐶} = ∅)
70	69	eqeq2d 2620	. . 3 ⊢ (¬ 𝐶 ∈ V → ((𝐴 ∪ 𝐵) = {𝐶} ↔ (𝐴 ∪ 𝐵) = ∅))
71	69	eqeq2d 2620	. . . . . . . 8 ⊢ (¬ 𝐶 ∈ V → (𝐴 = {𝐶} ↔ 𝐴 = ∅))
72	69	eqeq2d 2620	. . . . . . . 8 ⊢ (¬ 𝐶 ∈ V → (𝐵 = {𝐶} ↔ 𝐵 = ∅))
73	71, 72	anbi12d 743	. . . . . . 7 ⊢ (¬ 𝐶 ∈ V → ((𝐴 = {𝐶} ∧ 𝐵 = {𝐶}) ↔ (𝐴 = ∅ ∧ 𝐵 = ∅)))
74	71	anbi1d 737	. . . . . . 7 ⊢ (¬ 𝐶 ∈ V → ((𝐴 = {𝐶} ∧ 𝐵 = ∅) ↔ (𝐴 = ∅ ∧ 𝐵 = ∅)))
75	73, 74	orbi12d 742	. . . . . 6 ⊢ (¬ 𝐶 ∈ V → (((𝐴 = {𝐶} ∧ 𝐵 = {𝐶}) ∨ (𝐴 = {𝐶} ∧ 𝐵 = ∅)) ↔ ((𝐴 = ∅ ∧ 𝐵 = ∅) ∨ (𝐴 = ∅ ∧ 𝐵 = ∅))))
76	72	anbi2d 736	. . . . . 6 ⊢ (¬ 𝐶 ∈ V → ((𝐴 = ∅ ∧ 𝐵 = {𝐶}) ↔ (𝐴 = ∅ ∧ 𝐵 = ∅)))
77	75, 76	orbi12d 742	. . . . 5 ⊢ (¬ 𝐶 ∈ V → ((((𝐴 = {𝐶} ∧ 𝐵 = {𝐶}) ∨ (𝐴 = {𝐶} ∧ 𝐵 = ∅)) ∨ (𝐴 = ∅ ∧ 𝐵 = {𝐶})) ↔ (((𝐴 = ∅ ∧ 𝐵 = ∅) ∨ (𝐴 = ∅ ∧ 𝐵 = ∅)) ∨ (𝐴 = ∅ ∧ 𝐵 = ∅))))
78		pm4.25 536	. . . . . 6 ⊢ ((𝐴 = ∅ ∧ 𝐵 = ∅) ↔ ((𝐴 = ∅ ∧ 𝐵 = ∅) ∨ (𝐴 = ∅ ∧ 𝐵 = ∅)))
79	78	orbi1i 541	. . . . . 6 ⊢ (((𝐴 = ∅ ∧ 𝐵 = ∅) ∨ (𝐴 = ∅ ∧ 𝐵 = ∅)) ↔ (((𝐴 = ∅ ∧ 𝐵 = ∅) ∨ (𝐴 = ∅ ∧ 𝐵 = ∅)) ∨ (𝐴 = ∅ ∧ 𝐵 = ∅)))
80	78, 79	bitri 263	. . . . 5 ⊢ ((𝐴 = ∅ ∧ 𝐵 = ∅) ↔ (((𝐴 = ∅ ∧ 𝐵 = ∅) ∨ (𝐴 = ∅ ∧ 𝐵 = ∅)) ∨ (𝐴 = ∅ ∧ 𝐵 = ∅)))
81	77, 80	syl6rbbr 278	. . . 4 ⊢ (¬ 𝐶 ∈ V → ((𝐴 = ∅ ∧ 𝐵 = ∅) ↔ (((𝐴 = {𝐶} ∧ 𝐵 = {𝐶}) ∨ (𝐴 = {𝐶} ∧ 𝐵 = ∅)) ∨ (𝐴 = ∅ ∧ 𝐵 = {𝐶}))))
82		un00 3963	. . . . 5 ⊢ ((𝐴 = ∅ ∧ 𝐵 = ∅) ↔ (𝐴 ∪ 𝐵) = ∅)
83	82	bicomi 213	. . . 4 ⊢ ((𝐴 ∪ 𝐵) = ∅ ↔ (𝐴 = ∅ ∧ 𝐵 = ∅))
84		df-3or 1032	. . . 4 ⊢ (((𝐴 = {𝐶} ∧ 𝐵 = {𝐶}) ∨ (𝐴 = {𝐶} ∧ 𝐵 = ∅) ∨ (𝐴 = ∅ ∧ 𝐵 = {𝐶})) ↔ (((𝐴 = {𝐶} ∧ 𝐵 = {𝐶}) ∨ (𝐴 = {𝐶} ∧ 𝐵 = ∅)) ∨ (𝐴 = ∅ ∧ 𝐵 = {𝐶})))
85	81, 83, 84	3bitr4g 302	. . 3 ⊢ (¬ 𝐶 ∈ V → ((𝐴 ∪ 𝐵) = ∅ ↔ ((𝐴 = {𝐶} ∧ 𝐵 = {𝐶}) ∨ (𝐴 = {𝐶} ∧ 𝐵 = ∅) ∨ (𝐴 = ∅ ∧ 𝐵 = {𝐶}))))
86	70, 85	bitrd 267	. 2 ⊢ (¬ 𝐶 ∈ V → ((𝐴 ∪ 𝐵) = {𝐶} ↔ ((𝐴 = {𝐶} ∧ 𝐵 = {𝐶}) ∨ (𝐴 = {𝐶} ∧ 𝐵 = ∅) ∨ (𝐴 = ∅ ∧ 𝐵 = {𝐶}))))
87	67, 86	pm2.61i 175	1 ⊢ ((𝐴 ∪ 𝐵) = {𝐶} ↔ ((𝐴 = {𝐶} ∧ 𝐵 = {𝐶}) ∨ (𝐴 = {𝐶} ∧ 𝐵 = ∅) ∨ (𝐴 = ∅ ∧ 𝐵 = {𝐶})))

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