Theorem cbvalvw 2063

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209  ∀wal 1565

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807

This theorem is referenced by:  cbvexvw  2064  cbvaldvaw  2065  cbval2vw  2067  alcomimw  2070  hba1w  2076  rename-sb  2096  ax12wdemo  2176  mo4  2600  cbvmovw  2636  nfcjust  2917  cbvralvw  3249  sbralie  3349  sbralieOLD  3351  zfpow  5338  tfisi  7855  findcard  9148  pssnn  9153  ssfi  9157  findcard3  9243  zfinf  9608  ttrclss  9689  ttrclselem2  9695  aceq0  10102  kmlem1  10134  kmlem13  10146  fin23lem32  10328  fin23lem41  10336  zfac  10444  zfcndpow  10601  zfcndinf  10603  zfcndac  10604  axgroth4  10817  relexpindlem  15100  ramcl  17089  mreexexlemd  17700  bnj1112  35316  axprALT2  35445  axpowg  35482  dfon2lem6  36177  dfon2lem7  36178  dfon2  36181  cbvralvw2  36627  axtcond  36878  wl-dfcleq  38048  phpreu  38143  axc11n-16  39602  nfa1w  43299  eu6w  43300  abbibw  43301  dfac11  43681  ismnushort  44903  modelaxrep  45582  cbvals  50468