Theorem cbvalvw 2040

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783

This theorem is referenced by:  cbvexvw  2041  cbvaldvaw  2042  cbval2vw  2044  alcomiw  2047  hba1w  2051  sbjust  2067  ax12wdemo  2132  mo4  2561  cbvmovw  2597  nfcjust  2885  cbvralvw  3235  cbvraldva2  3345  sbralie  3355  zfpow  5365  tfisi  7848  findcard  9163  pssnn  9168  ssfi  9173  pssnnOLD  9265  findcard3  9285  findcard3OLD  9286  zfinf  9634  ttrclss  9715  ttrclselem2  9721  aceq0  10113  kmlem1  10145  kmlem13  10157  fin23lem32  10339  fin23lem41  10347  zfac  10455  zfcndpow  10611  zfcndinf  10613  zfcndac  10614  axgroth4  10827  relexpindlem  15010  ramcl  16962  mreexexlemd  17588  bnj1112  34025  dfon2lem6  34791  dfon2lem7  34792  dfon2  34795  phpreu  36520  axc11n-16  37856  dfac11  41852  ismnushort  43108