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)