Description: Restricted converse epsilon relation as a class of ordered pairs. (Contributed by Peter Mazsa, 10-Feb-2018)
Ref | Expression | ||
---|---|---|---|
Assertion | cnvepres | ⊢ ( ◡ E ↾ 𝐴 ) = { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝑥 ) } |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dfres2 | ⊢ ( ◡ E ↾ 𝐴 ) = { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑥 ◡ E 𝑦 ) } | |
2 | brcnvep | ⊢ ( 𝑥 ∈ V → ( 𝑥 ◡ E 𝑦 ↔ 𝑦 ∈ 𝑥 ) ) | |
3 | 2 | elv | ⊢ ( 𝑥 ◡ E 𝑦 ↔ 𝑦 ∈ 𝑥 ) |
4 | 3 | anbi2i | ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ◡ E 𝑦 ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝑥 ) ) |
5 | 4 | opabbii | ⊢ { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑥 ◡ E 𝑦 ) } = { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝑥 ) } |
6 | 1 5 | eqtri | ⊢ ( ◡ E ↾ 𝐴 ) = { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝑥 ) } |