Theorem cbvalvw 2037

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 1911	. 2 ⊢ (∀𝑥𝜑 → ∀𝑦∀𝑥𝜑)
2		ax-5 1911	. 2 ⊢ (¬ 𝜓 → ∀𝑥 ¬ 𝜓)
3		ax-5 1911	. 2 ⊢ (∀𝑦𝜓 → ∀𝑥∀𝑦𝜓)
4		ax-5 1911	. 2 ⊢ (¬ 𝜑 → ∀𝑦 ¬ 𝜑)
5		cbvalvw.1	. 2 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
6	1, 2, 3, 4, 5	cbvalw 2036	1 ⊢ (∀𝑥𝜑 ↔ ∀𝑦𝜓)

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009

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

This theorem is referenced by:  cbvexvw  2038  cbvaldvaw  2039  cbval2vw  2041  alcomimw  2044  hba1w  2050  sbjust  2066  ax12wdemo  2140  mo4  2566  cbvmovw  2602  nfcjust  2884  cbvralvw  3214  cbvraldva2  3318  sbralie  3322  sbralieOLD  3324  zfpow  5311  tfisi  7801  findcard  9088  pssnn  9093  ssfi  9097  findcard3  9183  zfinf  9548  ttrclss  9629  ttrclselem2  9635  aceq0  10028  kmlem1  10061  kmlem13  10073  fin23lem32  10254  fin23lem41  10262  zfac  10370  zfcndpow  10527  zfcndinf  10529  zfcndac  10530  axgroth4  10743  relexpindlem  14986  ramcl  16957  mreexexlemd  17567  bnj1112  35139  dfon2lem6  35980  dfon2lem7  35981  dfon2  35984  cbvralvw2  36420  phpreu  37805  axc11n-16  39198  nfa1w  42918  eu6w  42919  abbibw  42920  dfac11  43304  ismnushort  44542  modelaxrep  45222