Theorem rspe 3243

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

Assertion

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

Proof of Theorem rspe

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

Syntax hints:   → wi 4   ∧ wa 387  ∃wex 1742   ∈ wcel 2050  ∃wrex 3083

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-12 2106

This theorem depends on definitions:  df-bi 199  df-ex 1743  df-rex 3088

This theorem is referenced by:  rsp2e  3244  2rmorex  3648  2reurex  3653  ssiun2  4831  reusv2lem3  5148  tfrlem9  7819  isinf  8520  findcard2  8547  findcard3  8550  scott0  9103  ac6c4  9695  supaddc  11403  supadd  11404  supmul1  11405  supmul  11408  fsuppmapnn0fiub  13168  mreiincl  16719  restmetu  22877  bposlem3  25558  opphllem5  26233  pjpjpre  28971  atom1d  29905  actfunsnf1o  31523  bnj1398  31951  cvmlift2lem12  32146  nosupbnd1  32735  nosupbnd2  32737  finminlem  33187  neibastop2lem  33229  iooelexlt  34085  relowlpssretop  34087  ralssiun  34129  prtlem18  35458  pell14qrdich  38862  eliuniin  40787  eliuniin2  40809  eliunid  40841  disjinfi  40878  iunmapsn  40905  fvelimad  40945  infnsuprnmpt  40950  upbdrech  41001  limclner  41363  limsupre3uzlem  41447  climuzlem  41455  sge0iunmptlemre  42128  iundjiun  42173  meaiininclem  42199  isomenndlem  42243  ovnsubaddlem1  42283  vonioo  42395  vonicc  42398  smfaddlem1  42470  f1oresf1o2  42896