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 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 2433	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 2194  ax-12 2213  ax-13 2402

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  2438  cbvaldva  2439  axextnd  10669  axrepndlem1  10670  axunndlem1  10673  axpowndlem2  10676  axpowndlem3  10677  axpowndlem4  10678  axregndlem2  10681  axregnd  10682  axinfnd  10684  axacndlem5  10689  axacnd  10690  axextdist  36541  distel  36545  wl-sb8eut  38490