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  3714  2reurex  3720  ssiun2  5005  reusv2lem3  5347  fvelimad  6909  tfrlem9  8326  findcard2  9101  isinf  9177  findcard3  9195  scott0  9810  ac6c4  10403  supaddc  12121  supadd  12122  supmul1  12123  supmul  12126  fsuppmapnn0fiub  13926  mreiincl  17527  restmetu  24526  bposlem3  27265  nosupbnd1  27694  nosupbnd2  27696  noinfbnd1  27709  noinfbnd2  27711  opphllem5  28835  pjpjpre  31506  atom1d  32440  iinabrex  32655  actfunsnf1o  34781  bnj1398  35209  cvmlift2lem12  35527  finminlem  36531  neibastop2lem  36573  iooelexlt  37606  relowlpssretop  37608  ralssiun  37651  disjlem18  39143  prtlem18  39242  pell14qrdich  43215  unielss  43564  eliuniin  45447  eliuniin2  45468  eliunid  45495  disjinfi  45540  iunmapsn  45564  infnsuprnmpt  45597  upbdrech  45656  limclner  45998  limsupre3uzlem  46082  climuzlem  46090  sge0iunmptlemre  46762  iundjiun  46807  meaiininclem  46833  isomenndlem  46877  ovnsubaddlem1  46917  vonioo  47029  vonicc  47032  smfaddlem1  47110  f1oresf1o2  47640