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 ⊢ F = x ∈ A , y ∈ B ⟼ C
Assertion elrnmpog ⊢ D ∈ V → D ∈ ran ⁡ F ↔ ∃ x ∈ A ∃ y ∈ B D = C

Proof

Step Hyp Ref Expression
1 rngop.1 ⊢ F = x ∈ A , y ∈ B ⟼ C
2 eqeq1 ⊢ z = D → z = C ↔ D = C
3 2 2rexbidv ⊢ z = D → ∃ x ∈ A ∃ y ∈ B z = C ↔ ∃ x ∈ A ∃ y ∈ B D = C
4 1 rnmpo ⊢ ran ⁡ F = z | ∃ x ∈ A ∃ y ∈ B z = C
5 3 4 elab2g ⊢ D ∈ V → D ∈ ran ⁡ F ↔ ∃ x ∈ A ∃ y ∈ B D = C