Metamath Proof Explorer


Theorem cnvepres

Description: Restricted converse epsilon relation as a class of ordered pairs. (Contributed by Peter Mazsa, 10-Feb-2018)

Ref Expression
Assertion cnvepres ( E ↾ 𝐴 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥𝐴𝑦𝑥 ) }

Proof

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 ↾ 𝐴 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥𝐴𝑦𝑥 ) }