Theorem rspe 3255

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

Assertion

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

Proof of Theorem rspe

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

Syntax hints:   → wi 4   ∧ wa 395  ∃wex 1777   ∈ wcel 2108  ∃wrex 3076

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-12 2178

This theorem depends on definitions:  df-bi 207  df-ex 1778  df-rex 3077

This theorem is referenced by:  rsp2e  3284  2rmorex  3776  2reurex  3782  ssiun2  5070  reusv2lem3  5418  fvelimad  6989  tfrlem9  8441  findcard2  9230  isinf  9323  isinfOLD  9324  findcard3  9346  findcard3OLD  9347  scott0  9955  ac6c4  10550  supaddc  12262  supadd  12263  supmul1  12264  supmul  12267  fsuppmapnn0fiub  14042  mreiincl  17654  restmetu  24604  bposlem3  27348  nosupbnd1  27777  nosupbnd2  27779  noinfbnd1  27792  noinfbnd2  27794  opphllem5  28777  pjpjpre  31451  atom1d  32385  iinabrex  32591  actfunsnf1o  34581  bnj1398  35010  cvmlift2lem12  35282  finminlem  36284  neibastop2lem  36326  iooelexlt  37328  relowlpssretop  37330  ralssiun  37373  disjlem18  38756  prtlem18  38833  pell14qrdich  42825  unielss  43179  eliuniin  45001  eliuniin2  45022  eliunid  45052  disjinfi  45099  iunmapsn  45124  infnsuprnmpt  45159  upbdrech  45220  limclner  45572  limsupre3uzlem  45656  climuzlem  45664  sge0iunmptlemre  46336  iundjiun  46381  meaiininclem  46407  isomenndlem  46451  ovnsubaddlem1  46491  vonioo  46603  vonicc  46606  smfaddlem1  46684  tworepnotupword  46805  f1oresf1o2  47206