Theorem cbvald 2437

Description: Deduction used to change bound variables, using implicit substitution, particularly useful in conjunction with dvelim 2481. Usage of this theorem is discouraged because it depends on ax-13 2402. See cbvaldw 2368 for a version with 𝑥, 𝑦 disjoint, not depending on ax-13 2402. (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 1933	. 2 ⊢ Ⅎ𝑥𝜑
2		cbvald.1	. 2 ⊢ Ⅎ𝑦𝜑
3		cbvald.2	. 2 ⊢ (𝜑 → Ⅎ𝑦𝜓)
4		nfvd 1934	. 2 ⊢ (𝜑 → Ⅎ𝑥𝜒)
5		cbvald.3	. 2 ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒)))
6	1, 2, 3, 4, 5	cbv2 2433	1 ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑦𝜒))

Syntax hints:   → wi 4   ↔ wb 208  ∀wal 1557  Ⅎwnf 1802

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-11 2190  ax-12 2211  ax-13 2402

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-ex 1799  df-nf 1803

This theorem is referenced by:  cbvexd  2438  cbvaldva  2439  axextnd  10543  axrepndlem1  10544  axunndlem1  10547  axpowndlem2  10550  axpowndlem3  10551  axpowndlem4  10552  axregndlem2  10555  axregnd  10556  axinfnd  10558  axacndlem5  10563  axacnd  10564  axextdist  36108  distel  36112  wl-sb8eut  38042