Theorem cbvald 2424

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

Syntax hints:   → wi 4   ↔ wb 208  ∀wal 1531  Ⅎwnf 1780

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-11 2156  ax-12 2172  ax-13 2386

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-ex 1777  df-nf 1781

This theorem is referenced by:  cbvexd  2425  cbvaldva  2426  axextnd  10007  axrepndlem1  10008  axunndlem1  10011  axpowndlem2  10014  axpowndlem3  10015  axpowndlem4  10016  axregndlem2  10019  axregnd  10020  axinfnd  10022  axacndlem5  10027  axacnd  10028  axextdist  33039  distel  33043  wl-sb8eut  34807