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

Theorem spvv 2000
Description: Specialization, using implicit substitution. Version of spv 2392 with a disjoint variable condition, which does not require ax-7 2011, ax-12 2171, ax-13 2371. (Contributed by NM, 30-Aug-1993.) (Revised by BJ, 31-May-2019.)
Hypothesis
Ref Expression
spvv.1 (𝑥 = 𝑦 → (𝜑𝜓))
Assertion
Ref Expression
spvv (∀𝑥𝜑𝜓)
Distinct variable groups:   𝑥,𝑦   𝜓,𝑥
Allowed substitution hints:   𝜑(𝑥,𝑦)   𝜓(𝑦)

Proof of Theorem spvv
StepHypRef Expression
1 spvv.1 . . 3 (𝑥 = 𝑦 → (𝜑𝜓))
21biimpd 228 . 2 (𝑥 = 𝑦 → (𝜑𝜓))
32spimvw 1999 1 (∀𝑥𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wal 1539
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971
This theorem depends on definitions:  df-bi 206  df-ex 1782
This theorem is referenced by:  chvarvv  2002  nfcr  2888  ru  3776  nalset  5313  dfpo2  6295  isowe2  7349  tfisi  7850  findcard2  9166  findcard2OLD  9286  marypha1lem  9430  setind  9731  karden  9892  kmlem4  10150  axgroth3  10828  ramcl  16964  alexsubALTlem3  23560  i1fd  25205  dfon2lem6  34835  trer  35293  bj-ru0  35915  eleq2w2ALT  36020  elsetrecslem  47828
  Copyright terms: Public domain W3C validator