Theorem rexima

Description: Existential quantification under an image in terms of the base set. (Contributed by Stefan O'Rear, 21-Jan-2015)

	Ref	Expression
Hypothesis	rexima.x	⊢ ( 𝑥 = ( 𝐹 ‘ 𝑦 ) → ( 𝜑 ↔ 𝜓 ) )
Assertion	rexima	⊢ ( ( 𝐹 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	rexxfr2d	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴 ) → ( ∃ 𝑥 ∈ ( 𝐹 “ 𝐵 ) 𝜑 ↔ ∃ 𝑦 ∈ 𝐵 𝜓 ) )