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  3215  cbvraldva2  3321  sbralie  3326  sbralieOLD  3328  zfpow  5321  tfisi  7835  findcard  9127  pssnn  9132  ssfi  9137  findcard3  9229  findcard3OLD  9230  zfinf  9592  ttrclss  9673  ttrclselem2  9679  aceq0  10071  kmlem1  10104  kmlem13  10116  fin23lem32  10297  fin23lem41  10305  zfac  10413  zfcndpow  10569  zfcndinf  10571  zfcndac  10572  axgroth4  10785  relexpindlem  15029  ramcl  17000  mreexexlemd  17605  bnj1112  34973  dfon2lem6  35776  dfon2lem7  35777  dfon2  35780  cbvralvw2  36214  phpreu  37598  axc11n-16  38931  nfa1w  42663  eu6w  42664  abbibw  42665  dfac11  43051  ismnushort  44290  modelaxrep  44971