Theorem en0

Description: The empty set is equinumerous only to itself. Exercise 1 of TakeutiZaring p. 88. (Contributed by NM, 27-May-1998) Avoid ax-pow . (Revised by BTernaryTau, 31-Jul-2024)

	Ref	Expression
Assertion	en0	|- ( A ~~ (/) <-> A = (/) )

Proof

Step	Hyp	Ref	Expression
1		bren	|- ( A ~~ (/) <-> E. f f : A -1-1-onto-> (/) )
2		f1ocnv	|- ( f : A -1-1-onto-> (/) -> `' f : (/) -1-1-onto-> A )
3		f1o00	|- ( `' f : (/) -1-1-onto-> A <-> ( `' f = (/) /\ A = (/) ) )
4	3	simprbi	|- ( `' f : (/) -1-1-onto-> A -> A = (/) )
5	2 4	syl	|- ( f : A -1-1-onto-> (/) -> A = (/) )
6	5	exlimiv	|- ( E. f f : A -1-1-onto-> (/) -> A = (/) )
7	1 6	sylbi	|- ( A ~~ (/) -> A = (/) )
8		0ex	|- (/) e. _V
9		f1oeq1	|- ( f = (/) -> ( f : (/) -1-1-onto-> (/) <-> (/) : (/) -1-1-onto-> (/) ) )
10		f1o0	|- (/) : (/) -1-1-onto-> (/)
11	8 9 10	ceqsexv2d	|- E. f f : (/) -1-1-onto-> (/)
12		bren	|- ( (/) ~~ (/) <-> E. f f : (/) -1-1-onto-> (/) )
13	11 12	mpbir	|- (/) ~~ (/)
14		breq1	|- ( A = (/) -> ( A ~~ (/) <-> (/) ~~ (/) ) )
15	13 14	mpbiri	|- ( A = (/) -> A ~~ (/) )
16	7 15	impbii	|- ( A ~~ (/) <-> A = (/) )