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\approx B\to \left(A\in \mathrm{Fin}\leftrightarrow B\in \mathrm{Fin}\right)$$

Proof

Step	Hyp	Ref	Expression
1		enen1	$$⊢A\approx B\to \left(A\approx x\leftrightarrow B\approx x\right)$$
2	1	rexbidv	$$⊢A\approx B\to \left(\exists x\in \mathrm{\omega }A\approx x\leftrightarrow \exists x\in \mathrm{\omega }B\approx x\right)$$
3		isfi	$$⊢A\in \mathrm{Fin}\leftrightarrow \exists x\in \mathrm{\omega }A\approx x$$
4		isfi	$$⊢B\in \mathrm{Fin}\leftrightarrow \exists x\in \mathrm{\omega }B\approx x$$
5	2 3 4	3bitr4g	$$⊢A\approx B\to \left(A\in \mathrm{Fin}\leftrightarrow B\in \mathrm{Fin}\right)$$