This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ A ≈ B → A ∈ Fin ↔ B ∈ Fin

Proof

Step Hyp Ref Expression
1 enen1 ⊢ A ≈ B → A ≈ x ↔ B ≈ x
2 1 rexbidv ⊢ A ≈ B → ∃ x ∈ ω A ≈ x ↔ ∃ x ∈ ω B ≈ x
3 isfi ⊢ A ∈ Fin ↔ ∃ x ∈ ω A ≈ x
4 isfi ⊢ B ∈ Fin ↔ ∃ x ∈ ω B ≈ x
5 2 3 4 3bitr4g ⊢ A ≈ B → A ∈ Fin ↔ B ∈ Fin