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 𝐴𝐵𝐴 ) → ( ∀ 𝑥 ∈ ( 𝐹𝐵 ) 𝜑 ↔ ∀ 𝑦𝐵 𝜓 ) )