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

Theorem cbvalvw 2125
 Description: Change bound variable. Uses only Tarski's FOL axiom schemes. See cbvalv 2434 for a version with fewer DV 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 1991 . 2 (∀𝑥𝜑 → ∀𝑦𝑥𝜑)
2 ax-5 1991 . 2 𝜓 → ∀𝑥 ¬ 𝜓)
3 ax-5 1991 . 2 (∀𝑦𝜓 → ∀𝑥𝑦𝜓)
4 ax-5 1991 . 2 𝜑 → ∀𝑦 ¬ 𝜑)
5 cbvalvw.1 . 2 (𝑥 = 𝑦 → (𝜑𝜓))
61, 2, 3, 4, 5cbvalw 2124 1 (∀𝑥𝜑 ↔ ∀𝑦𝜓)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196  ∀wal 1629 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093 This theorem depends on definitions:  df-bi 197  df-an 383  df-ex 1853 This theorem is referenced by:  cbvexvw  2126  hba1w  2131  hba1wOLD  2132  ax12wdemo  2167  nfcjust  2901  zfpow  4975  tfisi  7205  pssnn  8334  findcard  8355  findcard3  8359  zfinf  8700  aceq0  9141  kmlem1  9174  kmlem13  9186  fin23lem32  9368  fin23lem41  9376  zfac  9484  zfcndpow  9640  zfcndinf  9642  zfcndac  9643  axgroth4  9856  relexpindlem  14011  ramcl  15940  mreexexlemd  16512  bnj1112  31389  dfon2lem6  32029  dfon2lem7  32030  dfon2  32033  bj-ssbjust  32956  phpreu  33726  axc11n-16  34746  dfac11  38158
 Copyright terms: Public domain W3C validator