Metamath Proof Explorer

Theorem ab2rexex2

Description: Existence of an existentially restricted class abstraction. ph normally has free-variable parameters x , y , and z . Compare abrexex2 . (Contributed by NM, 20-Sep-2011)

Ref Expression
Hypotheses ab2rexex2.1 ⊢ A ∈ V
ab2rexex2.2 ⊢ B ∈ V
ab2rexex2.3 ⊢ z | φ ∈ V
Assertion ab2rexex2 ⊢ z | ∃ x ∈ A ∃ y ∈ B φ ∈ V

Proof

Step Hyp Ref Expression
1 ab2rexex2.1 ⊢ A ∈ V
2 ab2rexex2.2 ⊢ B ∈ V
3 ab2rexex2.3 ⊢ z | φ ∈ V
4 2 3 abrexex2 ⊢ z | ∃ y ∈ B φ ∈ V
5 1 4 abrexex2 ⊢ z | ∃ x ∈ A ∃ y ∈ B φ ∈ V