Theorem en0ALT

Description: Shorter proof of en0 , depending on ax-pow and ax-un . (Contributed by NM, 27-May-1998) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	en0ALT	|- ( 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	8	enref	|- (/) ~~ (/)
10		breq1	|- ( A = (/) -> ( A ~~ (/) <-> (/) ~~ (/) ) )
11	9 10	mpbiri	|- ( A = (/) -> A ~~ (/) )
12	7 11	impbii	|- ( A ~~ (/) <-> A = (/) )