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	$⊢ x = F (y) \to (φ \leftrightarrow ψ)$
	Assertion	rexrn	$⊢ F Fn A \to (\exists x \in ran F φ \leftrightarrow \exists y \in A ψ)$

Proof

Step	Hyp	Ref	Expression
1		rexrn.1	$⊢ x = F (y) \to (φ \leftrightarrow ψ)$
2		fvexd	$⊢ (F Fn A \land y \in A) \to F (y) \in V$
3		fvelrnb	$⊢ F Fn A \to (x \in ran F \leftrightarrow \exists y \in A F (y) = x)$
4		eqcom	$⊢ F (y) = x \leftrightarrow x = F (y)$
5	4	rexbii	$⊢ \exists y \in A F (y) = x \leftrightarrow \exists y \in A x = F (y)$
6	3 5	bitrdi	$⊢ F Fn A \to (x \in ran F \leftrightarrow \exists y \in A x = F (y))$
7	1	adantl	$⊢ (F Fn A \land x = F (y)) \to (φ \leftrightarrow ψ)$
8	2 6 7	rexxfr2d	$⊢ F Fn A \to (\exists x \in ran F φ \leftrightarrow \exists y \in A ψ)$