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 | E. x e. (/) y = [ x ] R }
2 rex0 
 |-  -. E. x e. (/) y = [ x ] R
3 2 abf 
 |-  { y | E. x e. (/) y = [ x ] R } = (/)
4 1 3 eqtri 
 |-  ( (/) /. R ) = (/)