Theorem rspe 3304

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

Assertion

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

Proof of Theorem rspe

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

Syntax hints:   → wi 4   ∧ wa 398  ∃wex 1776   ∈ wcel 2110  ∃wrex 3139

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-12 2173

This theorem depends on definitions:  df-bi 209  df-ex 1777  df-rex 3144

This theorem is referenced by:  rsp2e  3305  2rmorex  3744  2reurex  3749  ssiun2  4963  reusv2lem3  5292  fvelimad  6726  tfrlem9  8015  isinf  8725  findcard2  8752  findcard3  8755  scott0  9309  ac6c4  9897  supaddc  11602  supadd  11603  supmul1  11604  supmul  11607  fsuppmapnn0fiub  13353  mreiincl  16861  restmetu  23174  bposlem3  25856  opphllem5  26531  pjpjpre  29190  atom1d  30124  actfunsnf1o  31870  bnj1398  32301  cvmlift2lem12  32556  nosupbnd1  33209  nosupbnd2  33211  finminlem  33661  neibastop2lem  33703  iooelexlt  34637  relowlpssretop  34639  ralssiun  34682  prtlem18  36007  pell14qrdich  39459  eliuniin  41358  eliuniin2  41379  eliunid  41412  disjinfi  41447  iunmapsn  41473  infnsuprnmpt  41515  upbdrech  41565  limclner  41925  limsupre3uzlem  42009  climuzlem  42017  sge0iunmptlemre  42691  iundjiun  42736  meaiininclem  42762  isomenndlem  42806  ovnsubaddlem1  42846  vonioo  42958  vonicc  42961  smfaddlem1  43033  f1oresf1o2  43484