Description: Obsolete version of enfi as of 23-Sep-2024. (Contributed by NM, 22-Aug-2008) (Proof modification is discouraged.) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Assertion | enfiOLD | ⊢ ( 𝐴 ≈ 𝐵 → ( 𝐴 ∈ Fin ↔ 𝐵 ∈ Fin ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | enen1 | ⊢ ( 𝐴 ≈ 𝐵 → ( 𝐴 ≈ 𝑥 ↔ 𝐵 ≈ 𝑥 ) ) | |
2 | 1 | rexbidv | ⊢ ( 𝐴 ≈ 𝐵 → ( ∃ 𝑥 ∈ ω 𝐴 ≈ 𝑥 ↔ ∃ 𝑥 ∈ ω 𝐵 ≈ 𝑥 ) ) |
3 | isfi | ⊢ ( 𝐴 ∈ Fin ↔ ∃ 𝑥 ∈ ω 𝐴 ≈ 𝑥 ) | |
4 | isfi | ⊢ ( 𝐵 ∈ Fin ↔ ∃ 𝑥 ∈ ω 𝐵 ≈ 𝑥 ) | |
5 | 2 3 4 | 3bitr4g | ⊢ ( 𝐴 ≈ 𝐵 → ( 𝐴 ∈ Fin ↔ 𝐵 ∈ Fin ) ) |