Theorem cbvalvw 2039

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205  ∀wal 1539

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782

This theorem is referenced by:  cbvexvw  2040  cbvaldvaw  2041  cbval2vw  2043  alcomiw  2046  hba1w  2050  sbjust  2066  ax12wdemo  2131  mo4  2560  cbvmovw  2596  nfcjust  2884  cbvralvw  3234  cbvraldva2  3344  sbralie  3354  zfpow  5363  tfisi  7844  findcard  9159  pssnn  9164  ssfi  9169  pssnnOLD  9261  findcard3  9281  findcard3OLD  9282  zfinf  9630  ttrclss  9711  ttrclselem2  9717  aceq0  10109  kmlem1  10141  kmlem13  10153  fin23lem32  10335  fin23lem41  10343  zfac  10451  zfcndpow  10607  zfcndinf  10609  zfcndac  10610  axgroth4  10823  relexpindlem  15006  ramcl  16958  mreexexlemd  17584  bnj1112  33982  dfon2lem6  34748  dfon2lem7  34749  dfon2  34752  phpreu  36460  axc11n-16  37796  dfac11  41789  ismnushort  43045