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.) abrexex2
Description: Existence of an existentially restricted class abstraction. ph
normally has free-variable parameters x and y . See also
abrexex . (Contributed by NM , 12-Sep-2004)
Ref
Expression
Hypotheses
abrexex2.1 ⊢ 𝐴 ∈ V
abrexex2.2 ⊢ { 𝑦 ∣ 𝜑 } ∈ V
Assertion
abrexex2 ⊢ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝜑 } ∈ V
Proof
Step
Hyp
Ref
Expression
1
abrexex2.1 ⊢ 𝐴 ∈ V
2
abrexex2.2 ⊢ { 𝑦 ∣ 𝜑 } ∈ V
3
2
rgenw ⊢ ∀ 𝑥 ∈ 𝐴 { 𝑦 ∣ 𝜑 } ∈ V
4
abrexex2g ⊢ ( ( 𝐴 ∈ V ∧ ∀ 𝑥 ∈ 𝐴 { 𝑦 ∣ 𝜑 } ∈ V ) → { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝜑 } ∈ V )
5
1 3 4
mp2an ⊢ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝜑 } ∈ V