Theorem cbvalvw 2039

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1777

This theorem is referenced by:  cbvexvw  2040  cbvaldvaw  2041  cbval2vw  2043  alcomiw  2046  hba1w  2050  sbjust  2064  ax12wdemo  2135  mo4  2646  nfcjust  2962  cbvralvw  3449  cbvraldva2  3456  cbvrexdva2OLD  3458  zfpow  5259  tfisi  7567  pssnn  8730  findcard  8751  findcard3  8755  zfinf  9096  aceq0  9538  kmlem1  9570  kmlem13  9582  fin23lem32  9760  fin23lem41  9768  zfac  9876  zfcndpow  10032  zfcndinf  10034  zfcndac  10035  axgroth4  10248  relexpindlem  14416  ramcl  16359  mreexexlemd  16909  bnj1112  32250  dfon2lem6  33028  dfon2lem7  33029  dfon2  33032  phpreu  34870  axc11n-16  36068  dfac11  39655