This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝐹 ↔ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝐷 = 𝐶 )