Theorem rspe 3246

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

Assertion

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

Proof of Theorem rspe

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

Syntax hints:   → wi 4   ∧ wa 398  ∃wex 1793   ∈ wcel 2136  ∃wrex 3080

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1809  ax-4 1823  ax-5 1924  ax-6 1981  ax-7 2022  ax-12 2206

This theorem depends on definitions:  df-bi 209  df-ex 1794  df-rex 3081

This theorem is referenced by:  rsp2e  3274  2rmorex  3711  2reurex  3717  ssiun2  4999  reusv2lem3  5351  fvelimad  6923  tfrlem9  8344  findcard2  9122  isinf  9198  findcard3  9216  scott0  9834  ac6c4  10428  supaddc  12149  supadd  12150  supmul1  12151  supmul  12154  fsuppmapnn0fiub  13994  mreiincl  17600  restmetu  24603  bposlem3  27320  nosupbnd1  27748  nosupbnd2  27750  noinfbnd1  27763  noinfbnd2  27765  opphllem5  28890  pjpjpre  31561  atom1d  32495  iinabrex  32711  actfunsnf1o  34855  bnj1398  35286  cvmlift2lem12  35612  finminlem  36626  neibastop2lem  36668  iooelexlt  37804  relowlpssretop  37806  ralssiun  37849  disjlem18  39350  prtlem18  39449  pell14qrdich  43394  unielss  43743  eliuniin  45625  eliuniin2  45646  eliunid  45673  disjinfi  45718  iunmapsn  45741  infnsuprnmpt  45773  upbdrech  45832  limclner  46173  limsupre3uzlem  46257  climuzlem  46265  sge0iunmptlemre  46937  iundjiun  46982  meaiininclem  47008  isomenndlem  47052  ovnsubaddlem1  47092  vonioo  47204  vonicc  47207  smfaddlem1  47285  f1oresf1o2  47833