Theorem cbvalvw 2035

Description: Change bound variable. Uses only Tarski's FOL axiom schemes. See cbvalv 2405 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 2034	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 2007

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780

This theorem is referenced by:  cbvexvw  2036  cbvaldvaw  2037  cbval2vw  2039  alcomimw  2042  hba1w  2047  sbjust  2063  ax12wdemo  2135  mo4  2566  cbvmovw  2602  nfcjust  2891  cbvralvw  3237  cbvraldva2  3348  sbralie  3358  zfpow  5366  tfisi  7880  findcard  9203  pssnn  9208  ssfi  9213  findcard3  9318  findcard3OLD  9319  zfinf  9679  ttrclss  9760  ttrclselem2  9766  aceq0  10158  kmlem1  10191  kmlem13  10203  fin23lem32  10384  fin23lem41  10392  zfac  10500  zfcndpow  10656  zfcndinf  10658  zfcndac  10659  axgroth4  10872  relexpindlem  15102  ramcl  17067  mreexexlemd  17687  bnj1112  34997  dfon2lem6  35789  dfon2lem7  35790  dfon2  35793  cbvralvw2  36227  phpreu  37611  axc11n-16  38939  nfa1w  42685  eu6w  42686  abbibw  42687  dfac11  43074  ismnushort  44320  modelaxrep  44998