Theorem cbvalvw 2048

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1787

This theorem is referenced by:  cbvexvw  2049  cbvaldvaw  2050  cbval2vw  2052  alcomiw  2055  hba1w  2059  sbjust  2073  ax12wdemo  2139  mo4  2567  cbvmovw  2604  nfcjust  2881  cbvralvw  3350  cbvraldva2  3359  zfpow  5234  tfisi  7595  findcard  8765  pssnn  8770  ssfi  8775  pssnnOLD  8818  findcard3  8838  zfinf  9178  aceq0  9621  kmlem1  9653  kmlem13  9665  fin23lem32  9847  fin23lem41  9855  zfac  9963  zfcndpow  10119  zfcndinf  10121  zfcndac  10122  axgroth4  10335  relexpindlem  14515  ramcl  16468  mreexexlemd  17021  bnj1112  32537  dfon2lem6  33341  dfon2lem7  33342  dfon2  33345  phpreu  35407  axc11n-16  36598  dfac11  40482