Theorem cbvalvw 2036

Description: Change bound variable. Uses only Tarski's FOL axiom schemes. See cbvalv 2399 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  2560  cbvmovw  2596  nfcjust  2878  cbvralvw  3216  cbvraldva2  3323  sbralie  3328  sbralieOLD  3330  zfpow  5323  tfisi  7837  findcard  9132  pssnn  9137  ssfi  9142  findcard3  9235  findcard3OLD  9236  zfinf  9598  ttrclss  9679  ttrclselem2  9685  aceq0  10077  kmlem1  10110  kmlem13  10122  fin23lem32  10303  fin23lem41  10311  zfac  10419  zfcndpow  10575  zfcndinf  10577  zfcndac  10578  axgroth4  10791  relexpindlem  15035  ramcl  17006  mreexexlemd  17611  bnj1112  34979  dfon2lem6  35771  dfon2lem7  35772  dfon2  35775  cbvralvw2  36209  phpreu  37593  axc11n-16  38926  nfa1w  42656  eu6w  42657  abbibw  42658  dfac11  43044  ismnushort  44283  modelaxrep  44964