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 }