Metamath Proof Explorer

Theorem ec1cnvres

Description: Converse restricted coset of B . (Contributed by Peter Mazsa, 22-Mar-2019) (Revised by Peter Mazsa, 21-Oct-2021)

Ref Expression
Assertion ec1cnvres 
|- ( B e. V -> [ B ] `' ( R |` A ) = { x e. A | x R B } )

Proof

Step Hyp Ref Expression
1 elec1cnvres 
 |-  ( B e. V -> ( x e. [ B ] `' ( R |` A ) <-> ( x e. A /\ x R B ) ) )
2 1 eqabdv 
 |-  ( B e. V -> [ B ] `' ( R |` A ) = { x | ( x e. A /\ x R B ) } )
3 df-rab 
 |-  { x e. A | x R B } = { x | ( x e. A /\ x R B ) }
4 2 3 eqtr4di 
 |-  ( B e. V -> [ B ] `' ( R |` A ) = { x e. A | x R B } )