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 𝐹 ↔ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝐷 = 𝐶 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rngop.1 | ⊢ 𝐹 = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) | |
2 | eqeq1 | ⊢ ( 𝑧 = 𝐷 → ( 𝑧 = 𝐶 ↔ 𝐷 = 𝐶 ) ) | |
3 | 2 | 2rexbidv | ⊢ ( 𝑧 = 𝐷 → ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑧 = 𝐶 ↔ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝐷 = 𝐶 ) ) |
4 | 1 | rnmpo | ⊢ ran 𝐹 = { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑧 = 𝐶 } |
5 | 3 4 | elab2g | ⊢ ( 𝐷 ∈ 𝑉 → ( 𝐷 ∈ ran 𝐹 ↔ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝐷 = 𝐶 ) ) |