Metamath Proof Explorer


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 ( 𝐴𝐵 → ( 𝐴 ∈ Fin ↔ 𝐵 ∈ Fin ) )

Proof

Step Hyp Ref Expression
1 enen1 ( 𝐴𝐵 → ( 𝐴𝑥𝐵𝑥 ) )
2 1 rexbidv ( 𝐴𝐵 → ( ∃ 𝑥 ∈ ω 𝐴𝑥 ↔ ∃ 𝑥 ∈ ω 𝐵𝑥 ) )
3 isfi ( 𝐴 ∈ Fin ↔ ∃ 𝑥 ∈ ω 𝐴𝑥 )
4 isfi ( 𝐵 ∈ Fin ↔ ∃ 𝑥 ∈ ω 𝐵𝑥 )
5 2 3 4 3bitr4g ( 𝐴𝐵 → ( 𝐴 ∈ Fin ↔ 𝐵 ∈ Fin ) )