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 f f : A 1-1 onto
2 f1ocnv f : A 1-1 onto f -1 : 1-1 onto A
3 f1o00 f -1 : 1-1 onto A f -1 = A =
4 3 simprbi f -1 : 1-1 onto A A =
5 2 4 syl f : A 1-1 onto A =
6 5 exlimiv f f : A 1-1 onto A =
7 1 6 sylbi A A =
8 0ex V
9 8 enref
10 breq1 A = A
11 9 10 mpbiri A = A
12 7 11 impbii A A =