Theorem cbvalvw 2071

Description: Change bound variable. Uses only Tarski's FOL axiom schemes. See cbvalv 2432 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

Step	Hyp	Ref	Expression
1		ax-5 1945	. 2 ⊢ (∀𝑥𝜑 → ∀𝑦∀𝑥𝜑)
2		ax-5 1945	. 2 ⊢ (¬ 𝜓 → ∀𝑥 ¬ 𝜓)
3		ax-5 1945	. 2 ⊢ (∀𝑦𝜓 → ∀𝑥∀𝑦𝜓)
4		ax-5 1945	. 2 ⊢ (¬ 𝜑 → ∀𝑦 ¬ 𝜑)
5		cbvalvw.1	. 2 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
6	1, 2, 3, 4, 5	cbvalw 2070	1 ⊢ (∀𝑥𝜑 ↔ ∀𝑦𝜓)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209  ∀wal 1568

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813

This theorem is used by:  cbvexvw  2072  cbvaldvaw  2073  cbval2vw  2075  alcomimw  2078  hba1w  2084  sbjust  2100  ax12wdemo  2174  mo4  2594  cbvmovw  2630  nfcjust  2912  cbvralvw  3244  sbralie  3342  sbralieOLD  3344  zfpow  5335  tfisi  7904  findcard  9217  pssnn  9222  ssfi  9226  findcard3  9312  zfinf  9677  ttrclss  9758  ttrclselem2  9764  aceq0  10236  kmlem1  10268  kmlem13  10280  fin23lem32  10461  fin23lem41  10469  zfac  10577  zfcndpow  10740  zfcndinf  10742  zfcndac  10743  axgroth4  10956  relexpindlem  15259  ramcl  17251  mreexexlemd  17868  bnj1112  35724  axprALT2  35857  axpowg  35955  srepdf  36128  dfon2lem6  36765  dfon2lem7  36766  dfon2  36769  cbvralvw2  37230  axtcond  37481  wl-dfcleq  38705  phpreu  38795  axc11n-16  40261  nfa1w  43952  eu6w  43953  abbibw  43954  dfac11  44330  ismnushort  45546  modelaxrep  46235  cbvals  51329