Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  rspe Structured version   Visualization version   GIF version

Theorem rspe 2997
 Description: Restricted specialization. (Contributed by NM, 12-Oct-1999.)
Assertion
Ref Expression
rspe ((𝑥𝐴𝜑) → ∃𝑥𝐴 𝜑)

Proof of Theorem rspe
StepHypRef Expression
1 19.8a 2049 . 2 ((𝑥𝐴𝜑) → ∃𝑥(𝑥𝐴𝜑))
2 df-rex 2913 . 2 (∃𝑥𝐴 𝜑 ↔ ∃𝑥(𝑥𝐴𝜑))
31, 2sylibr 224 1 ((𝑥𝐴𝜑) → ∃𝑥𝐴 𝜑)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 384  ∃wex 1701   ∈ wcel 1987  ∃wrex 2908 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-12 2044 This theorem depends on definitions:  df-bi 197  df-ex 1702  df-rex 2913 This theorem is referenced by:  rsp2e  2998  2rmorex  3394  ssiun2  4529  reusv2lem3  4831  tfrlem9  7426  isinf  8117  findcard2  8144  findcard3  8147  scott0  8693  ac6c4  9247  supaddc  10934  supadd  10935  supmul1  10936  supmul  10939  fsuppmapnn0fiub  12730  mreiincl  16177  restmetu  22285  bposlem3  24911  opphllem5  25543  pjpjpre  28127  atom1d  29061  bnj1398  30810  cvmlift2lem12  31004  finminlem  31954  neibastop2lem  31997  iooelexlt  32842  relowlpssretop  32844  prtlem18  33642  pell14qrdich  36913  eliuniin  38764  eliuniin2  38791  disjinfi  38854  iunmapsn  38883  fvelimad  38933  infnsuprnmpt  38941  upbdrech  38983  limclner  39287  limsupre3uzlem  39371  sge0iunmptlemre  39939  iundjiun  39984  meaiininclem  40007  isomenndlem  40051  ovnsubaddlem1  40091  vonioo  40203  vonicc  40206  smfaddlem1  40278  2reurex  40485
 Copyright terms: Public domain W3C validator