Theorem cbval 1780

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 1545	. 2 ⊢ (𝜑 → ∀𝑦𝜑)
3		cbval.2	. . 3 ⊢ Ⅎ𝑥𝜓
4	3	nfri 1545	. 2 ⊢ (𝜓 → ∀𝑥𝜓)
5		cbval.3	. 2 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
6	2, 4, 5	cbvalh 1779	1 ⊢ (∀𝑥𝜑 ↔ ∀𝑦𝜓)

Syntax hints:   → wi 4   ↔ wb 105  ∀wal 1373  Ⅎwnf 1486

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1473  ax-7 1474  ax-gen 1475  ax-ie1 1519  ax-ie2 1520  ax-8 1530  ax-4 1536  ax-17 1552  ax-i9 1556  ax-ial 1560

This theorem depends on definitions:  df-bi 117  df-nf 1487

This theorem is referenced by:  sb8  1882  cbval2  1948  sb8eu  2070  abbi  2323  cleqf  2377  cbvralf  2736  ralab2  2947  cbvralcsf  3167  dfss2f  3195  elintab  3913  cbviota  5259  sb8iota  5262  dffun6f  5307  dffun4f  5310  mptfvex  5693  findcard2  7019  findcard2s  7020