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

Proof

Step Hyp Ref Expression
1 rngop.1 ⊢ F = x ∈ A , y ∈ B ⟼ C
2 elrnmpo.1 ⊢ C ∈ V
3 1 rnmpo ⊢ ran ⁡ F = z | ∃ x ∈ A ∃ y ∈ B z = C
4 3 eleq2i ⊢ D ∈ ran ⁡ F ↔ D ∈ z | ∃ x ∈ A ∃ y ∈ B z = C
5 eleq1 ⊢ D = C → D ∈ V ↔ C ∈ V
6 2 5 mpbiri ⊢ D = C → D ∈ V
7 6 rexlimivw ⊢ ∃ y ∈ B D = C → D ∈ V
8 7 rexlimivw ⊢ ∃ x ∈ A ∃ y ∈ B D = C → D ∈ V
9 eqeq1 ⊢ z = D → z = C ↔ D = C
10 9 2rexbidv ⊢ z = D → ∃ x ∈ A ∃ y ∈ B z = C ↔ ∃ x ∈ A ∃ y ∈ B D = C
11 8 10 elab3 ⊢ D ∈ z | ∃ x ∈ A ∃ y ∈ B z = C ↔ ∃ x ∈ A ∃ y ∈ B D = C
12 4 11 bitri ⊢ D ∈ ran ⁡ F ↔ ∃ x ∈ A ∃ y ∈ B D = C