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

Metamath Proof Explorer

Theorem ralimaOLD

Description: Obsolete version of ralima as of 14-Aug-2025. (Contributed by Stefan O'Rear, 21-Jan-2015) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypothesis reximaOLD.x ⊢ ( 𝑥 = ( 𝐹 ‘ 𝑦 ) → ( 𝜑 ↔ 𝜓 ) )
Assertion ralimaOLD ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴 ) → ( ∀ 𝑥 ∈ ( 𝐹 “ 𝐵 ) 𝜑 ↔ ∀ 𝑦 ∈ 𝐵 𝜓 ) )

Proof

Step Hyp Ref Expression
1 reximaOLD.x ⊢ ( 𝑥 = ( 𝐹 ‘ 𝑦 ) → ( 𝜑 ↔ 𝜓 ) )
2 fvexd ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴 ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝐹 ‘ 𝑦 ) ∈ V )
3 fvelimab ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴 ) → ( 𝑥 ∈ ( 𝐹 “ 𝐵 ) ↔ ∃ 𝑦 ∈ 𝐵 ( 𝐹 ‘ 𝑦 ) = 𝑥 ) )
4 eqcom ⊢ ( ( 𝐹 ‘ 𝑦 ) = 𝑥 ↔ 𝑥 = ( 𝐹 ‘ 𝑦 ) )
5 4 rexbii ⊢ ( ∃ 𝑦 ∈ 𝐵 ( 𝐹 ‘ 𝑦 ) = 𝑥 ↔ ∃ 𝑦 ∈ 𝐵 𝑥 = ( 𝐹 ‘ 𝑦 ) )
6 3 5 bitrdi ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴 ) → ( 𝑥 ∈ ( 𝐹 “ 𝐵 ) ↔ ∃ 𝑦 ∈ 𝐵 𝑥 = ( 𝐹 ‘ 𝑦 ) ) )
7 1 adantl ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴 ) ∧ 𝑥 = ( 𝐹 ‘ 𝑦 ) ) → ( 𝜑 ↔ 𝜓 ) )
8 2 6 7 ralxfr2d ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴 ) → ( ∀ 𝑥 ∈ ( 𝐹 “ 𝐵 ) 𝜑 ↔ ∀ 𝑦 ∈ 𝐵 𝜓 ) )