Metamath Proof Explorer


Theorem cnvepresex

Description: Sethood condition for the restricted converse epsilon relation. (Contributed by Peter Mazsa, 24-Sep-2018)

Ref Expression
Assertion cnvepresex ( 𝐴𝑉 → ( E ↾ 𝐴 ) ∈ V )

Proof

Step Hyp Ref Expression
1 cnvepres ( E ↾ 𝐴 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥𝐴𝑦𝑥 ) }
2 id ( 𝐴𝑉𝐴𝑉 )
3 abid2 { 𝑦𝑦𝑥 } = 𝑥
4 vex 𝑥 ∈ V
5 3 4 eqeltri { 𝑦𝑦𝑥 } ∈ V
6 5 a1i ( ( 𝐴𝑉𝑥𝐴 ) → { 𝑦𝑦𝑥 } ∈ V )
7 2 6 opabex3d ( 𝐴𝑉 → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥𝐴𝑦𝑥 ) } ∈ V )
8 1 7 eqeltrid ( 𝐴𝑉 → ( E ↾ 𝐴 ) ∈ V )