Theorem rspe 3228

Description: Restricted specialization. (Contributed by NM, 12-Oct-1999.)

Assertion

Ref	Expression
rspe	⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) → ∃𝑥 ∈ 𝐴 𝜑)

Proof of Theorem rspe

Step	Hyp	Ref	Expression
1		19.8a 2189	. 2 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) → ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
2		df-rex 3063	. 2 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
3	1, 2	sylibr 234	1 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) → ∃𝑥 ∈ 𝐴 𝜑)

Syntax hints:   → wi 4   ∧ wa 395  ∃wex 1781   ∈ wcel 2114  ∃wrex 3062

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-12 2185

This theorem depends on definitions:  df-bi 207  df-ex 1782  df-rex 3063

This theorem is referenced by:  rsp2e  3256  2rmorex  3701  2reurex  3707  ssiun2  4991  reusv2lem3  5335  fvelimad  6899  tfrlem9  8315  findcard2  9090  isinf  9166  findcard3  9184  scott0  9799  ac6c4  10392  supaddc  12112  supadd  12113  supmul1  12114  supmul  12117  fsuppmapnn0fiub  13942  mreiincl  17547  restmetu  24544  bposlem3  27268  nosupbnd1  27697  nosupbnd2  27699  noinfbnd1  27712  noinfbnd2  27714  opphllem5  28838  pjpjpre  31510  atom1d  32444  iinabrex  32659  actfunsnf1o  34769  bnj1398  35197  cvmlift2lem12  35517  finminlem  36521  neibastop2lem  36563  iooelexlt  37689  relowlpssretop  37691  ralssiun  37734  disjlem18  39235  prtlem18  39334  pell14qrdich  43312  unielss  43661  eliuniin  45544  eliuniin2  45565  eliunid  45592  disjinfi  45637  iunmapsn  45661  infnsuprnmpt  45694  upbdrech  45753  limclner  46094  limsupre3uzlem  46178  climuzlem  46186  sge0iunmptlemre  46858  iundjiun  46903  meaiininclem  46929  isomenndlem  46973  ovnsubaddlem1  47013  vonioo  47125  vonicc  47128  smfaddlem1  47206  f1oresf1o2  47736