This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 = (/) )