Theorem elrnmpo

Description: Membership in the range of an operation class abstraction. (Contributed by NM, 1-Aug-2004) (Revised by Mario Carneiro, 31-Aug-2015)

	Ref	Expression
Hypotheses	rngop.1	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 )
	elrnmpo.1	⊢ 𝐶 ∈ V
Assertion	elrnmpo	⊢ ( 𝐷 ∈ ran 𝐹 ↔ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝐷 = 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		rngop.1	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 )
2		elrnmpo.1	⊢ 𝐶 ∈ V
3	1	rnmpo	⊢ ran 𝐹 = { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑧 = 𝐶 }
4	3	eleq2i	⊢ ( 𝐷 ∈ ran 𝐹 ↔ 𝐷 ∈ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑧 = 𝐶 } )
5		eleq1	⊢ ( 𝐷 = 𝐶 → ( 𝐷 ∈ V ↔ 𝐶 ∈ V ) )
6	2 5	mpbiri	⊢ ( 𝐷 = 𝐶 → 𝐷 ∈ V )
7	6	rexlimivw	⊢ ( ∃ 𝑦 ∈ 𝐵 𝐷 = 𝐶 → 𝐷 ∈ V )
8	7	rexlimivw	⊢ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝐷 = 𝐶 → 𝐷 ∈ V )
9		eqeq1	⊢ ( 𝑧 = 𝐷 → ( 𝑧 = 𝐶 ↔ 𝐷 = 𝐶 ) )
10	9	2rexbidv	⊢ ( 𝑧 = 𝐷 → ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑧 = 𝐶 ↔ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝐷 = 𝐶 ) )
11	8 10	elab3	⊢ ( 𝐷 ∈ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑧 = 𝐶 } ↔ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝐷 = 𝐶 )
12	4 11	bitri	⊢ ( 𝐷 ∈ ran 𝐹 ↔ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝐷 = 𝐶 )