Theorem cbvalv 2309

Description: Rule used to change bound variables, using implicit substitution. (Contributed by NM, 5-Aug-1993.) Remove dependency on ax-10 2059. (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 1879	. . . 4 ⊢ (𝜑 → ∀𝑦𝜑)
2	1	hbal 2076	. . 3 ⊢ (∀𝑥𝜑 → ∀𝑦∀𝑥𝜑)
3		cbvalv.1	. . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
4	3	spv 2296	. . 3 ⊢ (∀𝑥𝜑 → 𝜓)
5	2, 4	alrimih 1791	. 2 ⊢ (∀𝑥𝜑 → ∀𝑦𝜓)
6		ax-5 1879	. . . 4 ⊢ (𝜓 → ∀𝑥𝜓)
7	6	hbal 2076	. . 3 ⊢ (∀𝑦𝜓 → ∀𝑥∀𝑦𝜓)
8	3	equcoms 1993	. . . . 5 ⊢ (𝑦 = 𝑥 → (𝜑 ↔ 𝜓))
9	8	bicomd 213	. . . 4 ⊢ (𝑦 = 𝑥 → (𝜓 ↔ 𝜑))
10	9	spv 2296	. . 3 ⊢ (∀𝑦𝜓 → 𝜑)
11	7, 10	alrimih 1791	. 2 ⊢ (∀𝑦𝜓 → ∀𝑥𝜑)
12	5, 11	impbii 199	1 ⊢ (∀𝑥𝜑 ↔ ∀𝑦𝜓)

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-11 2074  ax-12 2087  ax-13 2282

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

This theorem is referenced by:  cbvexv  2311  cbvaldva  2317  cbval2v  2321  nfcjust  2781  cdeqal1  3459  zfpow  4874  tfisi  7100  pssnn  8219  findcard  8240  findcard3  8244  zfinf  8574  aceq0  8979  kmlem1  9010  kmlem13  9022  fin23lem32  9204  fin23lem41  9212  zfac  9320  zfcndpow  9476  zfcndinf  9478  zfcndac  9479  axgroth4  9692  relexpindlem  13847  ramcl  15780  mreexexlemd  16351  bnj1112  31177  dfon2lem6  31817  dfon2lem7  31818  dfon2  31821  phpreu  33523  axc11n-16  34542  dfac11  37949