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 ∈ V → dom ⁡ R / R ∈ V

Proof

Step Hyp Ref Expression
1 dmexg ⊢ R ∈ V → dom ⁡ R ∈ V
2 qsexg ⊢ dom ⁡ R ∈ V → dom ⁡ R / R ∈ V
3 1 2 syl ⊢ R ∈ V → dom ⁡ R / R ∈ V