Theorem cbvalvw 2035

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007

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

This theorem is referenced by:  cbvexvw  2036  cbvaldvaw  2037  cbval2vw  2039  alcomimw  2042  hba1w  2047  sbjust  2063  ax12wdemo  2135  mo4  2565  cbvmovw  2601  nfcjust  2884  cbvralvw  3220  cbvraldva2  3327  sbralie  3337  zfpow  5336  tfisi  7854  findcard  9177  pssnn  9182  ssfi  9187  findcard3  9290  findcard3OLD  9291  zfinf  9653  ttrclss  9734  ttrclselem2  9740  aceq0  10132  kmlem1  10165  kmlem13  10177  fin23lem32  10358  fin23lem41  10366  zfac  10474  zfcndpow  10630  zfcndinf  10632  zfcndac  10633  axgroth4  10846  relexpindlem  15082  ramcl  17049  mreexexlemd  17656  bnj1112  35014  dfon2lem6  35806  dfon2lem7  35807  dfon2  35810  cbvralvw2  36244  phpreu  37628  axc11n-16  38956  nfa1w  42698  eu6w  42699  abbibw  42700  dfac11  43086  ismnushort  44325  modelaxrep  45006