Theorem cbvald 2265

Description: Deduction used to change bound variables, using implicit substitution, particularly useful in conjunction with dvelim 2325. (Contributed by NM, 2-Jan-2002.) (Revised by Mario Carneiro, 6-Oct-2016.) (Revised by Wolf Lammen, 13-May-2018.)

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 1830	. 2 ⊢ Ⅎ𝑥𝜑
2		cbvald.1	. 2 ⊢ Ⅎ𝑦𝜑
3		cbvald.2	. 2 ⊢ (𝜑 → Ⅎ𝑦𝜓)
4		nfvd 1831	. 2 ⊢ (𝜑 → Ⅎ𝑥𝜒)
5		cbvald.3	. 2 ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒)))
6	1, 2, 3, 4, 5	cbv2 2258	1 ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑦𝜒))

Syntax hints:   → wi 4   ↔ wb 195  ∀wal 1473  Ⅎwnf 1699

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-ex 1696  df-nf 1701

This theorem is referenced by:  cbvexd  2266  cbvaldvaOLD  2270  axextnd  9292  axrepndlem1  9293  axunndlem1  9296  axpowndlem2  9299  axpowndlem3  9300  axpowndlem4  9301  axregndlem2  9304  axregnd  9305  axinfnd  9307  axacndlem5  9312  axacnd  9313  axextdist  30949  distel  30953  wl-sb8eut  32538