Theorem cbvalvw 2032

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004

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

This theorem is referenced by:  cbvexvw  2033  cbvaldvaw  2034  cbval2vw  2036  alcomimw  2039  hba1w  2044  sbjust  2060  ax12wdemo  2132  mo4  2563  cbvmovw  2599  nfcjust  2888  cbvralvw  3234  cbvraldva2  3345  sbralie  3355  zfpow  5371  tfisi  7879  findcard  9201  pssnn  9206  ssfi  9211  findcard3  9315  findcard3OLD  9316  zfinf  9676  ttrclss  9757  ttrclselem2  9763  aceq0  10155  kmlem1  10188  kmlem13  10200  fin23lem32  10381  fin23lem41  10389  zfac  10497  zfcndpow  10653  zfcndinf  10655  zfcndac  10656  axgroth4  10869  relexpindlem  15098  ramcl  17062  mreexexlemd  17688  bnj1112  34975  dfon2lem6  35769  dfon2lem7  35770  dfon2  35773  cbvralvw2  36208  phpreu  37590  axc11n-16  38919  nfa1w  42661  eu6w  42662  abbibw  42663  dfac11  43050  ismnushort  44296  modelaxrep  44945