Theorem cbvalvw 2036

Description: Change bound variable. Uses only Tarski's FOL axiom schemes. See cbvalv 2398 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 2035	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 2008

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

This theorem is referenced by:  cbvexvw  2037  cbvaldvaw  2038  cbval2vw  2040  alcomimw  2043  hba1w  2048  sbjust  2064  ax12wdemo  2136  mo4  2559  cbvmovw  2595  nfcjust  2877  cbvralvw  3207  cbvraldva2  3311  sbralie  3315  sbralieOLD  3317  zfpow  5305  tfisi  7792  findcard  9077  pssnn  9082  ssfi  9087  findcard3  9172  zfinf  9535  ttrclss  9616  ttrclselem2  9622  aceq0  10012  kmlem1  10045  kmlem13  10057  fin23lem32  10238  fin23lem41  10246  zfac  10354  zfcndpow  10510  zfcndinf  10512  zfcndac  10513  axgroth4  10726  relexpindlem  14970  ramcl  16941  mreexexlemd  17550  bnj1112  34950  dfon2lem6  35766  dfon2lem7  35767  dfon2  35770  cbvralvw2  36204  phpreu  37588  axc11n-16  38921  nfa1w  42652  eu6w  42653  abbibw  42654  dfac11  43039  ismnushort  44278  modelaxrep  44959