Theorem rspe 3213

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

Assertion

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

Proof of Theorem rspe

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

Syntax hints:   → wi 4   ∧ wa 399  ∃wex 1787   ∈ wcel 2112  ∃wrex 3052

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-12 2177

This theorem depends on definitions:  df-bi 210  df-ex 1788  df-rex 3057

This theorem is referenced by:  rsp2e  3214  2rmorex  3656  2reurex  3662  ssiun2  4942  reusv2lem3  5278  fvelimad  6757  tfrlem9  8099  findcard2  8820  isinf  8867  findcard2OLD  8891  findcard3  8892  scott0  9467  ac6c4  10060  supaddc  11764  supadd  11765  supmul1  11766  supmul  11769  fsuppmapnn0fiub  13529  mreiincl  17053  restmetu  23422  bposlem3  26121  opphllem5  26796  pjpjpre  29454  atom1d  30388  iinabrex  30581  actfunsnf1o  32250  bnj1398  32681  cvmlift2lem12  32943  nosupbnd1  33603  nosupbnd2  33605  noinfbnd1  33618  noinfbnd2  33620  finminlem  34193  neibastop2lem  34235  iooelexlt  35219  relowlpssretop  35221  ralssiun  35264  prtlem18  36577  pell14qrdich  40335  eliuniin  42263  eliuniin2  42283  eliunid  42313  disjinfi  42345  iunmapsn  42371  infnsuprnmpt  42409  upbdrech  42458  limclner  42810  limsupre3uzlem  42894  climuzlem  42902  sge0iunmptlemre  43571  iundjiun  43616  meaiininclem  43642  isomenndlem  43686  ovnsubaddlem1  43726  vonioo  43838  vonicc  43841  smfaddlem1  43913  f1oresf1o2  44398