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

Theorem spvv 1996
Description: Specialization, using implicit substitution. Version of spv 2398 with a disjoint variable condition, which does not require ax-7 2007, ax-12 2177, ax-13 2377. (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 229 . 2 (𝑥 = 𝑦 → (𝜑𝜓))
32spimvw 1995 1 (∀𝑥𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wal 1538
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967
This theorem depends on definitions:  df-bi 207  df-ex 1780
This theorem is referenced by:  chvarvv  1998  ru0  2127  nfcr  2895  ruOLD  3787  nalset  5313  dfpo2  6316  isowe2  7370  tfisi  7880  findcard2  9204  marypha1lem  9473  setind  9774  karden  9935  kmlem4  10194  axgroth3  10871  ramcl  17067  cnsubrglem  21434  alexsubALTlem3  24057  i1fd  25716  dfon2lem6  35789  trer  36317  eleq2w2ALT  37048  modelaxreplem1  44995  elsetrecslem  49218
  Copyright terms: Public domain W3C validator