Theorem rspe 3299

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

Assertion

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

Proof of Theorem rspe

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

Syntax hints:   → wi 4   ∧ wa 398  ∃wex 1780   ∈ wcel 2114  ∃wrex 3134

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 1970  ax-7 2015  ax-12 2177

This theorem depends on definitions:  df-bi 209  df-ex 1781  df-rex 3139

This theorem is referenced by:  rsp2e  3300  2rmorex  3731  2reurex  3736  ssiun2  4952  reusv2lem3  5282  fvelimad  6713  tfrlem9  8002  isinf  8712  findcard2  8739  findcard3  8742  scott0  9296  ac6c4  9884  supaddc  11589  supadd  11590  supmul1  11591  supmul  11594  fsuppmapnn0fiub  13344  mreiincl  16845  restmetu  23158  bposlem3  25843  opphllem5  26518  pjpjpre  29175  atom1d  30109  actfunsnf1o  31877  bnj1398  32308  cvmlift2lem12  32563  nosupbnd1  33216  nosupbnd2  33218  finminlem  33668  neibastop2lem  33710  iooelexlt  34654  relowlpssretop  34656  ralssiun  34699  prtlem18  36040  pell14qrdich  39553  eliuniin  41450  eliuniin2  41471  eliunid  41504  disjinfi  41539  iunmapsn  41565  infnsuprnmpt  41607  upbdrech  41657  limclner  42017  limsupre3uzlem  42101  climuzlem  42109  sge0iunmptlemre  42782  iundjiun  42827  meaiininclem  42853  isomenndlem  42897  ovnsubaddlem1  42937  vonioo  43049  vonicc  43052  smfaddlem1  43124  f1oresf1o2  43575