Theorem rspe 3230

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

Assertion

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

Proof of Theorem rspe

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

Syntax hints:   → wi 4   ∧ wa 396  ∃wex 1786   ∈ wcel 2119  ∃wrex 3064

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-12 2189

This theorem depends on definitions:  df-bi 208  df-ex 1787  df-rex 3065

This theorem is referenced by:  rsp2e  3258  2rmorex  3702  2reurex  3708  ssiun2  4984  reusv2lem3  5336  fvelimad  6901  tfrlem9  8321  findcard2  9096  isinf  9172  findcard3  9190  scott0  9808  ac6c4  10401  supaddc  12121  supadd  12122  supmul1  12123  supmul  12126  fsuppmapnn0fiub  13951  mreiincl  17556  restmetu  24560  bposlem3  27274  nosupbnd1  27703  nosupbnd2  27705  noinfbnd1  27718  noinfbnd2  27720  opphllem5  28844  pjpjpre  31515  atom1d  32449  iinabrex  32665  actfunsnf1o  34795  bnj1398  35223  cvmlift2lem12  35543  finminlem  36547  neibastop2lem  36589  iooelexlt  37725  relowlpssretop  37727  ralssiun  37770  disjlem18  39271  prtlem18  39370  pell14qrdich  43315  unielss  43664  eliuniin  45547  eliuniin2  45568  eliunid  45595  disjinfi  45640  iunmapsn  45663  infnsuprnmpt  45695  upbdrech  45754  limclner  46095  limsupre3uzlem  46179  climuzlem  46187  sge0iunmptlemre  46859  iundjiun  46904  meaiininclem  46930  isomenndlem  46974  ovnsubaddlem1  47014  vonioo  47126  vonicc  47129  smfaddlem1  47207  f1oresf1o2  47755