Theorem rspe 3244

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

Assertion

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

Proof of Theorem rspe

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

Syntax hints:   → wi 4   ∧ wa 394  ∃wex 1773   ∈ wcel 2098  ∃wrex 3067

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-12 2166

This theorem depends on definitions:  df-bi 206  df-ex 1774  df-rex 3068

This theorem is referenced by:  rsp2e  3273  2rmorex  3751  2reurex  3757  ssiun2  5054  reusv2lem3  5404  fvelimad  6971  tfrlem9  8412  findcard2  9195  isinf  9291  isinfOLD  9292  findcard2OLD  9315  findcard3  9316  findcard3OLD  9317  scott0  9917  ac6c4  10512  supaddc  12219  supadd  12220  supmul1  12221  supmul  12224  fsuppmapnn0fiub  13996  mreiincl  17583  restmetu  24499  bposlem3  27239  nosupbnd1  27667  nosupbnd2  27669  noinfbnd1  27682  noinfbnd2  27684  opphllem5  28575  pjpjpre  31249  atom1d  32183  iinabrex  32380  actfunsnf1o  34269  bnj1398  34698  cvmlift2lem12  34957  finminlem  35835  neibastop2lem  35877  iooelexlt  36874  relowlpssretop  36876  ralssiun  36919  disjlem18  38304  prtlem18  38381  pell14qrdich  42320  unielss  42677  eliuniin  44496  eliuniin2  44517  eliunid  44547  disjinfi  44595  iunmapsn  44620  infnsuprnmpt  44655  upbdrech  44716  limclner  45068  limsupre3uzlem  45152  climuzlem  45160  sge0iunmptlemre  45832  iundjiun  45877  meaiininclem  45903  isomenndlem  45947  ovnsubaddlem1  45987  vonioo  46099  vonicc  46102  smfaddlem1  46180  tworepnotupword  46301  f1oresf1o2  46700