Theorem cbvalvw 2032

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004

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

This theorem is referenced by:  cbvexvw  2033  cbvaldvaw  2034  cbval2vw  2036  alcomiw  2039  hba1w  2043  sbjust  2059  ax12wdemo  2124  mo4  2556  cbvmovw  2592  nfcjust  2880  cbvralvw  3230  cbvraldva2  3340  sbralie  3350  zfpow  5360  tfisi  7857  findcard  9181  pssnn  9186  ssfi  9191  pssnnOLD  9283  findcard3  9303  findcard3OLD  9304  zfinf  9656  ttrclss  9737  ttrclselem2  9743  aceq0  10135  kmlem1  10167  kmlem13  10179  fin23lem32  10361  fin23lem41  10369  zfac  10477  zfcndpow  10633  zfcndinf  10635  zfcndac  10636  axgroth4  10849  relexpindlem  15036  ramcl  16991  mreexexlemd  17617  bnj1112  34608  dfon2lem6  35378  dfon2lem7  35379  dfon2  35382  phpreu  37071  axc11n-16  38404  dfac11  42480  ismnushort  43732