Theorem uneqsn 38321

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 3618	. . . 4 ⊢ ((𝐴 ∪ 𝐵) = {𝐶} ↔ ((𝐴 ∪ 𝐵) ⊆ {𝐶} ∧ {𝐶} ⊆ (𝐴 ∪ 𝐵)))
2	1	a1i 11	. . 3 ⊢ (𝐶 ∈ V → ((𝐴 ∪ 𝐵) = {𝐶} ↔ ((𝐴 ∪ 𝐵) ⊆ {𝐶} ∧ {𝐶} ⊆ (𝐴 ∪ 𝐵))))
3		unss 3787	. . . . . 6 ⊢ ((𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}) ↔ (𝐴 ∪ 𝐵) ⊆ {𝐶})
4	3	bicomi 214	. . . . 5 ⊢ ((𝐴 ∪ 𝐵) ⊆ {𝐶} ↔ (𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}))
5	4	a1i 11	. . . 4 ⊢ (𝐶 ∈ V → ((𝐴 ∪ 𝐵) ⊆ {𝐶} ↔ (𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶})))
6		elun 3753	. . . . . 6 ⊢ (𝐶 ∈ (𝐴 ∪ 𝐵) ↔ (𝐶 ∈ 𝐴 ∨ 𝐶 ∈ 𝐵))
7		snssg 4327	. . . . . . 7 ⊢ (𝐶 ∈ V → (𝐶 ∈ 𝐴 ↔ {𝐶} ⊆ 𝐴))
8		snssg 4327	. . . . . . 7 ⊢ (𝐶 ∈ V → (𝐶 ∈ 𝐵 ↔ {𝐶} ⊆ 𝐵))
9	7, 8	orbi12d 746	. . . . . 6 ⊢ (𝐶 ∈ V → ((𝐶 ∈ 𝐴 ∨ 𝐶 ∈ 𝐵) ↔ ({𝐶} ⊆ 𝐴 ∨ {𝐶} ⊆ 𝐵)))
10	6, 9	syl5rbb 273	. . . . 5 ⊢ (𝐶 ∈ V → (({𝐶} ⊆ 𝐴 ∨ {𝐶} ⊆ 𝐵) ↔ 𝐶 ∈ (𝐴 ∪ 𝐵)))
11		snssg 4327	. . . . 5 ⊢ (𝐶 ∈ V → (𝐶 ∈ (𝐴 ∪ 𝐵) ↔ {𝐶} ⊆ (𝐴 ∪ 𝐵)))
12	10, 11	bitr2d 269	. . . 4 ⊢ (𝐶 ∈ V → ({𝐶} ⊆ (𝐴 ∪ 𝐵) ↔ ({𝐶} ⊆ 𝐴 ∨ {𝐶} ⊆ 𝐵)))
13	5, 12	anbi12d 747	. . 3 ⊢ (𝐶 ∈ V → (((𝐴 ∪ 𝐵) ⊆ {𝐶} ∧ {𝐶} ⊆ (𝐴 ∪ 𝐵)) ↔ ((𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}) ∧ ({𝐶} ⊆ 𝐴 ∨ {𝐶} ⊆ 𝐵))))
14		or3or 38319	. . . . . 6 ⊢ (({𝐶} ⊆ 𝐴 ∨ {𝐶} ⊆ 𝐵) ↔ (({𝐶} ⊆ 𝐴 ∧ {𝐶} ⊆ 𝐵) ∨ ({𝐶} ⊆ 𝐴 ∧ ¬ {𝐶} ⊆ 𝐵) ∨ (¬ {𝐶} ⊆ 𝐴 ∧ {𝐶} ⊆ 𝐵)))
15	14	anbi2i 730	. . . . 5 ⊢ (((𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}) ∧ ({𝐶} ⊆ 𝐴 ∨ {𝐶} ⊆ 𝐵)) ↔ ((𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}) ∧ (({𝐶} ⊆ 𝐴 ∧ {𝐶} ⊆ 𝐵) ∨ ({𝐶} ⊆ 𝐴 ∧ ¬ {𝐶} ⊆ 𝐵) ∨ (¬ {𝐶} ⊆ 𝐴 ∧ {𝐶} ⊆ 𝐵))))
16		andi3or 38320	. . . . 5 ⊢ (((𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}) ∧ (({𝐶} ⊆ 𝐴 ∧ {𝐶} ⊆ 𝐵) ∨ ({𝐶} ⊆ 𝐴 ∧ ¬ {𝐶} ⊆ 𝐵) ∨ (¬ {𝐶} ⊆ 𝐴 ∧ {𝐶} ⊆ 𝐵))) ↔ (((𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}) ∧ ({𝐶} ⊆ 𝐴 ∧ {𝐶} ⊆ 𝐵)) ∨ ((𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}) ∧ ({𝐶} ⊆ 𝐴 ∧ ¬ {𝐶} ⊆ 𝐵)) ∨ ((𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}) ∧ (¬ {𝐶} ⊆ 𝐴 ∧ {𝐶} ⊆ 𝐵))))
17	15, 16	bitri 264	. . . 4 ⊢ (((𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}) ∧ ({𝐶} ⊆ 𝐴 ∨ {𝐶} ⊆ 𝐵)) ↔ (((𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}) ∧ ({𝐶} ⊆ 𝐴 ∧ {𝐶} ⊆ 𝐵)) ∨ ((𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}) ∧ ({𝐶} ⊆ 𝐴 ∧ ¬ {𝐶} ⊆ 𝐵)) ∨ ((𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}) ∧ (¬ {𝐶} ⊆ 𝐴 ∧ {𝐶} ⊆ 𝐵))))
18		an4 865	. . . . . . 7 ⊢ (((𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}) ∧ ({𝐶} ⊆ 𝐴 ∧ {𝐶} ⊆ 𝐵)) ↔ ((𝐴 ⊆ {𝐶} ∧ {𝐶} ⊆ 𝐴) ∧ (𝐵 ⊆ {𝐶} ∧ {𝐶} ⊆ 𝐵)))
19		eqss 3618	. . . . . . . . 9 ⊢ (𝐴 = {𝐶} ↔ (𝐴 ⊆ {𝐶} ∧ {𝐶} ⊆ 𝐴))
20		eqss 3618	. . . . . . . . 9 ⊢ (𝐵 = {𝐶} ↔ (𝐵 ⊆ {𝐶} ∧ {𝐶} ⊆ 𝐵))
21	19, 20	anbi12i 733	. . . . . . . 8 ⊢ ((𝐴 = {𝐶} ∧ 𝐵 = {𝐶}) ↔ ((𝐴 ⊆ {𝐶} ∧ {𝐶} ⊆ 𝐴) ∧ (𝐵 ⊆ {𝐶} ∧ {𝐶} ⊆ 𝐵)))
22	21	bicomi 214	. . . . . . 7 ⊢ (((𝐴 ⊆ {𝐶} ∧ {𝐶} ⊆ 𝐴) ∧ (𝐵 ⊆ {𝐶} ∧ {𝐶} ⊆ 𝐵)) ↔ (𝐴 = {𝐶} ∧ 𝐵 = {𝐶}))
23	18, 22	bitri 264	. . . . . 6 ⊢ (((𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}) ∧ ({𝐶} ⊆ 𝐴 ∧ {𝐶} ⊆ 𝐵)) ↔ (𝐴 = {𝐶} ∧ 𝐵 = {𝐶}))
24	23	a1i 11	. . . . 5 ⊢ (𝐶 ∈ V → (((𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}) ∧ ({𝐶} ⊆ 𝐴 ∧ {𝐶} ⊆ 𝐵)) ↔ (𝐴 = {𝐶} ∧ 𝐵 = {𝐶})))
25		an4 865	. . . . . 6 ⊢ (((𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}) ∧ ({𝐶} ⊆ 𝐴 ∧ ¬ {𝐶} ⊆ 𝐵)) ↔ ((𝐴 ⊆ {𝐶} ∧ {𝐶} ⊆ 𝐴) ∧ (𝐵 ⊆ {𝐶} ∧ ¬ {𝐶} ⊆ 𝐵)))
26	19	bicomi 214	. . . . . . . 8 ⊢ ((𝐴 ⊆ {𝐶} ∧ {𝐶} ⊆ 𝐴) ↔ 𝐴 = {𝐶})
27	26	a1i 11	. . . . . . 7 ⊢ (𝐶 ∈ V → ((𝐴 ⊆ {𝐶} ∧ {𝐶} ⊆ 𝐴) ↔ 𝐴 = {𝐶}))
28		sssn 4358	. . . . . . . . . 10 ⊢ (𝐵 ⊆ {𝐶} ↔ (𝐵 = ∅ ∨ 𝐵 = {𝐶}))
29	28	a1i 11	. . . . . . . . 9 ⊢ (𝐶 ∈ V → (𝐵 ⊆ {𝐶} ↔ (𝐵 = ∅ ∨ 𝐵 = {𝐶})))
30	29	anbi1d 741	. . . . . . . 8 ⊢ (𝐶 ∈ V → ((𝐵 ⊆ {𝐶} ∧ ¬ {𝐶} ⊆ 𝐵) ↔ ((𝐵 = ∅ ∨ 𝐵 = {𝐶}) ∧ ¬ {𝐶} ⊆ 𝐵)))
31		andir 912	. . . . . . . . 9 ⊢ (((𝐵 = ∅ ∨ 𝐵 = {𝐶}) ∧ ¬ {𝐶} ⊆ 𝐵) ↔ ((𝐵 = ∅ ∧ ¬ {𝐶} ⊆ 𝐵) ∨ (𝐵 = {𝐶} ∧ ¬ {𝐶} ⊆ 𝐵)))
32		n0i 3920	. . . . . . . . . . . . 13 ⊢ (𝐶 ∈ 𝐵 → ¬ 𝐵 = ∅)
33	8, 32	syl6bir 244	. . . . . . . . . . . 12 ⊢ (𝐶 ∈ V → ({𝐶} ⊆ 𝐵 → ¬ 𝐵 = ∅))
34	33	con2d 129	. . . . . . . . . . 11 ⊢ (𝐶 ∈ V → (𝐵 = ∅ → ¬ {𝐶} ⊆ 𝐵))
35	34	pm4.71d 666	. . . . . . . . . 10 ⊢ (𝐶 ∈ V → (𝐵 = ∅ ↔ (𝐵 = ∅ ∧ ¬ {𝐶} ⊆ 𝐵)))
36		eqimss2 3658	. . . . . . . . . . . 12 ⊢ (𝐵 = {𝐶} → {𝐶} ⊆ 𝐵)
37		iman 440	. . . . . . . . . . . 12 ⊢ ((𝐵 = {𝐶} → {𝐶} ⊆ 𝐵) ↔ ¬ (𝐵 = {𝐶} ∧ ¬ {𝐶} ⊆ 𝐵))
38	36, 37	mpbi 220	. . . . . . . . . . 11 ⊢ ¬ (𝐵 = {𝐶} ∧ ¬ {𝐶} ⊆ 𝐵)
39	38	biorfi 422	. . . . . . . . . 10 ⊢ ((𝐵 = ∅ ∧ ¬ {𝐶} ⊆ 𝐵) ↔ ((𝐵 = ∅ ∧ ¬ {𝐶} ⊆ 𝐵) ∨ (𝐵 = {𝐶} ∧ ¬ {𝐶} ⊆ 𝐵)))
40	35, 39	syl6rbb 277	. . . . . . . . 9 ⊢ (𝐶 ∈ V → (((𝐵 = ∅ ∧ ¬ {𝐶} ⊆ 𝐵) ∨ (𝐵 = {𝐶} ∧ ¬ {𝐶} ⊆ 𝐵)) ↔ 𝐵 = ∅))
41	31, 40	syl5bb 272	. . . . . . . 8 ⊢ (𝐶 ∈ V → (((𝐵 = ∅ ∨ 𝐵 = {𝐶}) ∧ ¬ {𝐶} ⊆ 𝐵) ↔ 𝐵 = ∅))
42	30, 41	bitrd 268	. . . . . . 7 ⊢ (𝐶 ∈ V → ((𝐵 ⊆ {𝐶} ∧ ¬ {𝐶} ⊆ 𝐵) ↔ 𝐵 = ∅))
43	27, 42	anbi12d 747	. . . . . 6 ⊢ (𝐶 ∈ V → (((𝐴 ⊆ {𝐶} ∧ {𝐶} ⊆ 𝐴) ∧ (𝐵 ⊆ {𝐶} ∧ ¬ {𝐶} ⊆ 𝐵)) ↔ (𝐴 = {𝐶} ∧ 𝐵 = ∅)))
44	25, 43	syl5bb 272	. . . . 5 ⊢ (𝐶 ∈ V → (((𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}) ∧ ({𝐶} ⊆ 𝐴 ∧ ¬ {𝐶} ⊆ 𝐵)) ↔ (𝐴 = {𝐶} ∧ 𝐵 = ∅)))
45		an4 865	. . . . . 6 ⊢ (((𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}) ∧ (¬ {𝐶} ⊆ 𝐴 ∧ {𝐶} ⊆ 𝐵)) ↔ ((𝐴 ⊆ {𝐶} ∧ ¬ {𝐶} ⊆ 𝐴) ∧ (𝐵 ⊆ {𝐶} ∧ {𝐶} ⊆ 𝐵)))
46		sssn 4358	. . . . . . . . . 10 ⊢ (𝐴 ⊆ {𝐶} ↔ (𝐴 = ∅ ∨ 𝐴 = {𝐶}))
47	46	a1i 11	. . . . . . . . 9 ⊢ (𝐶 ∈ V → (𝐴 ⊆ {𝐶} ↔ (𝐴 = ∅ ∨ 𝐴 = {𝐶})))
48	47	anbi1d 741	. . . . . . . 8 ⊢ (𝐶 ∈ V → ((𝐴 ⊆ {𝐶} ∧ ¬ {𝐶} ⊆ 𝐴) ↔ ((𝐴 = ∅ ∨ 𝐴 = {𝐶}) ∧ ¬ {𝐶} ⊆ 𝐴)))
49		andir 912	. . . . . . . . 9 ⊢ (((𝐴 = ∅ ∨ 𝐴 = {𝐶}) ∧ ¬ {𝐶} ⊆ 𝐴) ↔ ((𝐴 = ∅ ∧ ¬ {𝐶} ⊆ 𝐴) ∨ (𝐴 = {𝐶} ∧ ¬ {𝐶} ⊆ 𝐴)))
50		n0i 3920	. . . . . . . . . . . . 13 ⊢ (𝐶 ∈ 𝐴 → ¬ 𝐴 = ∅)
51	7, 50	syl6bir 244	. . . . . . . . . . . 12 ⊢ (𝐶 ∈ V → ({𝐶} ⊆ 𝐴 → ¬ 𝐴 = ∅))
52	51	con2d 129	. . . . . . . . . . 11 ⊢ (𝐶 ∈ V → (𝐴 = ∅ → ¬ {𝐶} ⊆ 𝐴))
53	52	pm4.71d 666	. . . . . . . . . 10 ⊢ (𝐶 ∈ V → (𝐴 = ∅ ↔ (𝐴 = ∅ ∧ ¬ {𝐶} ⊆ 𝐴)))
54		eqimss2 3658	. . . . . . . . . . . 12 ⊢ (𝐴 = {𝐶} → {𝐶} ⊆ 𝐴)
55		iman 440	. . . . . . . . . . . 12 ⊢ ((𝐴 = {𝐶} → {𝐶} ⊆ 𝐴) ↔ ¬ (𝐴 = {𝐶} ∧ ¬ {𝐶} ⊆ 𝐴))
56	54, 55	mpbi 220	. . . . . . . . . . 11 ⊢ ¬ (𝐴 = {𝐶} ∧ ¬ {𝐶} ⊆ 𝐴)
57	56	biorfi 422	. . . . . . . . . 10 ⊢ ((𝐴 = ∅ ∧ ¬ {𝐶} ⊆ 𝐴) ↔ ((𝐴 = ∅ ∧ ¬ {𝐶} ⊆ 𝐴) ∨ (𝐴 = {𝐶} ∧ ¬ {𝐶} ⊆ 𝐴)))
58	53, 57	syl6rbb 277	. . . . . . . . 9 ⊢ (𝐶 ∈ V → (((𝐴 = ∅ ∧ ¬ {𝐶} ⊆ 𝐴) ∨ (𝐴 = {𝐶} ∧ ¬ {𝐶} ⊆ 𝐴)) ↔ 𝐴 = ∅))
59	49, 58	syl5bb 272	. . . . . . . 8 ⊢ (𝐶 ∈ V → (((𝐴 = ∅ ∨ 𝐴 = {𝐶}) ∧ ¬ {𝐶} ⊆ 𝐴) ↔ 𝐴 = ∅))
60	48, 59	bitrd 268	. . . . . . 7 ⊢ (𝐶 ∈ V → ((𝐴 ⊆ {𝐶} ∧ ¬ {𝐶} ⊆ 𝐴) ↔ 𝐴 = ∅))
61	20	bicomi 214	. . . . . . . 8 ⊢ ((𝐵 ⊆ {𝐶} ∧ {𝐶} ⊆ 𝐵) ↔ 𝐵 = {𝐶})
62	61	a1i 11	. . . . . . 7 ⊢ (𝐶 ∈ V → ((𝐵 ⊆ {𝐶} ∧ {𝐶} ⊆ 𝐵) ↔ 𝐵 = {𝐶}))
63	60, 62	anbi12d 747	. . . . . 6 ⊢ (𝐶 ∈ V → (((𝐴 ⊆ {𝐶} ∧ ¬ {𝐶} ⊆ 𝐴) ∧ (𝐵 ⊆ {𝐶} ∧ {𝐶} ⊆ 𝐵)) ↔ (𝐴 = ∅ ∧ 𝐵 = {𝐶})))
64	45, 63	syl5bb 272	. . . . 5 ⊢ (𝐶 ∈ V → (((𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}) ∧ (¬ {𝐶} ⊆ 𝐴 ∧ {𝐶} ⊆ 𝐵)) ↔ (𝐴 = ∅ ∧ 𝐵 = {𝐶})))
65	24, 44, 64	3orbi123d 1398	. . . 4 ⊢ (𝐶 ∈ V → ((((𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}) ∧ ({𝐶} ⊆ 𝐴 ∧ {𝐶} ⊆ 𝐵)) ∨ ((𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}) ∧ ({𝐶} ⊆ 𝐴 ∧ ¬ {𝐶} ⊆ 𝐵)) ∨ ((𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}) ∧ (¬ {𝐶} ⊆ 𝐴 ∧ {𝐶} ⊆ 𝐵))) ↔ ((𝐴 = {𝐶} ∧ 𝐵 = {𝐶}) ∨ (𝐴 = {𝐶} ∧ 𝐵 = ∅) ∨ (𝐴 = ∅ ∧ 𝐵 = {𝐶}))))
66	17, 65	syl5bb 272	. . 3 ⊢ (𝐶 ∈ V → (((𝐴 ⊆ {𝐶} ∧ 𝐵 ⊆ {𝐶}) ∧ ({𝐶} ⊆ 𝐴 ∨ {𝐶} ⊆ 𝐵)) ↔ ((𝐴 = {𝐶} ∧ 𝐵 = {𝐶}) ∨ (𝐴 = {𝐶} ∧ 𝐵 = ∅) ∨ (𝐴 = ∅ ∧ 𝐵 = {𝐶}))))
67	2, 13, 66	3bitrd 294	. 2 ⊢ (𝐶 ∈ V → ((𝐴 ∪ 𝐵) = {𝐶} ↔ ((𝐴 = {𝐶} ∧ 𝐵 = {𝐶}) ∨ (𝐴 = {𝐶} ∧ 𝐵 = ∅) ∨ (𝐴 = ∅ ∧ 𝐵 = {𝐶}))))
68		snprc 4253	. . . . 5 ⊢ (¬ 𝐶 ∈ V ↔ {𝐶} = ∅)
69	68	biimpi 206	. . . 4 ⊢ (¬ 𝐶 ∈ V → {𝐶} = ∅)
70	69	eqeq2d 2632	. . 3 ⊢ (¬ 𝐶 ∈ V → ((𝐴 ∪ 𝐵) = {𝐶} ↔ (𝐴 ∪ 𝐵) = ∅))
71	69	eqeq2d 2632	. . . . . . . 8 ⊢ (¬ 𝐶 ∈ V → (𝐴 = {𝐶} ↔ 𝐴 = ∅))
72	69	eqeq2d 2632	. . . . . . . 8 ⊢ (¬ 𝐶 ∈ V → (𝐵 = {𝐶} ↔ 𝐵 = ∅))
73	71, 72	anbi12d 747	. . . . . . 7 ⊢ (¬ 𝐶 ∈ V → ((𝐴 = {𝐶} ∧ 𝐵 = {𝐶}) ↔ (𝐴 = ∅ ∧ 𝐵 = ∅)))
74	71	anbi1d 741	. . . . . . 7 ⊢ (¬ 𝐶 ∈ V → ((𝐴 = {𝐶} ∧ 𝐵 = ∅) ↔ (𝐴 = ∅ ∧ 𝐵 = ∅)))
75	73, 74	orbi12d 746	. . . . . 6 ⊢ (¬ 𝐶 ∈ V → (((𝐴 = {𝐶} ∧ 𝐵 = {𝐶}) ∨ (𝐴 = {𝐶} ∧ 𝐵 = ∅)) ↔ ((𝐴 = ∅ ∧ 𝐵 = ∅) ∨ (𝐴 = ∅ ∧ 𝐵 = ∅))))
76	72	anbi2d 740	. . . . . 6 ⊢ (¬ 𝐶 ∈ V → ((𝐴 = ∅ ∧ 𝐵 = {𝐶}) ↔ (𝐴 = ∅ ∧ 𝐵 = ∅)))
77	75, 76	orbi12d 746	. . . . 5 ⊢ (¬ 𝐶 ∈ V → ((((𝐴 = {𝐶} ∧ 𝐵 = {𝐶}) ∨ (𝐴 = {𝐶} ∧ 𝐵 = ∅)) ∨ (𝐴 = ∅ ∧ 𝐵 = {𝐶})) ↔ (((𝐴 = ∅ ∧ 𝐵 = ∅) ∨ (𝐴 = ∅ ∧ 𝐵 = ∅)) ∨ (𝐴 = ∅ ∧ 𝐵 = ∅))))
78		pm4.25 537	. . . . . 6 ⊢ ((𝐴 = ∅ ∧ 𝐵 = ∅) ↔ ((𝐴 = ∅ ∧ 𝐵 = ∅) ∨ (𝐴 = ∅ ∧ 𝐵 = ∅)))
79	78	orbi1i 542	. . . . . 6 ⊢ (((𝐴 = ∅ ∧ 𝐵 = ∅) ∨ (𝐴 = ∅ ∧ 𝐵 = ∅)) ↔ (((𝐴 = ∅ ∧ 𝐵 = ∅) ∨ (𝐴 = ∅ ∧ 𝐵 = ∅)) ∨ (𝐴 = ∅ ∧ 𝐵 = ∅)))
80	78, 79	bitri 264	. . . . 5 ⊢ ((𝐴 = ∅ ∧ 𝐵 = ∅) ↔ (((𝐴 = ∅ ∧ 𝐵 = ∅) ∨ (𝐴 = ∅ ∧ 𝐵 = ∅)) ∨ (𝐴 = ∅ ∧ 𝐵 = ∅)))
81	77, 80	syl6rbbr 279	. . . 4 ⊢ (¬ 𝐶 ∈ V → ((𝐴 = ∅ ∧ 𝐵 = ∅) ↔ (((𝐴 = {𝐶} ∧ 𝐵 = {𝐶}) ∨ (𝐴 = {𝐶} ∧ 𝐵 = ∅)) ∨ (𝐴 = ∅ ∧ 𝐵 = {𝐶}))))
82		un00 4011	. . . . 5 ⊢ ((𝐴 = ∅ ∧ 𝐵 = ∅) ↔ (𝐴 ∪ 𝐵) = ∅)
83	82	bicomi 214	. . . 4 ⊢ ((𝐴 ∪ 𝐵) = ∅ ↔ (𝐴 = ∅ ∧ 𝐵 = ∅))
84		df-3or 1038	. . . 4 ⊢ (((𝐴 = {𝐶} ∧ 𝐵 = {𝐶}) ∨ (𝐴 = {𝐶} ∧ 𝐵 = ∅) ∨ (𝐴 = ∅ ∧ 𝐵 = {𝐶})) ↔ (((𝐴 = {𝐶} ∧ 𝐵 = {𝐶}) ∨ (𝐴 = {𝐶} ∧ 𝐵 = ∅)) ∨ (𝐴 = ∅ ∧ 𝐵 = {𝐶})))
85	81, 83, 84	3bitr4g 303	. . 3 ⊢ (¬ 𝐶 ∈ V → ((𝐴 ∪ 𝐵) = ∅ ↔ ((𝐴 = {𝐶} ∧ 𝐵 = {𝐶}) ∨ (𝐴 = {𝐶} ∧ 𝐵 = ∅) ∨ (𝐴 = ∅ ∧ 𝐵 = {𝐶}))))
86	70, 85	bitrd 268	. 2 ⊢ (¬ 𝐶 ∈ V → ((𝐴 ∪ 𝐵) = {𝐶} ↔ ((𝐴 = {𝐶} ∧ 𝐵 = {𝐶}) ∨ (𝐴 = {𝐶} ∧ 𝐵 = ∅) ∨ (𝐴 = ∅ ∧ 𝐵 = {𝐶}))))
87	67, 86	pm2.61i 176	1 ⊢ ((𝐴 ∪ 𝐵) = {𝐶} ↔ ((𝐴 = {𝐶} ∧ 𝐵 = {𝐶}) ∨ (𝐴 = {𝐶} ∧ 𝐵 = ∅) ∨ (𝐴 = ∅ ∧ 𝐵 = {𝐶})))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∨ wo 383   ∧ wa 384   ∨ w3o 1036   = wceq 1483   ∈ wcel 1990  Vcvv 3200   ∪ cun 3572   ⊆ wss 3574  ∅c0 3915  {csn 4177

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-xor 1465  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-sn 4178

This theorem is referenced by:  clsk1indlem3  38341