Metamath Proof Explorer


Theorem elrnmpog

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

Ref Expression
Hypothesis rngop.1 𝐹 = ( 𝑥𝐴 , 𝑦𝐵𝐶 )
Assertion elrnmpog ( 𝐷𝑉 → ( 𝐷 ∈ ran 𝐹 ↔ ∃ 𝑥𝐴𝑦𝐵 𝐷 = 𝐶 ) )

Proof

Step Hyp Ref Expression
1 rngop.1 𝐹 = ( 𝑥𝐴 , 𝑦𝐵𝐶 )
2 eqeq1 ( 𝑧 = 𝐷 → ( 𝑧 = 𝐶𝐷 = 𝐶 ) )
3 2 2rexbidv ( 𝑧 = 𝐷 → ( ∃ 𝑥𝐴𝑦𝐵 𝑧 = 𝐶 ↔ ∃ 𝑥𝐴𝑦𝐵 𝐷 = 𝐶 ) )
4 1 rnmpo ran 𝐹 = { 𝑧 ∣ ∃ 𝑥𝐴𝑦𝐵 𝑧 = 𝐶 }
5 3 4 elab2g ( 𝐷𝑉 → ( 𝐷 ∈ ran 𝐹 ↔ ∃ 𝑥𝐴𝑦𝐵 𝐷 = 𝐶 ) )