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 1811   ∈ wcel 2144  ∃wrex 3086

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-12 2212

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

This theorem is used by:  rsp2e  3280  2rmorex  3711  2reurex  3717  ssiun2  5005  reusv2lem3  5361  fvelimad  6952  tfrlem9  8394  findcard2  9181  isinf  9257  findcard3  9275  scott0b  9938  scott0OLD  9939  ac6c4  10560  supaddc  12285  supadd  12286  supmul1  12287  supmul  12290  fsuppmapnn0fiub  14135  mreiincl  17767  restmetu  24890  bposlem3  27614  nosupbnd1  28072  nosupbnd2  28074  noinfbnd1  28087  noinfbnd2  28089  opphllem5  29228  dfprlng2  29426  pjpjpre  32022  atom1d  32956  iinabrex  33206  actfunsnf1o  35276  bnj1398  35707  cvmlift2lem12  36148  finminlem  37181  neibastop2lem  37223  iooelexlt  38361  relowlpssretop  38363  ralssiun  38406  varprop  38718  disjlem18  39911  prtlem18  40010  pell14qrdich  43952  unielss  44296  eliuniin  46190  eliuniin2  46211  eliunid  46238  disjinfi  46283  iunmapsn  46306  infnsuprnmpt  46338  upbdrech  46397  limclner  46737  limsupre3uzlem  46821  climuzlem  46829  sge0iunmptlemre  47501  iundjiun  47546  meaiininclem  47572  isomenndlem  47616  ovnsubaddlem1  47656  vonioo  47768  vonicc  47771  smfaddlem1  47849  f1oresf1o2  48437