Theorem rspe 3253

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

Assertion

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

Proof of Theorem rspe

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

Syntax hints:   → wi 4   ∧ wa 400  ∃wex 1807   ∈ wcel 2141  ∃wrex 3087

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-12 2211

This theorem depends on definitions:  df-bi 210  df-ex 1808  df-rex 3088

This theorem is referenced by:  rsp2e  3281  2rmorex  3716  2reurex  3722  ssiun2  5011  reusv2lem3  5371  fvelimad  6948  tfrlem9  8371  findcard2  9148  isinf  9224  findcard3  9242  scott0  9859  ac6c4  10464  supaddc  12181  supadd  12182  supmul1  12183  supmul  12186  fsuppmapnn0fiub  14027  mreiincl  17647  restmetu  24706  bposlem3  27426  nosupbnd1  27854  nosupbnd2  27856  noinfbnd1  27869  noinfbnd2  27871  opphllem5  29007  dfprlng2  29170  pjpjpre  31737  atom1d  32671  iinabrex  32880  actfunsnf1o  34957  bnj1398  35388  cvmlift2lem12  35772  finminlem  36795  neibastop2lem  36837  iooelexlt  37974  relowlpssretop  37976  ralssiun  38019  disjlem18  39520  prtlem18  39619  pell14qrdich  43566  unielss  43915  eliuniin  45787  eliuniin2  45808  eliunid  45835  disjinfi  45880  iunmapsn  45903  infnsuprnmpt  45935  upbdrech  45994  limclner  46335  limsupre3uzlem  46419  climuzlem  46427  sge0iunmptlemre  47099  iundjiun  47144  meaiininclem  47170  isomenndlem  47214  ovnsubaddlem1  47254  vonioo  47366  vonicc  47369  smfaddlem1  47447  f1oresf1o2  47995