Theorem rspe 3227

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

Assertion

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

Proof of Theorem rspe

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

Syntax hints:   → wi 4   ∧ wa 395  ∃wex 1781   ∈ wcel 2114  ∃wrex 3061

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-12 2185

This theorem depends on definitions:  df-bi 207  df-ex 1782  df-rex 3062

This theorem is referenced by:  rsp2e  3255  2rmorex  3713  2reurex  3719  ssiun2  5004  reusv2lem3  5346  fvelimad  6902  tfrlem9  8318  findcard2  9093  isinf  9169  findcard3  9187  scott0  9802  ac6c4  10395  supaddc  12113  supadd  12114  supmul1  12115  supmul  12118  fsuppmapnn0fiub  13918  mreiincl  17519  restmetu  24518  bposlem3  27257  nosupbnd1  27686  nosupbnd2  27688  noinfbnd1  27701  noinfbnd2  27703  opphllem5  28806  pjpjpre  31477  atom1d  32411  iinabrex  32626  actfunsnf1o  34742  bnj1398  35171  cvmlift2lem12  35489  finminlem  36493  neibastop2lem  36535  iooelexlt  37538  relowlpssretop  37540  ralssiun  37583  disjlem18  39075  prtlem18  39174  pell14qrdich  43147  unielss  43496  eliuniin  45379  eliuniin2  45400  eliunid  45427  disjinfi  45472  iunmapsn  45497  infnsuprnmpt  45530  upbdrech  45589  limclner  45931  limsupre3uzlem  46015  climuzlem  46023  sge0iunmptlemre  46695  iundjiun  46740  meaiininclem  46766  isomenndlem  46810  ovnsubaddlem1  46850  vonioo  46962  vonicc  46965  smfaddlem1  47043  f1oresf1o2  47573