Theorem cbvalvw 2038

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

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

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 1912  ax-6 1969  ax-7 2010

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782

This theorem is referenced by:  cbvexvw  2039  cbvaldvaw  2040  cbval2vw  2042  alcomimw  2045  hba1w  2051  sbjust  2067  ax12wdemo  2141  mo4  2566  cbvmovw  2602  nfcjust  2884  cbvralvw  3215  sbralie  3315  sbralieOLD  3317  zfpow  5308  tfisi  7810  findcard  9098  pssnn  9103  ssfi  9107  findcard3  9193  zfinf  9560  ttrclss  9641  ttrclselem2  9647  aceq0  10040  kmlem1  10073  kmlem13  10085  fin23lem32  10266  fin23lem41  10274  zfac  10382  zfcndpow  10539  zfcndinf  10541  zfcndac  10542  axgroth4  10755  relexpindlem  15025  ramcl  17000  mreexexlemd  17610  bnj1112  35125  axprALT2  35253  dfon2lem6  35968  dfon2lem7  35969  dfon2  35972  cbvralvw2  36408  axtcond  36660  wl-dfcleq  37830  phpreu  37925  axc11n-16  39384  nfa1w  43108  eu6w  43109  abbibw  43110  dfac11  43490  ismnushort  44728  modelaxrep  45408