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

Theorem spcv 3567
Description: Rule of specialization, using implicit substitution. (Contributed by NM, 22-Jun-1994.)
Hypotheses
Ref Expression
spcv.1 𝐴 ∈ V
spcv.2 (𝑥 = 𝐴 → (𝜑𝜓))
Assertion
Ref Expression
spcv (∀𝑥𝜑𝜓)
Distinct variable groups:   𝑥,𝐴   𝜓,𝑥
Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem spcv
StepHypRef Expression
1 spcv.1 . 2 𝐴 ∈ V
2 spcv.2 . . 3 (𝑥 = 𝐴 → (𝜑𝜓))
32spcgv 3558 . 2 (𝐴 ∈ V → (∀𝑥𝜑𝜓))
41, 3ax-mp 5 1 (∀𝑥𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wal 1540   = wceq 1542  wcel 2107  Vcvv 3448
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-v 3450
This theorem is referenced by:  morex  3682  al0ssb  5270  rext  5410  relop  5811  dfpo2  6253  frxp  8063  frxp2  8081  findcard  9114  pssnn  9119  ssfi  9124  pssnnOLD  9216  fiint  9275  marypha1lem  9376  dfom3  9590  elom3  9591  ttrclss  9663  aceq3lem  10063  dfac3  10064  dfac5lem4  10069  dfac8  10078  dfac9  10079  dfacacn  10084  dfac13  10085  kmlem1  10093  kmlem10  10102  fin23lem34  10289  fin23lem35  10290  zorn2lem7  10445  zornn0g  10448  axgroth6  10771  nnunb  12416  symggen  19259  gsumval3lem2  19690  gsumzaddlem  19705  dfac14  22985  i1fd  25061  chlimi  30218  zarclssn  32494  ddemeas  32875  dfon2lem4  34400  dfon2lem5  34401  dfon2lem7  34403  ttac  41389  dfac11  41418  dfac21  41422  setrec2fun  47211
  Copyright terms: Public domain W3C validator