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