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 e. A |-> [ x ] R )

Proof

Step Hyp Ref Expression
1 df-qs
 |-  ( A /. R ) = { y | E. x e. A y = [ x ] R }
2 eqid
 |-  ( x e. A |-> [ x ] R ) = ( x e. A |-> [ x ] R )
3 2 rnmpt
 |-  ran ( x e. A |-> [ x ] R ) = { y | E. x e. A y = [ x ] R }
4 1 3 eqtr4i
 |-  ( A /. R ) = ran ( x e. A |-> [ x ] R )