Metamath Proof Explorer

Theorem dfcoels

Description: Alternate definition of the class of coelements on the class A . (Contributed by Peter Mazsa, 20-Apr-2019)

Ref Expression
Assertion dfcoels 
|- ~ A = { <. x , y >. | E. u e. A ( x e. u /\ y e. u ) }

Proof

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