Metamath Proof Explorer


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