Theorem cbvalvw 2069

Description: Change bound variable. Uses only Tarski's FOL axiom schemes. See cbvalv 2429 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  2172  mo4  2591  cbvmovw  2627  nfcjust  2908  cbvralvw  3240  sbralie  3338  sbralieOLD  3340  zfpow  5331  tfisi  7856  findcard  9161  pssnn  9166  ssfi  9170  findcard3  9256  zfinf  9621  ttrclss  9702  ttrclselem2  9708  aceq0  10124  kmlem1  10156  kmlem13  10168  fin23lem32  10349  fin23lem41  10357  zfac  10465  zfcndpow  10628  zfcndinf  10630  zfcndac  10631  axgroth4  10844  relexpindlem  15139  ramcl  17124  mreexexlemd  17735  bnj1112  35495  axprALT2  35620  axpowg  35675  dfon2lem6  36368  dfon2lem7  36369  dfon2  36372  cbvralvw2  36849  axtcond  37100  wl-dfcleq  38271  phpreu  38361  axc11n-16  39814  nfa1w  43524  eu6w  43525  abbibw  43526  dfac11  43906  ismnushort  45128  modelaxrep  45807  cbvals  50737