Theorem cbvalvw 2037

Description: Change bound variable. Uses only Tarski's FOL axiom schemes. See cbvalv 2402 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 1911	. 2 ⊢ (∀𝑥𝜑 → ∀𝑦∀𝑥𝜑)
2		ax-5 1911	. 2 ⊢ (¬ 𝜓 → ∀𝑥 ¬ 𝜓)
3		ax-5 1911	. 2 ⊢ (∀𝑦𝜓 → ∀𝑥∀𝑦𝜓)
4		ax-5 1911	. 2 ⊢ (¬ 𝜑 → ∀𝑦 ¬ 𝜑)
5		cbvalvw.1	. 2 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
6	1, 2, 3, 4, 5	cbvalw 2036	1 ⊢ (∀𝑥𝜑 ↔ ∀𝑦𝜓)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206  ∀wal 1539

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781

This theorem is referenced by:  cbvexvw  2038  cbvaldvaw  2039  cbval2vw  2041  alcomimw  2044  hba1w  2050  sbjust  2066  ax12wdemo  2140  mo4  2564  cbvmovw  2600  nfcjust  2882  cbvralvw  3212  cbvraldva2  3316  sbralie  3320  sbralieOLD  3322  zfpow  5309  tfisi  7799  findcard  9086  pssnn  9091  ssfi  9095  findcard3  9181  zfinf  9546  ttrclss  9627  ttrclselem2  9633  aceq0  10026  kmlem1  10059  kmlem13  10071  fin23lem32  10252  fin23lem41  10260  zfac  10368  zfcndpow  10525  zfcndinf  10527  zfcndac  10528  axgroth4  10741  relexpindlem  14984  ramcl  16955  mreexexlemd  17565  bnj1112  35088  dfon2lem6  35929  dfon2lem7  35930  dfon2  35933  cbvralvw2  36369  phpreu  37744  axc11n-16  39137  nfa1w  42860  eu6w  42861  abbibw  42862  dfac11  43246  ismnushort  44484  modelaxrep  45164