Theorem cbvalv 2261

Description: Rule used to change bound variables, using implicit substitution. (Contributed by NM, 5-Aug-1993.) Remove dependency on ax-10 2006. (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 1830	. . . 4 ⊢ Ⅎ𝑦𝜑
2	1	nfal 2139	. . 3 ⊢ Ⅎ𝑦∀𝑥𝜑
3		cbvalv.1	. . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
4	3	spv 2248	. . 3 ⊢ (∀𝑥𝜑 → 𝜓)
5	2, 4	alrimi 2069	. 2 ⊢ (∀𝑥𝜑 → ∀𝑦𝜓)
6		nfv 1830	. . . 4 ⊢ Ⅎ𝑥𝜓
7	6	nfal 2139	. . 3 ⊢ Ⅎ𝑥∀𝑦𝜓
8	3	equcoms 1934	. . . . 5 ⊢ (𝑦 = 𝑥 → (𝜑 ↔ 𝜓))
9	8	bicomd 212	. . . 4 ⊢ (𝑦 = 𝑥 → (𝜓 ↔ 𝜑))
10	9	spv 2248	. . 3 ⊢ (∀𝑦𝜓 → 𝜑)
11	7, 10	alrimi 2069	. 2 ⊢ (∀𝑦𝜓 → ∀𝑥𝜑)
12	5, 11	impbii 198	1 ⊢ (∀𝑥𝜑 ↔ ∀𝑦𝜓)

Syntax hints:   → wi 4   ↔ wb 195  ∀wal 1473

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234

This theorem depends on definitions:  df-bi 196  df-an 385  df-ex 1696  df-nf 1701

This theorem is referenced by:  cbvexv  2263  cbvaldva  2269  cbval2v  2273  nfcjust  2739  cdeqal1  3393  zfpow  4770  tfisi  6950  pssnn  8063  findcard  8084  findcard3  8088  zfinf  8419  aceq0  8824  kmlem1  8855  kmlem13  8867  fin23lem32  9049  fin23lem41  9057  zfac  9165  zfcndpow  9317  zfcndinf  9319  zfcndac  9320  axgroth4  9533  relexpindlem  13651  ramcl  15571  mreexexlemd  16127  bnj1112  30305  dfon2lem6  30937  dfon2lem7  30938  dfon2  30941  phpreu  32563  axc11n-16  33241  dfac11  36650