Theorem rspe 3228

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

Assertion

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

Proof of Theorem rspe

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

Syntax hints:   → wi 4   ∧ wa 395  ∃wex 1781   ∈ wcel 2114  ∃wrex 3062

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-12 2185

This theorem depends on definitions:  df-bi 207  df-ex 1782  df-rex 3063

This theorem is referenced by:  rsp2e  3256  2rmorex  3701  2reurex  3707  ssiun2  4991  reusv2lem3  5343  fvelimad  6908  tfrlem9  8324  findcard2  9099  isinf  9175  findcard3  9193  scott0  9810  ac6c4  10403  supaddc  12123  supadd  12124  supmul1  12125  supmul  12128  fsuppmapnn0fiub  13953  mreiincl  17558  restmetu  24535  bposlem3  27249  nosupbnd1  27678  nosupbnd2  27680  noinfbnd1  27693  noinfbnd2  27695  opphllem5  28819  pjpjpre  31490  atom1d  32424  iinabrex  32639  actfunsnf1o  34748  bnj1398  35176  cvmlift2lem12  35496  finminlem  36500  neibastop2lem  36542  iooelexlt  37678  relowlpssretop  37680  ralssiun  37723  disjlem18  39224  prtlem18  39323  pell14qrdich  43297  unielss  43646  eliuniin  45529  eliuniin2  45550  eliunid  45577  disjinfi  45622  iunmapsn  45646  infnsuprnmpt  45679  upbdrech  45738  limclner  46079  limsupre3uzlem  46163  climuzlem  46171  sge0iunmptlemre  46843  iundjiun  46888  meaiininclem  46914  isomenndlem  46958  ovnsubaddlem1  46998  vonioo  47110  vonicc  47113  smfaddlem1  47191  f1oresf1o2  47733