Theorem cbvalvw 2066

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 1940	. 2 ⊢ (∀𝑥𝜑 → ∀𝑦∀𝑥𝜑)
2		ax-5 1940	. 2 ⊢ (¬ 𝜓 → ∀𝑥 ¬ 𝜓)
3		ax-5 1940	. 2 ⊢ (∀𝑦𝜓 → ∀𝑥∀𝑦𝜓)
4		ax-5 1940	. 2 ⊢ (¬ 𝜑 → ∀𝑦 ¬ 𝜑)
5		cbvalvw.1	. 2 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
6	1, 2, 3, 4, 5	cbvalw 2065	1 ⊢ (∀𝑥𝜑 ↔ ∀𝑦𝜓)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209  ∀wal 1568

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810

This theorem is referenced by:  cbvexvw  2067  cbvaldvaw  2068  cbval2vw  2070  alcomimw  2073  hba1w  2079  sbjust  2095  ax12wdemo  2170  mo4  2594  cbvmovw  2630  nfcjust  2911  cbvralvw  3243  sbralie  3342  sbralieOLD  3344  zfpow  5337  tfisi  7851  findcard  9144  pssnn  9149  ssfi  9153  findcard3  9239  zfinf  9604  ttrclss  9685  ttrclselem2  9691  aceq0  10098  kmlem1  10130  kmlem13  10142  fin23lem32  10323  fin23lem41  10331  zfac  10439  zfcndpow  10596  zfcndinf  10598  zfcndac  10599  axgroth4  10812  relexpindlem  15096  ramcl  17084  mreexexlemd  17695  bnj1112  35371  axprALT2  35503  axpowg  35559  dfon2lem6  36278  dfon2lem7  36279  dfon2  36282  cbvralvw2  36758  axtcond  37009  wl-dfcleq  38180  phpreu  38275  axc11n-16  39732  nfa1w  43427  eu6w  43428  abbibw  43429  dfac11  43809  ismnushort  45031  modelaxrep  45710  cbvals  50603