Theorem rspe 3247

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

Assertion

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

Proof of Theorem rspe

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

Syntax hints:   → wi 4   ∧ wa 395  ∃wex 1776   ∈ wcel 2106  ∃wrex 3068

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-12 2175

This theorem depends on definitions:  df-bi 207  df-ex 1777  df-rex 3069

This theorem is referenced by:  rsp2e  3276  2rmorex  3763  2reurex  3769  ssiun2  5052  reusv2lem3  5406  fvelimad  6976  tfrlem9  8424  findcard2  9203  isinf  9294  isinfOLD  9295  findcard3  9316  findcard3OLD  9317  scott0  9924  ac6c4  10519  supaddc  12233  supadd  12234  supmul1  12235  supmul  12238  fsuppmapnn0fiub  14029  mreiincl  17641  restmetu  24599  bposlem3  27345  nosupbnd1  27774  nosupbnd2  27776  noinfbnd1  27789  noinfbnd2  27791  opphllem5  28774  pjpjpre  31448  atom1d  32382  iinabrex  32589  actfunsnf1o  34598  bnj1398  35027  cvmlift2lem12  35299  finminlem  36301  neibastop2lem  36343  iooelexlt  37345  relowlpssretop  37347  ralssiun  37390  disjlem18  38782  prtlem18  38859  pell14qrdich  42857  unielss  43207  eliuniin  45039  eliuniin2  45060  eliunid  45090  disjinfi  45135  iunmapsn  45160  infnsuprnmpt  45195  upbdrech  45256  limclner  45607  limsupre3uzlem  45691  climuzlem  45699  sge0iunmptlemre  46371  iundjiun  46416  meaiininclem  46442  isomenndlem  46486  ovnsubaddlem1  46526  vonioo  46638  vonicc  46641  smfaddlem1  46719  tworepnotupword  46840  f1oresf1o2  47241