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

Theorem cbvalvw 2039
 Description: Change bound variable. Uses only Tarski's FOL axiom schemes. See cbvalv 2414 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 1907 . 2 (∀𝑥𝜑 → ∀𝑦𝑥𝜑)
2 ax-5 1907 . 2 𝜓 → ∀𝑥 ¬ 𝜓)
3 ax-5 1907 . 2 (∀𝑦𝜓 → ∀𝑥𝑦𝜓)
4 ax-5 1907 . 2 𝜑 → ∀𝑦 ¬ 𝜑)
5 cbvalvw.1 . 2 (𝑥 = 𝑦 → (𝜑𝜓))
61, 2, 3, 4, 5cbvalw 2038 1 (∀𝑥𝜑 ↔ ∀𝑦𝜓)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208  ∀wal 1531 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011 This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1777 This theorem is referenced by:  cbvexvw  2040  cbvaldvaw  2041  cbval2vw  2043  alcomiw  2046  hba1w  2050  sbjust  2064  ax12wdemo  2135  mo4  2646  nfcjust  2962  cbvralvw  3449  cbvraldva2  3456  cbvrexdva2OLD  3458  zfpow  5266  tfisi  7572  pssnn  8735  findcard  8756  findcard3  8760  zfinf  9101  aceq0  9543  kmlem1  9575  kmlem13  9587  fin23lem32  9765  fin23lem41  9773  zfac  9881  zfcndpow  10037  zfcndinf  10039  zfcndac  10040  axgroth4  10253  relexpindlem  14421  ramcl  16364  mreexexlemd  16914  bnj1112  32255  dfon2lem6  33033  dfon2lem7  33034  dfon2  33037  phpreu  34875  axc11n-16  36073  dfac11  39662
 Copyright terms: Public domain W3C validator