Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Steven Nguyen
Utility theorems
dfqs2
Next ⟩
dfqs3
Metamath Proof Explorer
Ascii
Unicode
Theorem
dfqs2
Description:
Alternate definition of quotient set.
(Contributed by
Steven Nguyen
, 7-Jun-2023)
Ref
Expression
Assertion
dfqs2
⊢
A
/
R
=
ran
⁡
x
∈
A
⟼
x
R
Proof
Step
Hyp
Ref
Expression
1
df-qs
⊢
A
/
R
=
y
|
∃
x
∈
A
y
=
x
R
2
eqid
⊢
x
∈
A
⟼
x
R
=
x
∈
A
⟼
x
R
3
2
rnmpt
⊢
ran
⁡
x
∈
A
⟼
x
R
=
y
|
∃
x
∈
A
y
=
x
R
4
1
3
eqtr4i
⊢
A
/
R
=
ran
⁡
x
∈
A
⟼
x
R