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)

Ref Expression
Hypothesis rexima.x ( 𝑥 = ( 𝐹𝑦 ) → ( 𝜑𝜓 ) )
Assertion ralima ( ( 𝐹 Fn 𝐴𝐵𝐴 ) → ( ∀ 𝑥 ∈ ( 𝐹𝐵 ) 𝜑 ↔ ∀ 𝑦𝐵 𝜓 ) )

Proof

Step Hyp Ref Expression
1 rexima.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 𝐴𝐵𝐴 ) → ( ∀ 𝑥 ∈ ( 𝐹𝐵 ) 𝜑 ↔ ∀ 𝑦𝐵 𝜓 ) )