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