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 |` A ) = { <. x , y >. | ( x e. A /\ y e. x ) }

Proof

Step	Hyp	Ref	Expression
1		dfres2	|- ( `' _E |` A ) = { <. x , y >. | ( x e. A /\ x `' _E y ) }
2		brcnvep	|- ( x e. _V -> ( x `' _E y <-> y e. x ) )
3	2	elv	|- ( x `' _E y <-> y e. x )
4	3	anbi2i	|- ( ( x e. A /\ x `' _E y ) <-> ( x e. A /\ y e. x ) )
5	4	opabbii	|- { <. x , y >. | ( x e. A /\ x `' _E y ) } = { <. x , y >. | ( x e. A /\ y e. x ) }
6	1 5	eqtri	|- ( `' _E |` A ) = { <. x , y >. | ( x e. A /\ y e. x ) }