Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Peter Mazsa
Preparatory theorems
0qs
Next ⟩
Range Cartesian product
Metamath Proof Explorer
Ascii
Unicode
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
=
∅