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

Theorem cbvalvw 2032
Description: Change bound variable. Uses only Tarski's FOL axiom schemes. See cbvalv 2395 for a version with fewer disjoint variable conditions but requiring more axioms. (Contributed by NM, 9-Apr-2017.) (Proof shortened by Wolf Lammen, 28-Feb-2018.)
Hypothesis
Ref Expression
cbvalvw.1 (𝑥 = 𝑦 → (𝜑𝜓))
Assertion
Ref Expression
cbvalvw (∀𝑥𝜑 ↔ ∀𝑦𝜓)
Distinct variable groups:   𝑥,𝑦   𝜓,𝑥   𝜑,𝑦
Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑦)

Proof of Theorem cbvalvw
StepHypRef Expression
1 ax-5 1906 . 2 (∀𝑥𝜑 → ∀𝑦𝑥𝜑)
2 ax-5 1906 . 2 𝜓 → ∀𝑥 ¬ 𝜓)
3 ax-5 1906 . 2 (∀𝑦𝜓 → ∀𝑥𝑦𝜓)
4 ax-5 1906 . 2 𝜑 → ∀𝑦 ¬ 𝜑)
5 cbvalvw.1 . 2 (𝑥 = 𝑦 → (𝜑𝜓))
61, 2, 3, 4, 5cbvalw 2031 1 (∀𝑥𝜑 ↔ ∀𝑦𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wal 1532
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004
This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1775
This theorem is referenced by:  cbvexvw  2033  cbvaldvaw  2034  cbval2vw  2036  alcomiw  2039  hba1w  2043  sbjust  2059  ax12wdemo  2124  mo4  2556  cbvmovw  2592  nfcjust  2880  cbvralvw  3230  cbvraldva2  3340  sbralie  3350  zfpow  5360  tfisi  7857  findcard  9181  pssnn  9186  ssfi  9191  pssnnOLD  9283  findcard3  9303  findcard3OLD  9304  zfinf  9656  ttrclss  9737  ttrclselem2  9743  aceq0  10135  kmlem1  10167  kmlem13  10179  fin23lem32  10361  fin23lem41  10369  zfac  10477  zfcndpow  10633  zfcndinf  10635  zfcndac  10636  axgroth4  10849  relexpindlem  15036  ramcl  16991  mreexexlemd  17617  bnj1112  34608  dfon2lem6  35378  dfon2lem7  35379  dfon2  35382  phpreu  37071  axc11n-16  38404  dfac11  42480  ismnushort  43732
  Copyright terms: Public domain W3C validator