Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Peter Mazsa
Preparatory theorems
dfdm6
Next ⟩
dfrn6
Metamath Proof Explorer
Ascii
Unicode
Theorem
dfdm6
Description:
Alternate definition of domain.
(Contributed by
Peter Mazsa
, 2-Mar-2018)
Ref
Expression
Assertion
dfdm6
⊢
dom
⁡
R
=
x
|
x
R
≠
∅
Proof
Step
Hyp
Ref
Expression
1
ecdmn0
⊢
x
∈
dom
⁡
R
↔
x
R
≠
∅
2
1
abbi2i
⊢
dom
⁡
R
=
x
|
x
R
≠
∅