Theorem cbvalvw 2038

Description: Change bound variable. Uses only Tarski's FOL axiom schemes. See cbvalv 2405 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  2567  cbvmovw  2603  nfcjust  2885  cbvralvw  3216  sbralie  3316  sbralieOLD  3318  zfpow  5304  tfisi  7804  findcard  9092  pssnn  9097  ssfi  9101  findcard3  9187  zfinf  9554  ttrclss  9635  ttrclselem2  9641  aceq0  10034  kmlem1  10067  kmlem13  10079  fin23lem32  10260  fin23lem41  10268  zfac  10376  zfcndpow  10533  zfcndinf  10535  zfcndac  10536  axgroth4  10749  relexpindlem  15019  ramcl  16994  mreexexlemd  17604  bnj1112  35144  axprALT2  35272  dfon2lem6  35987  dfon2lem7  35988  dfon2  35991  cbvralvw2  36427  axtcond  36679  wl-dfcleq  37847  phpreu  37942  axc11n-16  39401  nfa1w  43125  eu6w  43126  abbibw  43127  dfac11  43511  ismnushort  44749  modelaxrep  45429