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

Theorem spv 2248
Description: Specialization, using implicit substitution. (Contributed by NM, 30-Aug-1993.)
Hypothesis
Ref Expression
spv.1 (𝑥 = 𝑦 → (𝜑𝜓))
Assertion
Ref Expression
spv (∀𝑥𝜑𝜓)
Distinct variable group:   𝜓,𝑥
Allowed substitution hints:   𝜑(𝑥,𝑦)   𝜓(𝑦)

Proof of Theorem spv
StepHypRef Expression
1 spv.1 . . 3 (𝑥 = 𝑦 → (𝜑𝜓))
21biimpd 218 . 2 (𝑥 = 𝑦 → (𝜑𝜓))
32spimv 2245 1 (∀𝑥𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 195  wal 1473
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-12 2034  ax-13 2234
This theorem depends on definitions:  df-bi 196  df-an 385  df-ex 1696
This theorem is referenced by:  chvarv  2251  cbvalv  2261  ru  3401  nalset  4723  isowe2  6500  tfisi  6950  findcard2  8085  marypha1lem  8222  setind  8493  karden  8641  kmlem4  8858  axgroth3  9532  ramcl  15571  alexsubALTlem3  21663  i1fd  23254  dfpo2  30898  dfon2lem6  30937  trer  31480  axc11n-16  33241  elsetrecslem  42243
  Copyright terms: Public domain W3C validator