Theorem cbvalvw 2069

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209  ∀wal 1568

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813

This theorem is used by:  cbvexvw  2070  cbvaldvaw  2071  cbval2vw  2073  alcomimw  2076  hba1w  2082  sbjust  2098  ax12wdemo  2173  mo4  2596  cbvmovw  2632  nfcjust  2913  cbvralvw  3245  sbralie  3344  sbralieOLD  3346  zfpow  5339  tfisi  7861  findcard  9155  pssnn  9160  ssfi  9164  findcard3  9250  zfinf  9615  ttrclss  9696  ttrclselem2  9702  aceq0  10118  kmlem1  10150  kmlem13  10162  fin23lem32  10343  fin23lem41  10351  zfac  10459  zfcndpow  10618  zfcndinf  10620  zfcndac  10621  axgroth4  10834  relexpindlem  15126  ramcl  17113  mreexexlemd  17724  bnj1112  35438  axprALT2  35563  axpowg  35618  dfon2lem6  36317  dfon2lem7  36318  dfon2  36321  cbvralvw2  36797  axtcond  37048  wl-dfcleq  38219  phpreu  38314  axc11n-16  39772  nfa1w  43467  eu6w  43468  abbibw  43469  dfac11  43849  ismnushort  45071  modelaxrep  45750  cbvals  50642