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

Theorem spcv 3604
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 3593 . 2 (𝐴 ∈ V → (∀𝑥𝜑𝜓))
41, 3ax-mp 5 1 (∀𝑥𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 208  wal 1528   = wceq 1530  wcel 2107  Vcvv 3493
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-ext 2791
This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1774  df-sb 2063  df-clab 2798  df-cleq 2812  df-clel 2891  df-v 3495
This theorem is referenced by:  morex  3708  al0ssb  5203  rext  5331  relop  5714  frxp  7812  pssnn  8728  findcard  8749  fiint  8787  marypha1lem  8889  dfom3  9102  elom3  9103  aceq3lem  9538  dfac3  9539  dfac5lem4  9544  dfac8  9553  dfac9  9554  dfacacn  9559  dfac13  9560  kmlem1  9568  kmlem10  9577  fin23lem34  9760  fin23lem35  9761  zorn2lem7  9916  zornn0g  9919  axgroth6  10242  nnunb  11885  symggen  18590  gsumval3lem2  19018  gsumzaddlem  19033  dfac14  22218  i1fd  24274  chlimi  29003  ddemeas  31483  dfpo2  32979  dfon2lem4  33019  dfon2lem5  33020  dfon2lem7  33022  ttac  39618  dfac11  39647  dfac21  39651  setrec2fun  44780
  Copyright terms: Public domain W3C validator