Metamath Proof Explorer


Theorem 0qs

Description: Quotient set with the empty set. (Contributed by Peter Mazsa, 14-Sep-2019)

Ref Expression
Assertion 0qs / R =

Proof

Step Hyp Ref Expression
1 df-qs / R = y | x y = x R
2 rex0 ¬ x y = x R
3 2 abf y | x y = x R =
4 1 3 eqtri / R =