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 )