Theorem rspe 3255

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

Assertion

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

Proof of Theorem rspe

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

Syntax hints:   → wi 4   ∧ wa 400  ∃wex 1802   ∈ wcel 2145  ∃wrex 3089

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-12 2215

This theorem depends on definitions:  df-bi 210  df-ex 1803  df-rex 3090

This theorem is referenced by:  rsp2e  3283  2rmorex  3720  2reurex  3726  ssiun2  5008  reusv2lem3  5362  fvelimad  6938  tfrlem9  8360  findcard2  9137  isinf  9213  findcard3  9231  scott0  9848  ac6c4  10453  supaddc  12173  supadd  12174  supmul1  12175  supmul  12178  fsuppmapnn0fiub  14018  mreiincl  17638  restmetu  24688  bposlem3  27408  nosupbnd1  27836  nosupbnd2  27838  noinfbnd1  27851  noinfbnd2  27853  opphllem5  28982  pjpjpre  31680  atom1d  32614  iinabrex  32824  actfunsnf1o  34908  bnj1398  35339  cvmlift2lem12  35677  finminlem  36691  neibastop2lem  36733  iooelexlt  37868  relowlpssretop  37870  ralssiun  37913  disjlem18  39414  prtlem18  39513  pell14qrdich  43458  unielss  43807  eliuniin  45675  eliuniin2  45696  eliunid  45723  disjinfi  45768  iunmapsn  45791  infnsuprnmpt  45823  upbdrech  45882  limclner  46223  limsupre3uzlem  46307  climuzlem  46315  sge0iunmptlemre  46987  iundjiun  47032  meaiininclem  47058  isomenndlem  47102  ovnsubaddlem1  47142  vonioo  47254  vonicc  47257  smfaddlem1  47335  f1oresf1o2  47883