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

Theorem spcv 3603
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 3592 . 2 (𝐴 ∈ V → (∀𝑥𝜑𝜓))
41, 3ax-mp 5 1 (∀𝑥𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wal 1526   = wceq 1528  wcel 2105  Vcvv 3492
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-v 3494
This theorem is referenced by:  morex  3707  al0ssb  5203  rext  5331  relop  5714  frxp  7809  pssnn  8724  findcard  8745  fiint  8783  marypha1lem  8885  dfom3  9098  elom3  9099  aceq3lem  9534  dfac3  9535  dfac5lem4  9540  dfac8  9549  dfac9  9550  dfacacn  9555  dfac13  9556  kmlem1  9564  kmlem10  9573  fin23lem34  9756  fin23lem35  9757  zorn2lem7  9912  zornn0g  9915  axgroth6  10238  nnunb  11881  symggen  18527  gsumval3lem2  18955  gsumzaddlem  18970  dfac14  22154  i1fd  24209  chlimi  28938  ddemeas  31394  dfpo2  32888  dfon2lem4  32928  dfon2lem5  32929  dfon2lem7  32931  ttac  39511  dfac11  39540  dfac21  39544  setrec2fun  44723
  Copyright terms: Public domain W3C validator