Theorem elrnmptg

Description: Membership in the range of a function. (Contributed by NM, 27-Aug-2007) (Revised by Mario Carneiro, 31-Aug-2015)

	Ref	Expression
Hypothesis	rnmpt.1	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
Assertion	elrnmptg	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → ( 𝐶 ∈ ran 𝐹 ↔ ∃ 𝑥 ∈ 𝐴 𝐶 = 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		rnmpt.1	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
2	1	rnmpt	⊢ ran 𝐹 = { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 }
3	2	eleq2i	⊢ ( 𝐶 ∈ ran 𝐹 ↔ 𝐶 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } )
4		r19.29	⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 ∧ ∃ 𝑥 ∈ 𝐴 𝐶 = 𝐵 ) → ∃ 𝑥 ∈ 𝐴 ( 𝐵 ∈ 𝑉 ∧ 𝐶 = 𝐵 ) )
5		eleq1	⊢ ( 𝐶 = 𝐵 → ( 𝐶 ∈ 𝑉 ↔ 𝐵 ∈ 𝑉 ) )
6	5	biimparc	⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝐶 = 𝐵 ) → 𝐶 ∈ 𝑉 )
7	6	elexd	⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝐶 = 𝐵 ) → 𝐶 ∈ V )
8	7	rexlimivw	⊢ ( ∃ 𝑥 ∈ 𝐴 ( 𝐵 ∈ 𝑉 ∧ 𝐶 = 𝐵 ) → 𝐶 ∈ V )
9	4 8	syl	⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 ∧ ∃ 𝑥 ∈ 𝐴 𝐶 = 𝐵 ) → 𝐶 ∈ V )
10	9	ex	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → ( ∃ 𝑥 ∈ 𝐴 𝐶 = 𝐵 → 𝐶 ∈ V ) )
11		eqeq1	⊢ ( 𝑦 = 𝐶 → ( 𝑦 = 𝐵 ↔ 𝐶 = 𝐵 ) )
12	11	rexbidv	⊢ ( 𝑦 = 𝐶 → ( ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 ↔ ∃ 𝑥 ∈ 𝐴 𝐶 = 𝐵 ) )
13	12	elab3g	⊢ ( ( ∃ 𝑥 ∈ 𝐴 𝐶 = 𝐵 → 𝐶 ∈ V ) → ( 𝐶 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } ↔ ∃ 𝑥 ∈ 𝐴 𝐶 = 𝐵 ) )
14	10 13	syl	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → ( 𝐶 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } ↔ ∃ 𝑥 ∈ 𝐴 𝐶 = 𝐵 ) )
15	3 14	bitrid	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → ( 𝐶 ∈ ran 𝐹 ↔ ∃ 𝑥 ∈ 𝐴 𝐶 = 𝐵 ) )