Metamath Proof Explorer


Theorem rexrn

Description: Restricted existential quantification over the range of a function. (Contributed by Mario Carneiro, 24-Dec-2013) (Revised by Mario Carneiro, 20-Aug-2014)

Ref Expression
Hypothesis rexrn.1 ( 𝑥 = ( 𝐹𝑦 ) → ( 𝜑𝜓 ) )
Assertion rexrn ( 𝐹 Fn 𝐴 → ( ∃ 𝑥 ∈ ran 𝐹 𝜑 ↔ ∃ 𝑦𝐴 𝜓 ) )

Proof

Step Hyp Ref Expression
1 rexrn.1 ( 𝑥 = ( 𝐹𝑦 ) → ( 𝜑𝜓 ) )
2 fvexd ( ( 𝐹 Fn 𝐴𝑦𝐴 ) → ( 𝐹𝑦 ) ∈ V )
3 fvelrnb ( 𝐹 Fn 𝐴 → ( 𝑥 ∈ ran 𝐹 ↔ ∃ 𝑦𝐴 ( 𝐹𝑦 ) = 𝑥 ) )
4 eqcom ( ( 𝐹𝑦 ) = 𝑥𝑥 = ( 𝐹𝑦 ) )
5 4 rexbii ( ∃ 𝑦𝐴 ( 𝐹𝑦 ) = 𝑥 ↔ ∃ 𝑦𝐴 𝑥 = ( 𝐹𝑦 ) )
6 3 5 bitrdi ( 𝐹 Fn 𝐴 → ( 𝑥 ∈ ran 𝐹 ↔ ∃ 𝑦𝐴 𝑥 = ( 𝐹𝑦 ) ) )
7 1 adantl ( ( 𝐹 Fn 𝐴𝑥 = ( 𝐹𝑦 ) ) → ( 𝜑𝜓 ) )
8 2 6 7 rexxfr2d ( 𝐹 Fn 𝐴 → ( ∃ 𝑥 ∈ ran 𝐹 𝜑 ↔ ∃ 𝑦𝐴 𝜓 ) )