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

Metamath Proof Explorer

Theorem ralima

Description: Universal quantification under an image in terms of the base set. (Contributed by Stefan O'Rear, 21-Jan-2015) Reduce DV conditions. (Revised by Matthew House, 14-Aug-2025)

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

Proof

Step Hyp Ref Expression
1 ralima.x ⊢ ( 𝑥 = ( 𝐹 ‘ 𝑦 ) → ( 𝜑 ↔ 𝜓 ) )
2 fnfun ⊢ ( 𝐹 Fn 𝐴 → Fun 𝐹 )
3 2 funfnd ⊢ ( 𝐹 Fn 𝐴 → 𝐹 Fn dom 𝐹 )
4 fndm ⊢ ( 𝐹 Fn 𝐴 → dom 𝐹 = 𝐴 )
5 4 sseq2d ⊢ ( 𝐹 Fn 𝐴 → ( 𝐵 ⊆ dom 𝐹 ↔ 𝐵 ⊆ 𝐴 ) )
6 5 biimpar ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴 ) → 𝐵 ⊆ dom 𝐹 )
7 fvexd ⊢ ( ( ( 𝐹 Fn dom 𝐹 ∧ 𝐵 ⊆ dom 𝐹 ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝐹 ‘ 𝑦 ) ∈ V )
8 fvelimab ⊢ ( ( 𝐹 Fn dom 𝐹 ∧ 𝐵 ⊆ dom 𝐹 ) → ( 𝑥 ∈ ( 𝐹 “ 𝐵 ) ↔ ∃ 𝑦 ∈ 𝐵 ( 𝐹 ‘ 𝑦 ) = 𝑥 ) )
9 eqcom ⊢ ( ( 𝐹 ‘ 𝑦 ) = 𝑥 ↔ 𝑥 = ( 𝐹 ‘ 𝑦 ) )
10 9 rexbii ⊢ ( ∃ 𝑦 ∈ 𝐵 ( 𝐹 ‘ 𝑦 ) = 𝑥 ↔ ∃ 𝑦 ∈ 𝐵 𝑥 = ( 𝐹 ‘ 𝑦 ) )
11 8 10 bitrdi ⊢ ( ( 𝐹 Fn dom 𝐹 ∧ 𝐵 ⊆ dom 𝐹 ) → ( 𝑥 ∈ ( 𝐹 “ 𝐵 ) ↔ ∃ 𝑦 ∈ 𝐵 𝑥 = ( 𝐹 ‘ 𝑦 ) ) )
12 1 adantl ⊢ ( ( ( 𝐹 Fn dom 𝐹 ∧ 𝐵 ⊆ dom 𝐹 ) ∧ 𝑥 = ( 𝐹 ‘ 𝑦 ) ) → ( 𝜑 ↔ 𝜓 ) )
13 7 11 12 ralxfr2d ⊢ ( ( 𝐹 Fn dom 𝐹 ∧ 𝐵 ⊆ dom 𝐹 ) → ( ∀ 𝑥 ∈ ( 𝐹 “ 𝐵 ) 𝜑 ↔ ∀ 𝑦 ∈ 𝐵 𝜓 ) )
14 3 6 13 syl2an2r ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴 ) → ( ∀ 𝑥 ∈ ( 𝐹 “ 𝐵 ) 𝜑 ↔ ∀ 𝑦 ∈ 𝐵 𝜓 ) )