Theorem cbvalvw 2036

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206  ∀wal 1538

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780

This theorem is referenced by:  cbvexvw  2037  cbvaldvaw  2038  cbval2vw  2040  alcomimw  2043  hba1w  2048  sbjust  2064  ax12wdemo  2136  mo4  2559  cbvmovw  2595  nfcjust  2877  cbvralvw  3213  cbvraldva2  3318  sbralie  3323  sbralieOLD  3325  zfpow  5316  tfisi  7815  findcard  9104  pssnn  9109  ssfi  9114  findcard3  9205  findcard3OLD  9206  zfinf  9568  ttrclss  9649  ttrclselem2  9655  aceq0  10047  kmlem1  10080  kmlem13  10092  fin23lem32  10273  fin23lem41  10281  zfac  10389  zfcndpow  10545  zfcndinf  10547  zfcndac  10548  axgroth4  10761  relexpindlem  15005  ramcl  16976  mreexexlemd  17581  bnj1112  34946  dfon2lem6  35749  dfon2lem7  35750  dfon2  35753  cbvralvw2  36187  phpreu  37571  axc11n-16  38904  nfa1w  42636  eu6w  42637  abbibw  42638  dfac11  43024  ismnushort  44263  modelaxrep  44944