Theorem cbvalvw 2143

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 198  ∀wal 1654

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112

This theorem depends on definitions:  df-bi 199  df-an 387  df-ex 1879

This theorem is referenced by:  cbvexvw  2144  hba1w  2149  ax12wdemo  2186  nfcjust  2957  zfpow  5068  tfisi  7324  pssnn  8453  findcard  8474  findcard3  8478  zfinf  8820  aceq0  9261  kmlem1  9294  kmlem13  9306  fin23lem32  9488  fin23lem41  9496  zfac  9604  zfcndpow  9760  zfcndinf  9762  zfcndac  9763  axgroth4  9976  relexpindlem  14187  ramcl  16111  mreexexlemd  16664  bnj1112  31593  dfon2lem6  32226  dfon2lem7  32227  dfon2  32230  bj-ssbjustlem  33153  phpreu  33931  axc11n-16  35008  cbvabvw  38041  dfac11  38470