Metamath Proof Explorer

Theorem brdmqss

Description: The domain quotient binary relation. (Contributed by Peter Mazsa, 17-Apr-2019)

Ref Expression
Assertion brdmqss 
|- ( ( A e. V /\ R e. W ) -> ( R DomainQss A <-> ( dom R /. R ) = A ) )

Proof

Step Hyp Ref Expression
1 dmqseq 
 |-  ( x = R -> ( dom x /. x ) = ( dom R /. R ) )
2 id 
 |-  ( y = A -> y = A )
3 1 2 eqeqan12d 
 |-  ( ( x = R /\ y = A ) -> ( ( dom x /. x ) = y <-> ( dom R /. R ) = A ) )
4 df-dmqss 
 |-  DomainQss = { <. x , y >. | ( dom x /. x ) = y }
5 3 4 brabga 
 |-  ( ( R e. W /\ A e. V ) -> ( R DomainQss A <-> ( dom R /. R ) = A ) )
6 5 ancoms 
 |-  ( ( A e. V /\ R e. W ) -> ( R DomainQss A <-> ( dom R /. R ) = A ) )