Description: Membership in a range. (Contributed by NM, 10-Jul-1994)
Ref | Expression | ||
---|---|---|---|
Hypothesis | elrn.1 | ⊢ 𝐴 ∈ V | |
Assertion | elrn2 | ⊢ ( 𝐴 ∈ ran 𝐵 ↔ ∃ 𝑥 〈 𝑥 , 𝐴 〉 ∈ 𝐵 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elrn.1 | ⊢ 𝐴 ∈ V | |
2 | opeq2 | ⊢ ( 𝑦 = 𝐴 → 〈 𝑥 , 𝑦 〉 = 〈 𝑥 , 𝐴 〉 ) | |
3 | 2 | eleq1d | ⊢ ( 𝑦 = 𝐴 → ( 〈 𝑥 , 𝑦 〉 ∈ 𝐵 ↔ 〈 𝑥 , 𝐴 〉 ∈ 𝐵 ) ) |
4 | 3 | exbidv | ⊢ ( 𝑦 = 𝐴 → ( ∃ 𝑥 〈 𝑥 , 𝑦 〉 ∈ 𝐵 ↔ ∃ 𝑥 〈 𝑥 , 𝐴 〉 ∈ 𝐵 ) ) |
5 | dfrn3 | ⊢ ran 𝐵 = { 𝑦 ∣ ∃ 𝑥 〈 𝑥 , 𝑦 〉 ∈ 𝐵 } | |
6 | 1 4 5 | elab2 | ⊢ ( 𝐴 ∈ ran 𝐵 ↔ ∃ 𝑥 〈 𝑥 , 𝐴 〉 ∈ 𝐵 ) |