Theorem coss2cnvepres

Description: Special case of coss1cnvres . (Contributed by Peter Mazsa, 8-Jun-2020)

	Ref	Expression
Assertion	coss2cnvepres	|- ,~ `' ( `' _E |` A ) = { <. u , v >. | ( ( u e. A /\ v e. A ) /\ E. x ( x e. u /\ x e. v ) ) }

Proof

Step	Hyp	Ref	Expression
1		coss1cnvres	|- ,~ `' ( `' _E |` A ) = { <. u , v >. | ( ( u e. A /\ v e. A ) /\ E. x ( u `' _E x /\ v `' _E x ) ) }
2		brcnvep	|- ( u e. _V -> ( u `' _E x <-> x e. u ) )
3	2	elv	|- ( u `' _E x <-> x e. u )
4		brcnvep	|- ( v e. _V -> ( v `' _E x <-> x e. v ) )
5	4	elv	|- ( v `' _E x <-> x e. v )
6	3 5	anbi12i	|- ( ( u `' _E x /\ v `' _E x ) <-> ( x e. u /\ x e. v ) )
7	6	exbii	|- ( E. x ( u `' _E x /\ v `' _E x ) <-> E. x ( x e. u /\ x e. v ) )
8	7	anbi2i	|- ( ( ( u e. A /\ v e. A ) /\ E. x ( u `' _E x /\ v `' _E x ) ) <-> ( ( u e. A /\ v e. A ) /\ E. x ( x e. u /\ x e. v ) ) )
9	8	opabbii	|- { <. u , v >. | ( ( u e. A /\ v e. A ) /\ E. x ( u `' _E x /\ v `' _E x ) ) } = { <. u , v >. | ( ( u e. A /\ v e. A ) /\ E. x ( x e. u /\ x e. v ) ) }
10	1 9	eqtri	|- ,~ `' ( `' _E |` A ) = { <. u , v >. | ( ( u e. A /\ v e. A ) /\ E. x ( x e. u /\ x e. v ) ) }