uneqsn - Mathbox for Richard Penner

	Mathbox for Richard Penner		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > uneqsn		Structured version Visualization version Unicode version

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 $/\$
3		unss 3787	. . . . . 6 $/\$
4	3	bicomi 214	. . . . 5 $/\$
5	4	a1i 11	. . . 4 $/\$
6		elun 3753	. . . . . 6 $\/$
7		snssg 4327	. . . . . . 7
8		snssg 4327	. . . . . . 7
9	7, 8	orbi12d 746	. . . . . 6 $\/$ $\/$
10	6, 9	syl5rbb 273	. . . . 5 $\/$
11		snssg 4327	. . . . 5
12	10, 11	bitr2d 269	. . . 4 $\/$
13	5, 12	anbi12d 747	. . 3 $/\$ $/\$ $/\$ $\/$
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 $/\$ $/\$ $/\$ $/\$
25		an4 865	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
26	19	bicomi 214	. . . . . . . 8 $/\$
27	26	a1i 11	. . . . . . 7 $/\$
28		sssn 4358	. . . . . . . . . 10 $\/$
29	28	a1i 11	. . . . . . . . 9 $\/$
30	29	anbi1d 741	. . . . . . . 8 $/\$ $\/$ $/\$
31		andir 912	. . . . . . . . 9 $\/$ $/\$ $/\$ $\/$ $/\$
32		n0i 3920	. . . . . . . . . . . . 13
33	8, 32	syl6bir 244	. . . . . . . . . . . 12
34	33	con2d 129	. . . . . . . . . . 11
35	34	pm4.71d 666	. . . . . . . . . 10 $/\$
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 $/\$ $\/$ $/\$
41	31, 40	syl5bb 272	. . . . . . . 8 $\/$ $/\$
42	30, 41	bitrd 268	. . . . . . 7 $/\$
43	27, 42	anbi12d 747	. . . . . 6 $/\$ $/\$ $/\$ $/\$
44	25, 43	syl5bb 272	. . . . 5 $/\$ $/\$ $/\$ $/\$
45		an4 865	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
46		sssn 4358	. . . . . . . . . 10 $\/$
47	46	a1i 11	. . . . . . . . 9 $\/$
48	47	anbi1d 741	. . . . . . . 8 $/\$ $\/$ $/\$
49		andir 912	. . . . . . . . 9 $\/$ $/\$ $/\$ $\/$ $/\$
50		n0i 3920	. . . . . . . . . . . . 13
51	7, 50	syl6bir 244	. . . . . . . . . . . 12
52	51	con2d 129	. . . . . . . . . . 11
53	52	pm4.71d 666	. . . . . . . . . 10 $/\$
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 $/\$ $\/$ $/\$
59	49, 58	syl5bb 272	. . . . . . . 8 $\/$ $/\$
60	48, 59	bitrd 268	. . . . . . 7 $/\$
61	20	bicomi 214	. . . . . . . 8 $/\$
62	61	a1i 11	. . . . . . 7 $/\$
63	60, 62	anbi12d 747	. . . . . 6 $/\$ $/\$ $/\$ $/\$
64	45, 63	syl5bb 272	. . . . 5 $/\$ $/\$ $/\$ $/\$
65	24, 44, 64	3orbi123d 1398	. . . 4 $/\$ $/\$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$
66	17, 65	syl5bb 272	. . 3 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
67	2, 13, 66	3bitrd 294	. 2 $/\$ $\/$ $/\$ $\/$ $/\$
68		snprc 4253	. . . . 5
69	68	biimpi 206	. . . 4
70	69	eqeq2d 2632	. . 3
71	69	eqeq2d 2632	. . . . . . . 8
72	69	eqeq2d 2632	. . . . . . . 8
73	71, 72	anbi12d 747	. . . . . . 7 $/\$ $/\$
74	71	anbi1d 741	. . . . . . 7 $/\$ $/\$
75	73, 74	orbi12d 746	. . . . . 6 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
76	72	anbi2d 740	. . . . . 6 $/\$ $/\$
77	75, 76	orbi12d 746	. . . . 5 $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$
78		pm4.25 537	. . . . . 6 $/\$ $/\$ $\/$ $/\$
79	78	orbi1i 542	. . . . . 6 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$
80	78, 79	bitri 264	. . . . 5 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$
81	77, 80	syl6rbbr 279	. . . 4 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$
82		un00 4011	. . . . 5 $/\$
83	82	bicomi 214	. . . 4 $/\$
84		df-3or 1038	. . . 4 $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$
85	81, 83, 84	3bitr4g 303	. . 3 $/\$ $\/$ $/\$ $\/$ $/\$
86	70, 85	bitrd 268	. 2 $/\$ $\/$ $/\$ $\/$ $/\$
87	67, 86	pm2.61i 176	1 $/\$ $\/$ $/\$ $\/$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 196 $\/$ wo 383 $/\$ wa 384 $\/$ w3o 1036

wceq 1483

wcel 1990

cvv 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

W3C validator