Metamath Proof Explorer

Theorem dmqsex

Description: Sethood of the domain quotient under sethood of R . (Contributed by Peter Mazsa, 2-Nov-2018)

Ref Expression
Assertion dmqsex 
|- ( R e. V -> ( dom R /. R ) e. _V )

Proof

Step Hyp Ref Expression
1 dmexg 
 |-  ( R e. V -> dom R e. _V )
2 qsexg 
 |-  ( dom R e. _V -> ( dom R /. R ) e. _V )
3 1 2 syl 
 |-  ( R e. V -> ( dom R /. R ) e. _V )