Theorem cbvex2 2005

Description: Rule used to change bound variables, using implicit substitution. (Contributed by NM, 14-Sep-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
cbvex2	⊢ (∃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 cbvex2

Step	Hyp	Ref	Expression
1		cbval2.1	. . 3 ⊢ Ⅎzφ
2	1	nfex 1843	. 2 ⊢ Ⅎz∃yφ
3		cbval2.3	. . 3 ⊢ Ⅎxψ
4	3	nfex 1843	. 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	cbvex 1985	. . . 4 ⊢ (∃y(x = z ∧ φ) ↔ ∃w(x = z ∧ ψ))
15		19.42v 1905	. . . 4 ⊢ (∃y(x = z ∧ φ) ↔ (x = z ∧ ∃yφ))
16		19.42v 1905	. . . 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	cbvex 1985	1 ⊢ (∃x∃yφ ↔ ∃z∃wψ)

Syntax hints:   → wi 4   ↔ wb 176   ∧ wa 358  ∃wex 1541  Ⅎwnf 1544

This theorem was proved from 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 theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545

This theorem is referenced by:  cbvex2v  2007  2eu6  2289  cbvopab  4631  cbvoprab12  5570