Theorem cbvald 2405

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

Syntax hints:   → wi 4   ↔ wb 205  ∀wal 1539  Ⅎwnf 1785

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-11 2154  ax-12 2171  ax-13 2370

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-ex 1782  df-nf 1786

This theorem is referenced by:  cbvexd  2406  cbvaldva  2407  axextnd  10536  axrepndlem1  10537  axunndlem1  10540  axpowndlem2  10543  axpowndlem3  10544  axpowndlem4  10545  axregndlem2  10548  axregnd  10549  axinfnd  10551  axacndlem5  10556  axacnd  10557  axextdist  34460  distel  34464  wl-sb8eut  36105