Metamath Proof Explorer


Theorem qsexg

Description: A quotient set exists. (Contributed by FL, 19-May-2007) (Revised by Mario Carneiro, 9-Jul-2014)

Ref Expression
Assertion qsexg
|- ( A e. V -> ( A /. R ) e. _V )

Proof

Step Hyp Ref Expression
1 df-qs
 |-  ( A /. R ) = { y | E. x e. A y = [ x ] R }
2 abrexexg
 |-  ( A e. V -> { y | E. x e. A y = [ x ] R } e. _V )
3 1 2 eqeltrid
 |-  ( A e. V -> ( A /. R ) e. _V )