Theorem uniintsn 4514

Description: Two ways to express " A is a singleton." See also en1 8023, en1b 8024, card1 8794, and eusn 4265. (Contributed by NM, 2-Aug-2010.)

Assertion

Ref	Expression
uniintsn	|- ( U. A = |^| A <-> E. x A = { x } )

Distinct variable group:   x, A

Proof of Theorem uniintsn

Dummy variable y is distinct from all other variables.

Step	Hyp	Ref	Expression
1		vn0 3924	. . . . . 6 |- _V =/= (/)
2		inteq 4478	. . . . . . . . . . 11 |- ( A = (/) -> |^| A = |^| (/) )
3		int0 4490	. . . . . . . . . . 11 |- |^| (/) = _V
4	2, 3	syl6eq 2672	. . . . . . . . . 10 |- ( A = (/) -> |^| A = _V )
5	4	adantl 482	. . . . . . . . 9 |- ( ( U. A = |^| A /\ A = (/) ) -> |^| A = _V )
6		unieq 4444	. . . . . . . . . . . 12 |- ( A = (/) -> U. A = U. (/) )
7		uni0 4465	. . . . . . . . . . . 12 |- U. (/) = (/)
8	6, 7	syl6eq 2672	. . . . . . . . . . 11 |- ( A = (/) -> U. A = (/) )
9		eqeq1 2626	. . . . . . . . . . 11 |- ( U. A = |^| A -> ( U. A = (/) <-> |^| A = (/) ) )
10	8, 9	syl5ib 234	. . . . . . . . . 10 |- ( U. A = |^| A -> ( A = (/) -> |^| A = (/) ) )
11	10	imp 445	. . . . . . . . 9 |- ( ( U. A = |^| A /\ A = (/) ) -> |^| A = (/) )
12	5, 11	eqtr3d 2658	. . . . . . . 8 |- ( ( U. A = |^| A /\ A = (/) ) -> _V = (/) )
13	12	ex 450	. . . . . . 7 |- ( U. A = |^| A -> ( A = (/) -> _V = (/) ) )
14	13	necon3d 2815	. . . . . 6 |- ( U. A = |^| A -> ( _V =/= (/) -> A =/= (/) ) )
15	1, 14	mpi 20	. . . . 5 |- ( U. A = |^| A -> A =/= (/) )
16		n0 3931	. . . . 5 |- ( A =/= (/) <-> E. x x e. A )
17	15, 16	sylib 208	. . . 4 |- ( U. A = |^| A -> E. x x e. A )
18		vex 3203	. . . . . . 7 |- x e. _V
19		vex 3203	. . . . . . 7 |- y e. _V
20	18, 19	prss 4351	. . . . . 6 |- ( ( x e. A /\ y e. A ) <-> { x , y } C_ A )
21		uniss 4458	. . . . . . . . . . . . 13 |- ( { x , y } C_ A -> U. { x , y } C_ U. A )
22	21	adantl 482	. . . . . . . . . . . 12 |- ( ( U. A = |^| A /\ { x , y } C_ A ) -> U. { x , y } C_ U. A )
23		simpl 473	. . . . . . . . . . . 12 |- ( ( U. A = |^| A /\ { x , y } C_ A ) -> U. A = |^| A )
24	22, 23	sseqtrd 3641	. . . . . . . . . . 11 |- ( ( U. A = |^| A /\ { x , y } C_ A ) -> U. { x , y } C_ |^| A )
25		intss 4498	. . . . . . . . . . . 12 |- ( { x , y } C_ A -> |^| A C_ |^| { x , y } )
26	25	adantl 482	. . . . . . . . . . 11 |- ( ( U. A = |^| A /\ { x , y } C_ A ) -> |^| A C_ |^| { x , y } )
27	24, 26	sstrd 3613	. . . . . . . . . 10 |- ( ( U. A = |^| A /\ { x , y } C_ A ) -> U. { x , y } C_ |^| { x , y } )
28	18, 19	unipr 4449	. . . . . . . . . 10 |- U. { x , y } = ( x u. y )
29	18, 19	intpr 4510	. . . . . . . . . 10 |- |^| { x , y } = ( x i^i y )
30	27, 28, 29	3sstr3g 3645	. . . . . . . . 9 |- ( ( U. A = |^| A /\ { x , y } C_ A ) -> ( x u. y ) C_ ( x i^i y ) )
31		inss1 3833	. . . . . . . . . 10 |- ( x i^i y ) C_ x
32		ssun1 3776	. . . . . . . . . 10 |- x C_ ( x u. y )
33	31, 32	sstri 3612	. . . . . . . . 9 |- ( x i^i y ) C_ ( x u. y )
34	30, 33	jctir 561	. . . . . . . 8 |- ( ( U. A = |^| A /\ { x , y } C_ A ) -> ( ( x u. y ) C_ ( x i^i y ) /\ ( x i^i y ) C_ ( x u. y ) ) )
35		eqss 3618	. . . . . . . . 9 |- ( ( x u. y ) = ( x i^i y ) <-> ( ( x u. y ) C_ ( x i^i y ) /\ ( x i^i y ) C_ ( x u. y ) ) )
36		uneqin 3878	. . . . . . . . 9 |- ( ( x u. y ) = ( x i^i y ) <-> x = y )
37	35, 36	bitr3i 266	. . . . . . . 8 |- ( ( ( x u. y ) C_ ( x i^i y ) /\ ( x i^i y ) C_ ( x u. y ) ) <-> x = y )
38	34, 37	sylib 208	. . . . . . 7 |- ( ( U. A = |^| A /\ { x , y } C_ A ) -> x = y )
39	38	ex 450	. . . . . 6 |- ( U. A = |^| A -> ( { x , y } C_ A -> x = y ) )
40	20, 39	syl5bi 232	. . . . 5 |- ( U. A = |^| A -> ( ( x e. A /\ y e. A ) -> x = y ) )
41	40	alrimivv 1856	. . . 4 |- ( U. A = |^| A -> A. x A. y ( ( x e. A /\ y e. A ) -> x = y ) )
42	17, 41	jca 554	. . 3 |- ( U. A = |^| A -> ( E. x x e. A /\ A. x A. y ( ( x e. A /\ y e. A ) -> x = y ) ) )
43		euabsn 4261	. . . 4 |- ( E! x x e. A <-> E. x { x | x e. A } = { x } )
44		eleq1 2689	. . . . 5 |- ( x = y -> ( x e. A <-> y e. A ) )
45	44	eu4 2518	. . . 4 |- ( E! x x e. A <-> ( E. x x e. A /\ A. x A. y ( ( x e. A /\ y e. A ) -> x = y ) ) )
46		abid2 2745	. . . . . 6 |- { x | x e. A } = A
47	46	eqeq1i 2627	. . . . 5 |- ( { x | x e. A } = { x } <-> A = { x } )
48	47	exbii 1774	. . . 4 |- ( E. x { x | x e. A } = { x } <-> E. x A = { x } )
49	43, 45, 48	3bitr3i 290	. . 3 |- ( ( E. x x e. A /\ A. x A. y ( ( x e. A /\ y e. A ) -> x = y ) ) <-> E. x A = { x } )
50	42, 49	sylib 208	. 2 |- ( U. A = |^| A -> E. x A = { x } )
51	18	unisn 4451	. . . 4 |- U. { x } = x
52		unieq 4444	. . . 4 |- ( A = { x } -> U. A = U. { x } )
53		inteq 4478	. . . . 5 |- ( A = { x } -> |^| A = |^| { x } )
54	18	intsn 4513	. . . . 5 |- |^| { x } = x
55	53, 54	syl6eq 2672	. . . 4 |- ( A = { x } -> |^| A = x )
56	51, 52, 55	3eqtr4a 2682	. . 3 |- ( A = { x } -> U. A = |^| A )
57	56	exlimiv 1858	. 2 |- ( E. x A = { x } -> U. A = |^| A )
58	50, 57	impbii 199	1 |- ( U. A = |^| A <-> E. x A = { x } )

Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384   A.wal 1481   = wceq 1483   E.wex 1704   e. wcel 1990   E!weu 2470   {cab 2608   =/= wne 2794   _Vcvv 3200   u. cun 3572   i^i cin 3573   C_ wss 3574   (/)c0 3915   {csn 4177   {cpr 4179   U.cuni 4436   |^|cint 4475

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-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-sn 4178  df-pr 4180  df-uni 4437  df-int 4476

This theorem is referenced by:  uniintab  4515