Description: Membership in a range. (Contributed by NM, 2-Apr-2004)
Ref | Expression | ||
---|---|---|---|
Hypothesis | elrn.1 | ⊢ 𝐴 ∈ V | |
Assertion | elrn | ⊢ ( 𝐴 ∈ ran 𝐵 ↔ ∃ 𝑥 𝑥 𝐵 𝐴 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elrn.1 | ⊢ 𝐴 ∈ V | |
2 | 1 | elrn2 | ⊢ ( 𝐴 ∈ ran 𝐵 ↔ ∃ 𝑥 〈 𝑥 , 𝐴 〉 ∈ 𝐵 ) |
3 | df-br | ⊢ ( 𝑥 𝐵 𝐴 ↔ 〈 𝑥 , 𝐴 〉 ∈ 𝐵 ) | |
4 | 3 | exbii | ⊢ ( ∃ 𝑥 𝑥 𝐵 𝐴 ↔ ∃ 𝑥 〈 𝑥 , 𝐴 〉 ∈ 𝐵 ) |
5 | 2 4 | bitr4i | ⊢ ( 𝐴 ∈ ran 𝐵 ↔ ∃ 𝑥 𝑥 𝐵 𝐴 ) |