Theorem cbvalvw 2043

Description: Change bound variable. Uses only Tarski's FOL axiom schemes. See cbvalv 2407 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 2042	1 ⊢ (∀𝑥𝜑 ↔ ∀𝑦𝜓)

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015

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

This theorem is referenced by:  cbvexvw  2044  cbvaldvaw  2045  cbval2vw  2047  alcomiw  2050  hba1w  2054  sbjust  2068  ax12wdemo  2136  mo4  2625  nfcjust  2937  cbvralvw  3396  cbvraldva2  3403  cbvrexdva2OLD  3405  zfpow  5232  tfisi  7553  pssnn  8720  findcard  8741  findcard3  8745  zfinf  9086  aceq0  9529  kmlem1  9561  kmlem13  9573  fin23lem32  9755  fin23lem41  9763  zfac  9871  zfcndpow  10027  zfcndinf  10029  zfcndac  10030  axgroth4  10243  relexpindlem  14414  ramcl  16355  mreexexlemd  16907  bnj1112  32365  dfon2lem6  33146  dfon2lem7  33147  dfon2  33150  phpreu  35041  axc11n-16  36234  dfac11  40006