Metamath Proof Explorer


Theorem ab2rexex

Description: Existence of a class abstraction of existentially restricted sets. Variables x and y are normally free-variable parameters in the class expression substituted for C , which can be thought of as C ( x , y ) . See comments for abrexex . (Contributed by NM, 20-Sep-2011)

Ref Expression
Hypotheses ab2rexex.1 𝐴 ∈ V
ab2rexex.2 𝐵 ∈ V
Assertion ab2rexex { 𝑧 ∣ ∃ 𝑥𝐴𝑦𝐵 𝑧 = 𝐶 } ∈ V

Proof

Step Hyp Ref Expression
1 ab2rexex.1 𝐴 ∈ V
2 ab2rexex.2 𝐵 ∈ V
3 2 abrexex { 𝑧 ∣ ∃ 𝑦𝐵 𝑧 = 𝐶 } ∈ V
4 1 3 abrexex2 { 𝑧 ∣ ∃ 𝑥𝐴𝑦𝐵 𝑧 = 𝐶 } ∈ V