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 ⊢ A ∈ V
ab2rexex.2 ⊢ B ∈ V
Assertion ab2rexex ⊢ z | ∃ x ∈ A ∃ y ∈ B z = C ∈ V

Proof

Step Hyp Ref Expression
1 ab2rexex.1 ⊢ A ∈ V
2 ab2rexex.2 ⊢ B ∈ V
3 2 abrexex ⊢ z | ∃ y ∈ B z = C ∈ V
4 1 3 abrexex2 ⊢ z | ∃ x ∈ A ∃ y ∈ B z = C ∈ V