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 axrep6g , axrep6 , ax-rep . 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) Avoid ax-10 , ax-11 , ax-12 , ax-pr , ax-un and shorten proof. (Revised by SN, 11-Dec-2024)

Ref Expression
Assertion abrexexg ( 𝐴𝑉 → { 𝑦 ∣ ∃ 𝑥𝐴 𝑦 = 𝐵 } ∈ V )

Proof

Step Hyp Ref Expression
1 moeq ∃* 𝑦 𝑦 = 𝐵
2 1 ax-gen 𝑥 ∃* 𝑦 𝑦 = 𝐵
3 axrep6g ( ( 𝐴𝑉 ∧ ∀ 𝑥 ∃* 𝑦 𝑦 = 𝐵 ) → { 𝑦 ∣ ∃ 𝑥𝐴 𝑦 = 𝐵 } ∈ V )
4 2 3 mpan2 ( 𝐴𝑉 → { 𝑦 ∣ ∃ 𝑥𝐴 𝑦 = 𝐵 } ∈ V )