Theorem rspe 3220

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

Assertion

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

Proof of Theorem rspe

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

Syntax hints:   → wi 4   ∧ wa 395  ∃wex 1780   ∈ wcel 2110  ∃wrex 3054

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-12 2179

This theorem depends on definitions:  df-bi 207  df-ex 1781  df-rex 3055

This theorem is referenced by:  rsp2e  3248  2rmorex  3711  2reurex  3717  ssiun2  4994  reusv2lem3  5336  fvelimad  6884  tfrlem9  8299  findcard2  9069  isinf  9144  findcard3  9162  scott0  9771  ac6c4  10364  supaddc  12081  supadd  12082  supmul1  12083  supmul  12086  fsuppmapnn0fiub  13890  mreiincl  17490  restmetu  24478  bposlem3  27217  nosupbnd1  27646  nosupbnd2  27648  noinfbnd1  27661  noinfbnd2  27663  opphllem5  28722  pjpjpre  31389  atom1d  32323  iinabrex  32539  actfunsnf1o  34607  bnj1398  35036  cvmlift2lem12  35326  finminlem  36331  neibastop2lem  36373  iooelexlt  37375  relowlpssretop  37377  ralssiun  37420  disjlem18  38817  prtlem18  38895  pell14qrdich  42881  unielss  43230  eliuniin  45115  eliuniin2  45136  eliunid  45163  disjinfi  45208  iunmapsn  45233  infnsuprnmpt  45266  upbdrech  45325  limclner  45668  limsupre3uzlem  45752  climuzlem  45760  sge0iunmptlemre  46432  iundjiun  46477  meaiininclem  46503  isomenndlem  46547  ovnsubaddlem1  46587  vonioo  46699  vonicc  46702  smfaddlem1  46780  f1oresf1o2  47301