Theorem cbvalvw 2043

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 207  ∀wal 1545

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787

This theorem is referenced by:  cbvexvw  2044  cbvaldvaw  2045  cbval2vw  2047  alcomimw  2050  hba1w  2056  sbjust  2072  ax12wdemo  2146  mo4  2570  cbvmovw  2606  nfcjust  2887  cbvralvw  3217  sbralie  3317  sbralieOLD  3319  zfpow  5295  tfisi  7799  findcard  9088  pssnn  9093  ssfi  9097  findcard3  9183  zfinf  9551  ttrclss  9632  ttrclselem2  9638  aceq0  10031  kmlem1  10064  kmlem13  10076  fin23lem32  10257  fin23lem41  10265  zfac  10373  zfcndpow  10530  zfcndinf  10532  zfcndac  10533  axgroth4  10746  relexpindlem  15016  ramcl  16991  mreexexlemd  17601  bnj1112  35165  axprALT2  35290  axpowg  35327  dfon2lem6  36014  dfon2lem7  36015  dfon2  36018  cbvralvw2  36454  axtcond  36706  wl-dfcleq  37876  phpreu  37971  axc11n-16  39430  nfa1w  43125  eu6w  43126  abbibw  43127  dfac11  43507  ismnushort  44745  modelaxrep  45425