Metamath Proof Explorer


Theorem dfqs3

Description: Alternate definition of quotient set. (Contributed by Steven Nguyen, 7-Jun-2023)

Ref Expression
Assertion dfqs3
|- ( A /. R ) = U_ x e. A { [ x ] R }

Proof

Step Hyp Ref Expression
1 df-qs
 |-  ( A /. R ) = { y | E. x e. A y = [ x ] R }
2 iunsn
 |-  U_ x e. A { [ x ] R } = { y | E. x e. A y = [ x ] R }
3 1 2 eqtr4i
 |-  ( A /. R ) = U_ x e. A { [ x ] R }