Theorem cbval 1677

Description: Rule used to change bound variables, using implicit substitution. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 3-Oct-2016.)

Hypotheses

Ref	Expression
cbval.1	⊢ Ⅎ𝑦𝜑
cbval.2	⊢ Ⅎ𝑥𝜓
cbval.3	⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))

Assertion

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

Proof of Theorem cbval

Step	Hyp	Ref	Expression
1		cbval.1	. . 3 ⊢ Ⅎ𝑦𝜑
2	1	nfri 1452	. 2 ⊢ (𝜑 → ∀𝑦𝜑)
3		cbval.2	. . 3 ⊢ Ⅎ𝑥𝜓
4	3	nfri 1452	. 2 ⊢ (𝜓 → ∀𝑥𝜓)
5		cbval.3	. 2 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
6	2, 4, 5	cbvalh 1676	1 ⊢ (∀𝑥𝜑 ↔ ∀𝑦𝜓)

Syntax hints:   → wi 4   ↔ wb 103  ∀wal 1282  Ⅎwnf 1389

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1376  ax-7 1377  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-8 1435  ax-4 1440  ax-17 1459  ax-i9 1463  ax-ial 1467

This theorem depends on definitions:  df-bi 115  df-nf 1390

This theorem is referenced by:  sb8  1777  cbval2  1837  sb8eu  1954  abbi  2192  cleqf  2242  cbvralf  2571  ralab2  2756  cbvralcsf  2964  dfss2f  2990  elintab  3647  cbviota  4892  sb8iota  4894  dffun6f  4935  dffun4f  4938  mptfvex  5277  findcard2  6373  findcard2s  6374