This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) ) }