Theorem cbvalvw 2070

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209  ∀wal 1567

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812

This theorem is used by:  cbvexvw  2071  cbvaldvaw  2072  cbval2vw  2074  alcomimw  2077  hba1w  2083  sbjust  2099  ax12wdemo  2173  mo4  2594  cbvmovw  2630  nfcjust  2911  cbvralvw  3243  sbralie  3341  sbralieOLD  3343  zfpow  5331  tfisi  7877  findcard  9190  pssnn  9195  ssfi  9199  findcard3  9285  zfinf  9650  ttrclss  9731  ttrclselem2  9737  aceq0  10207  kmlem1  10239  kmlem13  10251  fin23lem32  10432  fin23lem41  10440  zfac  10548  zfcndpow  10711  zfcndinf  10713  zfcndac  10714  axgroth4  10927  relexpindlem  15228  ramcl  17219  mreexexlemd  17830  bnj1112  35666  axprALT2  35795  axpowg  35885  srepdf  36041  dfon2lem6  36677  dfon2lem7  36678  dfon2  36681  cbvralvw2  37142  axtcond  37393  wl-dfcleq  38577  phpreu  38667  axc11n-16  40135  nfa1w  43826  eu6w  43827  abbibw  43828  dfac11  44204  ismnushort  45425  modelaxrep  46110  cbvals  51115