Theorem rspe 3254

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

Assertion

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

Proof of Theorem rspe

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 400  ∃wex 1808   ∈ wcel 2142  ∃wrex 3088

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-12 2212

This proof depends on definitions:  df-bi 210  df-ex 1809  df-rex 3089

This theorem is used by:  rsp2e  3282  2rmorex  3716  2reurex  3722  ssiun2  5011  reusv2lem3  5370  fvelimad  6948  tfrlem9  8370  findcard2  9147  isinf  9223  findcard3  9241  scott0b  9864  scott0OLD  9865  ac6c4  10471  supaddc  12188  supadd  12189  supmul1  12190  supmul  12193  fsuppmapnn0fiub  14034  mreiincl  17654  restmetu  24738  bposlem3  27461  nosupbnd1  27889  nosupbnd2  27891  noinfbnd1  27904  noinfbnd2  27906  opphllem5  29043  dfprlng2  29208  pjpjpre  31782  atom1d  32716  iinabrex  32925  actfunsnf1o  35000  bnj1398  35431  cvmlift2lem12  35814  finminlem  36857  neibastop2lem  36899  iooelexlt  38036  relowlpssretop  38038  ralssiun  38081  disjlem18  39580  prtlem18  39679  pell14qrdich  43624  unielss  43973  eliuniin  45845  eliuniin2  45866  eliunid  45893  disjinfi  45938  iunmapsn  45961  infnsuprnmpt  45993  upbdrech  46052  limclner  46393  limsupre3uzlem  46477  climuzlem  46485  sge0iunmptlemre  47157  iundjiun  47202  meaiininclem  47228  isomenndlem  47272  ovnsubaddlem1  47312  vonioo  47424  vonicc  47427  smfaddlem1  47505  f1oresf1o2  48056