Theorem rspe 3234

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

Assertion

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

Proof of Theorem rspe

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

Syntax hints:   → wi 4   ∧ wa 395  ∃wex 1785   ∈ wcel 2109  ∃wrex 3066

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-12 2174

This theorem depends on definitions:  df-bi 206  df-ex 1786  df-rex 3071

This theorem is referenced by:  rsp2e  3235  2rmorex  3692  2reurex  3698  ssiun2  4981  reusv2lem3  5326  fvelimad  6830  tfrlem9  8200  findcard2  8912  isinf  8997  findcard2OLD  9017  findcard3  9018  scott0  9628  ac6c4  10221  supaddc  11925  supadd  11926  supmul1  11927  supmul  11930  fsuppmapnn0fiub  13692  mreiincl  17286  restmetu  23707  bposlem3  26415  opphllem5  27093  pjpjpre  29760  atom1d  30694  iinabrex  30887  actfunsnf1o  32563  bnj1398  32993  cvmlift2lem12  33255  nosupbnd1  33896  nosupbnd2  33898  noinfbnd1  33911  noinfbnd2  33913  finminlem  34486  neibastop2lem  34528  iooelexlt  35512  relowlpssretop  35514  ralssiun  35557  prtlem18  36870  pell14qrdich  40671  eliuniin  42602  eliuniin2  42622  eliunid  42652  disjinfi  42684  iunmapsn  42710  infnsuprnmpt  42749  upbdrech  42798  limclner  43146  limsupre3uzlem  43230  climuzlem  43238  sge0iunmptlemre  43907  iundjiun  43952  meaiininclem  43978  isomenndlem  44022  ovnsubaddlem1  44062  vonioo  44174  vonicc  44177  smfaddlem1  44249  f1oresf1o2  44734