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  17585  bnj1112  34966  dfon2lem6  35769  dfon2lem7  35770  dfon2  35773  cbvralvw2  36207  phpreu  37591  axc11n-16  38924  nfa1w  42656  eu6w  42657  abbibw  42658  dfac11  43044  ismnushort  44283  modelaxrep  44964