Theorem cbvalvw 2069

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209  ∀wal 1568

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813

This theorem is used by:  cbvexvw  2070  cbvaldvaw  2071  cbval2vw  2073  alcomimw  2076  hba1w  2082  sbjust  2098  ax12wdemo  2172  mo4  2592  cbvmovw  2628  nfcjust  2909  cbvralvw  3241  sbralie  3339  sbralieOLD  3341  zfpow  5328  tfisi  7870  findcard  9179  pssnn  9184  ssfi  9188  findcard3  9274  zfinf  9640  ttrclss  9721  ttrclselem2  9727  aceq0  10197  kmlem1  10229  kmlem13  10241  fin23lem32  10422  fin23lem41  10430  zfac  10538  zfcndpow  10701  zfcndinf  10703  zfcndac  10704  axgroth4  10917  relexpindlem  15216  ramcl  17207  mreexexlemd  17818  bnj1112  35613  axprALT2  35734  axpowg  35814  dfon2lem6  36550  dfon2lem7  36551  dfon2  36554  cbvralvw2  37015  axtcond  37266  wl-dfcleq  38437  phpreu  38527  axc11n-16  39995  nfa1w  43686  eu6w  43687  abbibw  43688  dfac11  44063  ismnushort  45284  modelaxrep  45970  cbvals  50900