Theorem rspe 3247

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

Assertion

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

Proof of Theorem rspe

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

Syntax hints:   → wi 4   ∧ wa 397  ∃wex 1782   ∈ wcel 2107  ∃wrex 3071

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-12 2172

This theorem depends on definitions:  df-bi 206  df-ex 1783  df-rex 3072

This theorem is referenced by:  rsp2e  3276  2rmorex  3751  2reurex  3757  ssiun2  5051  reusv2lem3  5399  fvelimad  6960  tfrlem9  8385  findcard2  9164  isinf  9260  isinfOLD  9261  findcard2OLD  9284  findcard3  9285  findcard3OLD  9286  scott0  9881  ac6c4  10476  supaddc  12181  supadd  12182  supmul1  12183  supmul  12186  fsuppmapnn0fiub  13956  mreiincl  17540  restmetu  24079  bposlem3  26789  nosupbnd1  27217  nosupbnd2  27219  noinfbnd1  27232  noinfbnd2  27234  opphllem5  28002  pjpjpre  30672  atom1d  31606  iinabrex  31800  actfunsnf1o  33616  bnj1398  34045  cvmlift2lem12  34305  finminlem  35203  neibastop2lem  35245  iooelexlt  36243  relowlpssretop  36245  ralssiun  36288  disjlem18  37670  prtlem18  37747  pell14qrdich  41607  unielss  41967  eliuniin  43788  eliuniin2  43809  eliunid  43839  disjinfi  43891  iunmapsn  43916  infnsuprnmpt  43954  upbdrech  44015  limclner  44367  limsupre3uzlem  44451  climuzlem  44459  sge0iunmptlemre  45131  iundjiun  45176  meaiininclem  45202  isomenndlem  45246  ovnsubaddlem1  45286  vonioo  45398  vonicc  45401  smfaddlem1  45479  tworepnotupword  45600  f1oresf1o2  45999