Theorem ra4e 1244

Description: Restricted specialization.

Assertion

Ref	Expression
ra4e	⊢ ((x ∈ A ∧ φ) → ∃x ∈ A φ)

Proof of Theorem ra4e

Step	Hyp	Ref	Expression
1		19.8a 712	. 2 ⊢ ((x ∈ A ∧ φ) → ∃x(x ∈ A ∧ φ))
2		df-rex 1206	. 2 ⊢ (∃x ∈ A φ ↔ ∃x(x ∈ A ∧ φ))
3	1, 2	sylibr 175	1 ⊢ ((x ∈ A ∧ φ) → ∃x ∈ A φ)

Syntax hints:   → wi 2   ∧ wa 196  ∃wex 678   ∈ wcel 1092  ∃wrex 1202

This theorem is referenced by:  ssiun2 2019  onfr 2237  tfrlem8 2956  tfrlem9 2957  scott0 3542  infxpidmlem7 4939  infxpidmlem8 4940  atom1d 5750

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673

This theorem depends on definitions:  df-bi 128  df-ex 679  df-rex 1206

metamath.org