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  cbvraldva2  3320  sbralie  3324  sbralieOLD  3326  zfpow  5313  tfisi  7811  findcard  9100  pssnn  9105  ssfi  9109  findcard3  9195  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  14998  ramcl  16969  mreexexlemd  17579  bnj1112  35159  axprALT2  35287  dfon2lem6  36002  dfon2lem7  36003  dfon2  36006  cbvralvw2  36442  phpreu  37855  axc11n-16  39314  nfa1w  43033  eu6w  43034  abbibw  43035  dfac11  43419  ismnushort  44657  modelaxrep  45337