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 2219	. 2 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) → ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
2		df-rex 3089	. 2 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
3	1, 2	sylibr 237	1 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) → ∃𝑥 ∈ 𝐴 𝜑)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401  ∃wex 1812   ∈ wcel 2145  ∃wrex 3088

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-12 2215

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

This theorem is used by:  rsp2e  3282  2rmorex  3715  2reurex  3721  ssiun2  5010  reusv2lem3  5369  fvelimad  6949  tfrlem9  8377  findcard2  9162  isinf  9238  findcard3  9256  scott0b  9879  scott0OLD  9880  ac6c4  10486  supaddc  12209  supadd  12210  supmul1  12211  supmul  12214  fsuppmapnn0fiub  14057  mreiincl  17684  restmetu  24800  bposlem3  27523  nosupbnd1  27951  nosupbnd2  27953  noinfbnd1  27966  noinfbnd2  27968  opphllem5  29107  dfprlng2  29305  pjpjpre  31901  atom1d  32835  iinabrex  33044  actfunsnf1o  35114  bnj1398  35545  cvmlift2lem12  35895  finminlem  36939  neibastop2lem  36981  iooelexlt  38118  relowlpssretop  38120  ralssiun  38163  disjlem18  39653  prtlem18  39752  pell14qrdich  43712  unielss  44061  eliuniin  45933  eliuniin2  45954  eliunid  45981  disjinfi  46026  iunmapsn  46049  infnsuprnmpt  46081  upbdrech  46140  limclner  46481  limsupre3uzlem  46565  climuzlem  46573  sge0iunmptlemre  47245  iundjiun  47290  meaiininclem  47316  isomenndlem  47360  ovnsubaddlem1  47400  vonioo  47512  vonicc  47515  smfaddlem1  47593  f1oresf1o2  48181