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 𝐹 𝜑 ↔ ∃ 𝑦 ∈ 𝐴 𝜓 ) )