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

Theorem spv 2296
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 219 . 2 (𝑥 = 𝑦 → (𝜑𝜓))
32spimv 2293 1 (∀𝑥𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wal 1521
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-12 2087  ax-13 2282
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745
This theorem is referenced by:  chvarv  2299  cbvalv  2309  ru  3467  nalset  4828  isowe2  6640  tfisi  7100  findcard2  8241  marypha1lem  8380  setind  8648  karden  8796  kmlem4  9013  axgroth3  9691  ramcl  15780  alexsubALTlem3  21900  i1fd  23493  dfpo2  31771  dfon2lem6  31817  trer  32435  axc11n-16  34542  elsetrecslem  42770
  Copyright terms: Public domain W3C validator