Theorem rspe 3252

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

Assertion

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

Proof of Theorem rspe

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401  ∃wex 1812   ∈ wcel 2145  ∃wrex 3086

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-12 2213

This proof depends on definitions:  df-bi 210  df-ex 1813  df-rex 3087

This theorem is used by:  rsp2e  3280  2rmorex  3711  2reurex  3717  ssiun2  5005  reusv2lem3  5361  fvelimad  6940  tfrlem9  8371  findcard2  9158  isinf  9234  findcard3  9252  scott0b  9909  scott0OLD  9910  ac6c4  10531  supaddc  12254  supadd  12255  supmul1  12256  supmul  12259  fsuppmapnn0fiub  14103  mreiincl  17728  restmetu  24851  bposlem3  27577  nosupbnd1  28005  nosupbnd2  28007  noinfbnd1  28020  noinfbnd2  28022  opphllem5  29161  dfprlng2  29359  pjpjpre  31955  atom1d  32889  iinabrex  33097  actfunsnf1o  35168  bnj1398  35599  cvmlift2lem12  36000  finminlem  37028  neibastop2lem  37070  iooelexlt  38205  relowlpssretop  38207  ralssiun  38250  varprop  38562  disjlem18  39755  prtlem18  39854  pell14qrdich  43814  unielss  44163  eliuniin  46035  eliuniin2  46056  eliunid  46083  disjinfi  46128  iunmapsn  46151  infnsuprnmpt  46183  upbdrech  46242  limclner  46583  limsupre3uzlem  46667  climuzlem  46675  sge0iunmptlemre  47347  iundjiun  47392  meaiininclem  47418  isomenndlem  47462  ovnsubaddlem1  47502  vonioo  47614  vonicc  47617  smfaddlem1  47695  f1oresf1o2  48283