Theorem enfiALT

Description: Shorter proof of enfi using ax-pow . (Contributed by NM, 22-Aug-2008) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	enfiALT	|- ( A ~~ B -> ( A e. Fin <-> B e. Fin ) )

Proof

Step	Hyp	Ref	Expression
1		enen1	|- ( A ~~ B -> ( A ~~ x <-> B ~~ x ) )
2	1	rexbidv	|- ( A ~~ B -> ( E. x e. _om A ~~ x <-> E. x e. _om B ~~ x ) )
3		isfi	|- ( A e. Fin <-> E. x e. _om A ~~ x )
4		isfi	|- ( B e. Fin <-> E. x e. _om B ~~ x )
5	2 3 4	3bitr4g	|- ( A ~~ B -> ( A e. Fin <-> B e. Fin ) )