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

Theorem cbvalvw 2034
Description: Change bound variable. Uses only Tarski's FOL axiom schemes. See cbvalv 2409 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 1902 . 2 (∀𝑥𝜑 → ∀𝑦𝑥𝜑)
2 ax-5 1902 . 2 𝜓 → ∀𝑥 ¬ 𝜓)
3 ax-5 1902 . 2 (∀𝑦𝜓 → ∀𝑥𝑦𝜓)
4 ax-5 1902 . 2 𝜑 → ∀𝑦 ¬ 𝜑)
5 cbvalvw.1 . 2 (𝑥 = 𝑦 → (𝜑𝜓))
61, 2, 3, 4, 5cbvalw 2033 1 (∀𝑥𝜑 ↔ ∀𝑦𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207  wal 1526
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772
This theorem is referenced by:  cbvexvw  2035  cbvaldvaw  2036  cbval2vw  2038  alcomiw  2041  hba1w  2045  sbjust  2059  ax12wdemo  2130  mo4  2643  nfcjust  2959  cbvralvw  3447  cbvraldva2  3454  cbvrexdva2OLD  3456  zfpow  5258  tfisi  7562  pssnn  8724  findcard  8745  findcard3  8749  zfinf  9090  aceq0  9532  kmlem1  9564  kmlem13  9576  fin23lem32  9754  fin23lem41  9762  zfac  9870  zfcndpow  10026  zfcndinf  10028  zfcndac  10029  axgroth4  10242  relexpindlem  14410  ramcl  16353  mreexexlemd  16903  bnj1112  32152  dfon2lem6  32930  dfon2lem7  32931  dfon2  32934  phpreu  34757  axc11n-16  35954  dfac11  39540
  Copyright terms: Public domain W3C validator