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  3775  nalset  5312  dfpo2  6292  isowe2  7343  tfisi  7844  findcard2  9160  findcard2OLD  9280  marypha1lem  9424  setind  9725  karden  9886  kmlem4  10144  axgroth3  10822  ramcl  16958  alexsubALTlem3  23544  i1fd  25189  dfon2lem6  34748  trer  35189  bj-ru0  35811  eleq2w2ALT  35916  elsetrecslem  47697
  Copyright terms: Public domain W3C validator