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