Metamath Proof Explorer


Theorem abrexexg

Description: Existence of a class abstraction of existentially restricted sets. The class B can be thought of as an expression in x (which is typically a free variable in the class expression substituted for B ) and the class abstraction appearing in the statement as the class of values B as x varies through A . If the "domain" A is a set, then the abstraction is also a set. Therefore, this statement is a kind of Replacement. This can be seen by tracing back through the path mptexg , funex , fnex , resfunexg , and funimaexg . See also abrexex2g . There are partial converses under additional conditions, see for instance abnexg . (Contributed by NM, 3-Nov-2003) (Proof shortened by Mario Carneiro, 31-Aug-2015)

Ref Expression
Assertion abrexexg
|- ( A e. V -> { y | E. x e. A y = B } e. _V )

Proof

Step Hyp Ref Expression
1 eqid
 |-  ( x e. A |-> B ) = ( x e. A |-> B )
2 1 rnmpt
 |-  ran ( x e. A |-> B ) = { y | E. x e. A y = B }
3 mptexg
 |-  ( A e. V -> ( x e. A |-> B ) e. _V )
4 rnexg
 |-  ( ( x e. A |-> B ) e. _V -> ran ( x e. A |-> B ) e. _V )
5 3 4 syl
 |-  ( A e. V -> ran ( x e. A |-> B ) e. _V )
6 2 5 eqeltrrid
 |-  ( A e. V -> { y | E. x e. A y = B } e. _V )