Theorem cbval2 2004

Description: Rule used to change bound variables, using implicit substitution. (Contributed by NM, 22-Dec-2003.) (Revised by Mario Carneiro, 6-Oct-2016.)

Hypotheses

Ref	Expression
cbval2.1	⊢ Ⅎzφ
cbval2.2	⊢ Ⅎwφ
cbval2.3	⊢ Ⅎxψ
cbval2.4	⊢ Ⅎyψ
cbval2.5	⊢ ((x = z ∧ y = w) → (φ ↔ ψ))

Assertion

Ref	Expression
cbval2	⊢ (∀x∀yφ ↔ ∀z∀wψ)

Distinct variable groups:   x,y   y,z   x,w   z,w

Allowed substitution hints:   φ(x, y, z, w)   ψ(x, y, z, w)

Proof of Theorem cbval2

Step	Hyp	Ref	Expression
1		cbval2.1	. . 3 ⊢ Ⅎzφ
2	1	nfal 1842	. 2 ⊢ Ⅎz∀yφ
3		cbval2.3	. . 3 ⊢ Ⅎxψ
4	3	nfal 1842	. 2 ⊢ Ⅎx∀wψ
5		nfv 1619	. . . . . 6 ⊢ Ⅎw x = z
6		cbval2.2	. . . . . 6 ⊢ Ⅎwφ
7	5, 6	nfan 1824	. . . . 5 ⊢ Ⅎw(x = z ∧ φ)
8		nfv 1619	. . . . . 6 ⊢ Ⅎy x = z
9		cbval2.4	. . . . . 6 ⊢ Ⅎyψ
10	8, 9	nfan 1824	. . . . 5 ⊢ Ⅎy(x = z ∧ ψ)
11		cbval2.5	. . . . . . 7 ⊢ ((x = z ∧ y = w) → (φ ↔ ψ))
12	11	expcom 424	. . . . . 6 ⊢ (y = w → (x = z → (φ ↔ ψ)))
13	12	pm5.32d 620	. . . . 5 ⊢ (y = w → ((x = z ∧ φ) ↔ (x = z ∧ ψ)))
14	7, 10, 13	cbval 1984	. . . 4 ⊢ (∀y(x = z ∧ φ) ↔ ∀w(x = z ∧ ψ))
15		19.28v 1895	. . . 4 ⊢ (∀y(x = z ∧ φ) ↔ (x = z ∧ ∀yφ))
16		19.28v 1895	. . . 4 ⊢ (∀w(x = z ∧ ψ) ↔ (x = z ∧ ∀wψ))
17	14, 15, 16	3bitr3i 266	. . 3 ⊢ ((x = z ∧ ∀yφ) ↔ (x = z ∧ ∀wψ))
18		pm5.32 617	. . 3 ⊢ ((x = z → (∀yφ ↔ ∀wψ)) ↔ ((x = z ∧ ∀yφ) ↔ (x = z ∧ ∀wψ)))
19	17, 18	mpbir 200	. 2 ⊢ (x = z → (∀yφ ↔ ∀wψ))
20	2, 4, 19	cbval 1984	1 ⊢ (∀x∀yφ ↔ ∀z∀wψ)

This proof depends on syntax axioms:   → wi 4   ↔ wb 176   ∧ wa 358  ∀wal 1540  Ⅎwnf 1544

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925

This proof depends on definitions:  df-bi 177  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545

This theorem is used by:  cbval2v  2006  2mo  2282  2eu6  2289