Theorem rspe 3256

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

Assertion

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

Proof of Theorem rspe

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

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

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 1945  ax-6 2002  ax-7 2043  ax-12 2216

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

This theorem is used by:  rsp2e  3284  2rmorex  3715  2reurex  3721  ssiun2  5009  reusv2lem3  5366  fvelimad  6975  tfrlem9  8421  findcard2  9208  isinf  9284  findcard3  9302  scott0b  9964  scott0OLD  9965  ac6c4  10586  supaddc  12311  supadd  12312  supmul1  12313  supmul  12316  fsuppmapnn0fiub  14161  mreiincl  17795  restmetu  24919  bposlem3  27643  nosupbnd1  28101  nosupbnd2  28103  noinfbnd1  28116  noinfbnd2  28118  opphllem5  29257  dfprlng2  29455  pjpjpre  32051  atom1d  32985  iinabrex  33235  actfunsnf1o  35303  bnj1398  35734  cvmlift2lem12  36246  finminlem  37284  neibastop2lem  37326  iooelexlt  38477  relowlpssretop  38479  ralssiun  38522  varprop  38834  disjlem18  40027  prtlem18  40126  pell14qrdich  44069  unielss  44412  eliuniin  46319  eliuniin2  46340  eliunid  46367  disjinfi  46412  iunmapsn  46435  infnsuprnmpt  46467  upbdrech  46526  limclner  46866  limsupre3uzlem  46950  climuzlem  46958  sge0iunmptlemre  47630  iundjiun  47675  meaiininclem  47701  isomenndlem  47745  ovnsubaddlem1  47785  vonioo  47897  vonicc  47900  smfaddlem1  47978  f1oresf1o2  48566