Theorem cbvalvw 2042

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1786

This theorem is referenced by:  cbvexvw  2043  cbvaldvaw  2044  cbval2vw  2046  alcomiw  2049  hba1w  2053  sbjust  2069  ax12wdemo  2134  mo4  2567  cbvmovw  2603  nfcjust  2889  cbvralvw  3380  cbvraldva2  3389  zfpow  5292  tfisi  7693  findcard  8911  pssnn  8916  ssfi  8921  pssnnOLD  9001  findcard3  9018  zfinf  9358  ttrclss  9439  ttrclselem2  9445  aceq0  9858  kmlem1  9890  kmlem13  9902  fin23lem32  10084  fin23lem41  10092  zfac  10200  zfcndpow  10356  zfcndinf  10358  zfcndac  10359  axgroth4  10572  relexpindlem  14755  ramcl  16711  mreexexlemd  17334  bnj1112  32942  dfon2lem6  33743  dfon2lem7  33744  dfon2  33747  phpreu  35740  axc11n-16  36931  dfac11  40867  ismnushort  41872