Theorem cbvalv 2260

Description: Rule used to change bound variables, using implicit substitution. (Contributed by NM, 5-Aug-1993.) Remove dependency on ax-10 2005. (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		nfv 1829	. . . 4 ⊢ Ⅎ𝑦𝜑
2	1	nfal 2138	. . 3 ⊢ Ⅎ𝑦∀𝑥𝜑
3		cbvalv.1	. . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
4	3	spv 2247	. . 3 ⊢ (∀𝑥𝜑 → 𝜓)
5	2, 4	alrimi 2068	. 2 ⊢ (∀𝑥𝜑 → ∀𝑦𝜓)
6		nfv 1829	. . . 4 ⊢ Ⅎ𝑥𝜓
7	6	nfal 2138	. . 3 ⊢ Ⅎ𝑥∀𝑦𝜓
8	3	equcoms 1933	. . . . 5 ⊢ (𝑦 = 𝑥 → (𝜑 ↔ 𝜓))
9	8	bicomd 211	. . . 4 ⊢ (𝑦 = 𝑥 → (𝜓 ↔ 𝜑))
10	9	spv 2247	. . 3 ⊢ (∀𝑦𝜓 → 𝜑)
11	7, 10	alrimi 2068	. 2 ⊢ (∀𝑦𝜓 → ∀𝑥𝜑)
12	5, 11	impbii 197	1 ⊢ (∀𝑥𝜑 ↔ ∀𝑦𝜓)

Syntax hints:   → wi 4   ↔ wb 194  ∀wal 1472

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233

This theorem depends on definitions:  df-bi 195  df-an 384  df-ex 1695  df-nf 1700

This theorem is referenced by:  cbvexv  2262  cbvaldva  2268  cbval2v  2272  nfcjust  2738  cdeqal1  3392  zfpow  4764  tfisi  6927  pssnn  8040  findcard  8061  findcard3  8065  zfinf  8396  aceq0  8801  kmlem1  8832  kmlem13  8844  fin23lem32  9026  fin23lem41  9034  zfac  9142  zfcndpow  9294  zfcndinf  9296  zfcndac  9297  axgroth4  9510  relexpindlem  13599  ramcl  15519  mreexexlemd  16075  bnj1112  30098  dfon2lem6  30730  dfon2lem7  30731  dfon2  30734  phpreu  32346  axc11n-16  33024  dfac11  36433