Description: If A and R are sets, the domain quotient binary relation and the domain quotient predicate are the same. (Contributed by Peter Mazsa, 14-Aug-2021)
Ref | Expression | ||
---|---|---|---|
Assertion | brdmqssqs | |- ( ( A e. V /\ R e. W ) -> ( R DomainQss A <-> R DomainQs A ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | brdmqss | |- ( ( A e. V /\ R e. W ) -> ( R DomainQss A <-> ( dom R /. R ) = A ) ) |
|
2 | df-dmqs | |- ( R DomainQs A <-> ( dom R /. R ) = A ) |
|
3 | 1 2 | bitr4di | |- ( ( A e. V /\ R e. W ) -> ( R DomainQss A <-> R DomainQs A ) ) |