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

Theorem cbvalvw 2143
Description: Change bound variable. Uses only Tarski's FOL axiom schemes. See cbvalv 2425 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 2009 . 2 (∀𝑥𝜑 → ∀𝑦𝑥𝜑)
2 ax-5 2009 . 2 𝜓 → ∀𝑥 ¬ 𝜓)
3 ax-5 2009 . 2 (∀𝑦𝜓 → ∀𝑥𝑦𝜓)
4 ax-5 2009 . 2 𝜑 → ∀𝑦 ¬ 𝜑)
5 cbvalvw.1 . 2 (𝑥 = 𝑦 → (𝜑𝜓))
61, 2, 3, 4, 5cbvalw 2142 1 (∀𝑥𝜑 ↔ ∀𝑦𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 198  wal 1654
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112
This theorem depends on definitions:  df-bi 199  df-an 387  df-ex 1879
This theorem is referenced by:  cbvexvw  2144  hba1w  2149  ax12wdemo  2186  nfcjust  2957  zfpow  5068  tfisi  7324  pssnn  8453  findcard  8474  findcard3  8478  zfinf  8820  aceq0  9261  kmlem1  9294  kmlem13  9306  fin23lem32  9488  fin23lem41  9496  zfac  9604  zfcndpow  9760  zfcndinf  9762  zfcndac  9763  axgroth4  9976  relexpindlem  14187  ramcl  16111  mreexexlemd  16664  bnj1112  31593  dfon2lem6  32226  dfon2lem7  32227  dfon2  32230  bj-ssbjustlem  33153  phpreu  33931  axc11n-16  35008  cbvabvw  38041  dfac11  38470
  Copyright terms: Public domain W3C validator