Theorem cbvald 2441

Description: Deduction used to change bound variables, using implicit substitution, particularly useful in conjunction with dvelim 2485. Usage of this theorem is discouraged because it depends on ax-13 2406. See cbvaldw 2372 for a version with 𝑥, 𝑦 disjoint, not depending on ax-13 2406. (Contributed by NM, 2-Jan-2002.) (Revised by Mario Carneiro, 6-Oct-2016.) (Revised by Wolf Lammen, 13-May-2018.) (New usage is discouraged.)

Hypotheses

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

Assertion

Ref	Expression
cbvald	⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑦𝜒))

Distinct variable groups:   𝜑,𝑥   𝜒,𝑥

Allowed substitution hints:   𝜑(𝑦)   𝜓(𝑥, 𝑦)   𝜒(𝑦)

Proof of Theorem cbvald

Step	Hyp	Ref	Expression
1		nfv 1947	. 2 ⊢ Ⅎ𝑥𝜑
2		cbvald.1	. 2 ⊢ Ⅎ𝑦𝜑
3		cbvald.2	. 2 ⊢ (𝜑 → Ⅎ𝑦𝜓)
4		nfvd 1948	. 2 ⊢ (𝜑 → Ⅎ𝑥𝜒)
5		cbvald.3	. 2 ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒)))
6	1, 2, 3, 4, 5	cbv2 2437	1 ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑦𝜒))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209  ∀wal 1568  Ⅎwnf 1816

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-11 2195  ax-12 2216  ax-13 2406

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1813  df-nf 1817

This theorem is used by:  cbvexd  2442  cbvaldva  2443  axextnd  10591  axrepndlem1  10592  axunndlem1  10595  axpowndlem2  10598  axpowndlem3  10599  axpowndlem4  10600  axregndlem2  10603  axregnd  10604  axinfnd  10606  axacndlem5  10611  axacnd  10612  axextdist  36326  distel  36330  wl-sb8eut  38290