This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database ZF (ZERMELO-FRAENKEL) SET THEORY ZF Set Theory - add the Axiom of Union Relations and functions (cont.) 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 ⊢ 𝐴 ∈ V
ab2rexex2.2 ⊢ 𝐵 ∈ V
ab2rexex2.3 ⊢ { 𝑧 ∣ 𝜑 } ∈ V
Assertion
ab2rexex2 ⊢ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 } ∈ V
Proof
Step
Hyp
Ref
Expression
1
ab2rexex2.1 ⊢ 𝐴 ∈ V
2
ab2rexex2.2 ⊢ 𝐵 ∈ V
3
ab2rexex2.3 ⊢ { 𝑧 ∣ 𝜑 } ∈ V
4
2 3
abrexex2 ⊢ { 𝑧 ∣ ∃ 𝑦 ∈ 𝐵 𝜑 } ∈ V
5
1 4
abrexex2 ⊢ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 } ∈ V