Theorem cbvalvw 2056

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208  ∀wal 1558

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1800

This theorem is referenced by:  cbvexvw  2057  cbvaldvaw  2058  cbval2vw  2060  alcomimw  2063  hba1w  2069  rename-sb  2089  ax12wdemo  2169  mo4  2593  cbvmovw  2629  nfcjust  2910  cbvralvw  3240  sbralie  3340  sbralieOLD  3342  zfpow  5323  tfisi  7839  findcard  9132  pssnn  9137  ssfi  9141  findcard3  9227  zfinf  9594  ttrclss  9675  ttrclselem2  9681  aceq0  10074  kmlem1  10107  kmlem13  10119  fin23lem32  10301  fin23lem41  10309  zfac  10417  zfcndpow  10574  zfcndinf  10576  zfcndac  10577  axgroth4  10790  relexpindlem  15076  ramcl  17065  mreexexlemd  17676  bnj1112  35278  axprALT2  35405  axpowg  35442  dfon2lem6  36136  dfon2lem7  36137  dfon2  36140  cbvralvw2  36586  axtcond  36838  wl-dfcleq  38008  phpreu  38103  axc11n-16  39562  nfa1w  43257  eu6w  43258  abbibw  43259  dfac11  43639  ismnushort  44877  modelaxrep  45557