Theorem cbvalvw 2035

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007

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

This theorem is referenced by:  cbvexvw  2036  cbvaldvaw  2037  cbval2vw  2039  alcomimw  2042  hba1w  2047  sbjust  2063  ax12wdemo  2135  mo4  2569  cbvmovw  2605  nfcjust  2894  cbvralvw  3243  cbvraldva2  3356  sbralie  3366  zfpow  5384  tfisi  7896  findcard  9229  pssnn  9234  ssfi  9240  findcard3  9346  findcard3OLD  9347  zfinf  9708  ttrclss  9789  ttrclselem2  9795  aceq0  10187  kmlem1  10220  kmlem13  10232  fin23lem32  10413  fin23lem41  10421  zfac  10529  zfcndpow  10685  zfcndinf  10687  zfcndac  10688  axgroth4  10901  relexpindlem  15112  ramcl  17076  mreexexlemd  17702  bnj1112  34959  dfon2lem6  35752  dfon2lem7  35753  dfon2  35756  cbvralvw2  36192  phpreu  37564  axc11n-16  38894  nfa1w  42630  eu6w  42631  abbibw  42632  dfac11  43019  ismnushort  44270