Theorem cbvalvw 2037

Description: Change bound variable. Uses only Tarski's FOL axiom schemes. See cbvalv 2400 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  2138  mo4  2561  cbvmovw  2597  nfcjust  2880  cbvralvw  3210  cbvraldva2  3314  sbralie  3318  sbralieOLD  3320  zfpow  5302  tfisi  7789  findcard  9073  pssnn  9078  ssfi  9082  findcard3  9167  zfinf  9529  ttrclss  9610  ttrclselem2  9616  aceq0  10009  kmlem1  10042  kmlem13  10054  fin23lem32  10235  fin23lem41  10243  zfac  10351  zfcndpow  10507  zfcndinf  10509  zfcndac  10510  axgroth4  10723  relexpindlem  14970  ramcl  16941  mreexexlemd  17550  bnj1112  34995  dfon2lem6  35830  dfon2lem7  35831  dfon2  35834  cbvralvw2  36270  phpreu  37654  axc11n-16  39047  nfa1w  42778  eu6w  42779  abbibw  42780  dfac11  43165  ismnushort  44404  modelaxrep  45084