Theorem rspe 2986

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

Assertion

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

Proof of Theorem rspe

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

Syntax hints:   → wi 4   ∧ wa 383  ∃wex 1695   ∈ wcel 1977  ∃wrex 2897

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-12 2034

This theorem depends on definitions:  df-bi 196  df-ex 1696  df-rex 2902

This theorem is referenced by:  rsp2e  2987  2rmorex  3379  ssiun2  4499  reusv2lem3  4797  tfrlem9  7368  isinf  8058  findcard2  8085  findcard3  8088  scott0  8632  ac6c4  9186  supaddc  10867  supadd  10868  supmul1  10869  supmul  10872  fsuppmapnn0fiub  12652  mreiincl  16079  restmetu  22185  bposlem3  24811  opphllem5  25443  pjpjpre  27662  atom1d  28596  bnj1398  30356  cvmlift2lem12  30550  finminlem  31482  neibastop2lem  31525  iooelexlt  32386  relowlpssretop  32388  prtlem18  33180  pell14qrdich  36451  eliuniin  38307  eliuniin2  38335  disjinfi  38375  iunmapsn  38404  upbdrech  38460  limclner  38718  sge0iunmptlemre  39308  iundjiun  39353  meaiininclem  39376  isomenndlem  39420  ovnsubaddlem1  39460  vonioo  39573  vonicc  39576  smfaddlem1  39649  2reurex  39830