Theorem rspe 3219

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

Assertion

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

Proof of Theorem rspe

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

Syntax hints:   → wi 4   ∧ wa 395  ∃wex 1779   ∈ wcel 2109  ∃wrex 3053

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-12 2178

This theorem depends on definitions:  df-bi 207  df-ex 1780  df-rex 3054

This theorem is referenced by:  rsp2e  3247  2rmorex  3716  2reurex  3722  ssiun2  4999  reusv2lem3  5342  fvelimad  6894  tfrlem9  8314  findcard2  9088  isinf  9165  isinfOLD  9166  findcard3  9187  findcard3OLD  9188  scott0  9801  ac6c4  10394  supaddc  12110  supadd  12111  supmul1  12112  supmul  12115  fsuppmapnn0fiub  13916  mreiincl  17516  restmetu  24474  bposlem3  27213  nosupbnd1  27642  nosupbnd2  27644  noinfbnd1  27657  noinfbnd2  27659  opphllem5  28714  pjpjpre  31381  atom1d  32315  iinabrex  32531  actfunsnf1o  34571  bnj1398  35000  cvmlift2lem12  35286  finminlem  36291  neibastop2lem  36333  iooelexlt  37335  relowlpssretop  37337  ralssiun  37380  disjlem18  38777  prtlem18  38855  pell14qrdich  42842  unielss  43191  eliuniin  45077  eliuniin2  45098  eliunid  45125  disjinfi  45170  iunmapsn  45195  infnsuprnmpt  45228  upbdrech  45287  limclner  45633  limsupre3uzlem  45717  climuzlem  45725  sge0iunmptlemre  46397  iundjiun  46442  meaiininclem  46468  isomenndlem  46512  ovnsubaddlem1  46552  vonioo  46664  vonicc  46667  smfaddlem1  46745  tworepnotupword  46868  f1oresf1o2  47276