Theorem rspe 3224

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

Assertion

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

Proof of Theorem rspe

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

Syntax hints:   → wi 4   ∧ wa 395  ∃wex 1780   ∈ wcel 2113  ∃wrex 3058

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 2182

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

This theorem is referenced by:  rsp2e  3252  2rmorex  3710  2reurex  3716  ssiun2  5000  reusv2lem3  5342  fvelimad  6898  tfrlem9  8313  findcard2  9084  isinf  9159  findcard3  9177  scott0  9789  ac6c4  10382  supaddc  12099  supadd  12100  supmul1  12101  supmul  12104  fsuppmapnn0fiub  13908  mreiincl  17508  restmetu  24495  bposlem3  27234  nosupbnd1  27663  nosupbnd2  27665  noinfbnd1  27678  noinfbnd2  27680  opphllem5  28739  pjpjpre  31410  atom1d  32344  iinabrex  32560  actfunsnf1o  34628  bnj1398  35057  cvmlift2lem12  35369  finminlem  36373  neibastop2lem  36415  iooelexlt  37417  relowlpssretop  37419  ralssiun  37462  disjlem18  38908  prtlem18  38986  pell14qrdich  42976  unielss  43325  eliuniin  45210  eliuniin2  45231  eliunid  45258  disjinfi  45303  iunmapsn  45328  infnsuprnmpt  45361  upbdrech  45420  limclner  45763  limsupre3uzlem  45847  climuzlem  45855  sge0iunmptlemre  46527  iundjiun  46572  meaiininclem  46598  isomenndlem  46642  ovnsubaddlem1  46682  vonioo  46794  vonicc  46797  smfaddlem1  46875  f1oresf1o2  47405