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  5324  tfisi  7838  findcard  9133  pssnn  9138  ssfi  9143  findcard3  9236  findcard3OLD  9237  zfinf  9599  ttrclss  9680  ttrclselem2  9686  aceq0  10078  kmlem1  10111  kmlem13  10123  fin23lem32  10304  fin23lem41  10312  zfac  10420  zfcndpow  10576  zfcndinf  10578  zfcndac  10579  axgroth4  10792  relexpindlem  15036  ramcl  17007  mreexexlemd  17612  bnj1112  34980  dfon2lem6  35783  dfon2lem7  35784  dfon2  35787  cbvralvw2  36221  phpreu  37605  axc11n-16  38938  nfa1w  42670  eu6w  42671  abbibw  42672  dfac11  43058  ismnushort  44297  modelaxrep  44978