Theorem cbvald 2428

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

Syntax hints:   → wi 4   ↔ wb 208  ∀wal 1548  Ⅎwnf 1793

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1805  ax-4 1819  ax-5 1920  ax-6 1977  ax-7 2018  ax-11 2181  ax-12 2202  ax-13 2393

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 857  df-ex 1790  df-nf 1794

This theorem is referenced by:  cbvexd  2429  cbvaldva  2430  axextnd  10535  axrepndlem1  10536  axunndlem1  10539  axpowndlem2  10542  axpowndlem3  10543  axpowndlem4  10544  axregndlem2  10547  axregnd  10548  axinfnd  10550  axacndlem5  10555  axacnd  10556  axextdist  36085  distel  36089  wl-sb8eut  38019