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

Theorem cbvalvw 2037
Description: Change bound variable. Uses only Tarski's FOL axiom schemes. See cbvalv 2398 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 1911 . 2 (∀𝑥𝜑 → ∀𝑦𝑥𝜑)
2 ax-5 1911 . 2 𝜓 → ∀𝑥 ¬ 𝜓)
3 ax-5 1911 . 2 (∀𝑦𝜓 → ∀𝑥𝑦𝜓)
4 ax-5 1911 . 2 𝜑 → ∀𝑦 ¬ 𝜑)
5 cbvalvw.1 . 2 (𝑥 = 𝑦 → (𝜑𝜓))
61, 2, 3, 4, 5cbvalw 2036 1 (∀𝑥𝜑 ↔ ∀𝑦𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wal 1537
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009
This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1780
This theorem is referenced by:  cbvexvw  2038  cbvaldvaw  2039  cbval2vw  2041  alcomiw  2044  hba1w  2048  sbjust  2064  ax12wdemo  2129  mo4  2564  cbvmovw  2600  nfcjust  2886  cbvralvw  3222  cbvraldva2  3404  zfpow  5298  tfisi  7737  findcard  8984  pssnn  8989  ssfi  8994  pssnnOLD  9086  findcard3  9105  zfinf  9445  ttrclss  9526  ttrclselem2  9532  aceq0  9924  kmlem1  9956  kmlem13  9968  fin23lem32  10150  fin23lem41  10158  zfac  10266  zfcndpow  10422  zfcndinf  10424  zfcndac  10425  axgroth4  10638  relexpindlem  14823  ramcl  16779  mreexexlemd  17402  bnj1112  33012  dfon2lem6  33813  dfon2lem7  33814  dfon2  33817  phpreu  35809  axc11n-16  37152  dfac11  41083  ismnushort  42132
  Copyright terms: Public domain W3C validator