Theorem cbval 1801

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

Syntax hints:   → wi 4   ↔ wb 105  ∀wal 1395  Ⅎwnf 1508

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 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582

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

This theorem is referenced by:  sb8  1903  cbval2  1969  sb8eu  2091  abbi  2344  cleqf  2398  cbvralf  2757  ralab2  2969  cbvralcsf  3189  dfss2f  3217  elintab  3940  cbviota  5293  sb8iota  5296  dffun6f  5341  dffun4f  5344  mptfvex  5735  findcard2  7083  findcard2s  7084