Theorem cbvalv 2382

Description: Rule used to change bound variables, using implicit substitution. (Contributed by NM, 5-Aug-1993.) Remove dependency on ax-10 2132. (Revised by Wolf Lammen, 17-Jul-2021.)

Hypothesis

Ref	Expression
cbvalv.1	⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
cbvalv	⊢ (∀𝑥𝜑 ↔ ∀𝑦𝜓)

Distinct variable groups:   𝜑,𝑦   𝜓,𝑥

Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑦)

Proof of Theorem cbvalv

Step	Hyp	Ref	Expression
1		ax-5 1952	. . . 4 ⊢ (𝜑 → ∀𝑦𝜑)
2	1	hbal 2149	. . 3 ⊢ (∀𝑥𝜑 → ∀𝑦∀𝑥𝜑)
3		cbvalv.1	. . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
4	3	spv 2369	. . 3 ⊢ (∀𝑥𝜑 → 𝜓)
5	2, 4	alrimih 1864	. 2 ⊢ (∀𝑥𝜑 → ∀𝑦𝜓)
6		ax-5 1952	. . . 4 ⊢ (𝜓 → ∀𝑥𝜓)
7	6	hbal 2149	. . 3 ⊢ (∀𝑦𝜓 → ∀𝑥∀𝑦𝜓)
8	3	equcoms 2066	. . . . 5 ⊢ (𝑦 = 𝑥 → (𝜑 ↔ 𝜓))
9	8	bicomd 213	. . . 4 ⊢ (𝑦 = 𝑥 → (𝜓 ↔ 𝜑))
10	9	spv 2369	. . 3 ⊢ (∀𝑦𝜓 → 𝜑)
11	7, 10	alrimih 1864	. 2 ⊢ (∀𝑦𝜓 → ∀𝑥𝜑)
12	5, 11	impbii 199	1 ⊢ (∀𝑥𝜑 ↔ ∀𝑦𝜓)

Syntax hints:   → wi 4   ↔ wb 196  ∀wal 1594

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1835  ax-4 1850  ax-5 1952  ax-6 2018  ax-7 2054  ax-11 2147  ax-12 2160  ax-13 2355

This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1818

This theorem is referenced by:  cbvexv  2384  cbvaldva  2390  cbval2v  2394  nfcjust  2854  cdeqal1  3532  zfpow  4949  tfisi  7175  pssnn  8294  findcard  8315  findcard3  8319  zfinf  8649  aceq0  9054  kmlem1  9085  kmlem13  9097  fin23lem32  9279  fin23lem41  9287  zfac  9395  zfcndpow  9551  zfcndinf  9553  zfcndac  9554  axgroth4  9767  relexpindlem  13923  ramcl  15856  mreexexlemd  16427  bnj1112  31279  dfon2lem6  31919  dfon2lem7  31920  dfon2  31923  phpreu  33625  axc11n-16  34644  dfac11  38051