Metamath Proof Explorer


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