Theorem en1b 7365

Description: A set is equinumerous to ordinal one iff it is a singleton. (Contributed by Mario Carneiro, 17-Jan-2015.)

Assertion

Ref	Expression
en1b	|- ( A ~~ 1o <-> A = { U. A } )

Proof of Theorem en1b

Dummy variable x is distinct from all other variables.

Step	Hyp	Ref	Expression
1		en1 7364	. . 3 |- ( A ~~ 1o <-> E. x A = { x } )
2		id 22	. . . . 5 |- ( A = { x } -> A = { x } )
3		unieq 4087	. . . . . . 7 |- ( A = { x } -> U. A = U. { x } )
4		vex 2965	. . . . . . . 8 |- x e. _V
5	4	unisn 4094	. . . . . . 7 |- U. { x } = x
6	3, 5	syl6eq 2481	. . . . . 6 |- ( A = { x } -> U. A = x )
7	6	sneqd 3877	. . . . 5 |- ( A = { x } -> { U. A } = { x } )
8	2, 7	eqtr4d 2468	. . . 4 |- ( A = { x } -> A = { U. A } )
9	8	exlimiv 1687	. . 3 |- ( E. x A = { x } -> A = { U. A } )
10	1, 9	sylbi 195	. 2 |- ( A ~~ 1o -> A = { U. A } )
11		id 22	. . 3 |- ( A = { U. A } -> A = { U. A } )
12		snex 4521	. . . . . 6 |- { U. A } e. _V
13	11, 12	syl6eqel 2521	. . . . 5 |- ( A = { U. A } -> A e. _V )
14		uniexg 6366	. . . . 5 |- ( A e. _V -> U. A e. _V )
15	13, 14	syl 16	. . . 4 |- ( A = { U. A } -> U. A e. _V )
16		ensn1g 7362	. . . 4 |- ( U. A e. _V -> { U. A } ~~ 1o )
17	15, 16	syl 16	. . 3 |- ( A = { U. A } -> { U. A } ~~ 1o )
18	11, 17	eqbrtrd 4300	. 2 |- ( A = { U. A } -> A ~~ 1o )
19	10, 18	impbii 188	1 |- ( A ~~ 1o <-> A = { U. A } )

Syntax hints:   <-> wb 184   = wceq 1362   E.wex 1589   e. wcel 1755   _Vcvv 2962   {csn 3865   U.cuni 4079   class class class wbr 4280   1oc1o 6901   ~~ cen 7295

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-8 1757  ax-9 1759  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414  ax-sep 4401  ax-nul 4409  ax-pr 4519  ax-un 6361

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-eu 2258  df-mo 2259  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ne 2598  df-ral 2710  df-rex 2711  df-reu 2712  df-rab 2714  df-v 2964  df-sbc 3176  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-nul 3626  df-if 3780  df-sn 3866  df-pr 3868  df-op 3872  df-uni 4080  df-br 4281  df-opab 4339  df-id 4623  df-suc 4712  df-xp 4833  df-rel 4834  df-cnv 4835  df-co 4836  df-dm 4837  df-rn 4838  df-res 4839  df-ima 4840  df-iota 5369  df-fun 5408  df-fn 5409  df-f 5410  df-f1 5411  df-fo 5412  df-f1o 5413  df-fv 5414  df-1o 6908  df-en 7299

This theorem is referenced by:  en1uniel  7369  sylow2alem2  16096  sylow2a  16097  frgpcyg  17847  ptcmplem3  19467  cnextfvval  19478  cnextcn  19480  minveclem4a  20758  isppw  22336  xrge0tsmsbi  26106