Theorem rspe 3232

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

Assertion

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

Proof of Theorem rspe

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

Syntax hints:   → wi 4   ∧ wa 395  ∃wex 1783   ∈ wcel 2108  ∃wrex 3064

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-12 2173

This theorem depends on definitions:  df-bi 206  df-ex 1784  df-rex 3069

This theorem is referenced by:  rsp2e  3233  2rmorex  3684  2reurex  3690  ssiun2  4973  reusv2lem3  5318  fvelimad  6818  tfrlem9  8187  findcard2  8909  isinf  8965  findcard2OLD  8986  findcard3  8987  scott0  9575  ac6c4  10168  supaddc  11872  supadd  11873  supmul1  11874  supmul  11877  fsuppmapnn0fiub  13639  mreiincl  17222  restmetu  23632  bposlem3  26339  opphllem5  27016  pjpjpre  29682  atom1d  30616  iinabrex  30809  actfunsnf1o  32484  bnj1398  32914  cvmlift2lem12  33176  nosupbnd1  33844  nosupbnd2  33846  noinfbnd1  33859  noinfbnd2  33861  finminlem  34434  neibastop2lem  34476  iooelexlt  35460  relowlpssretop  35462  ralssiun  35505  prtlem18  36818  pell14qrdich  40607  eliuniin  42538  eliuniin2  42558  eliunid  42588  disjinfi  42620  iunmapsn  42646  infnsuprnmpt  42685  upbdrech  42734  limclner  43082  limsupre3uzlem  43166  climuzlem  43174  sge0iunmptlemre  43843  iundjiun  43888  meaiininclem  43914  isomenndlem  43958  ovnsubaddlem1  43998  vonioo  44110  vonicc  44113  smfaddlem1  44185  f1oresf1o2  44670