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 )