Theorem ceqsex2 2896

Description: Elimination of two existential quantifiers, using implicit substitution. (Contributed by Scott Fenton, 7-Jun-2006.)

Hypotheses

Ref	Expression
ceqsex2.1	⊢ Ⅎxψ
ceqsex2.2	⊢ Ⅎyχ
ceqsex2.3	⊢ A ∈ V
ceqsex2.4	⊢ B ∈ V
ceqsex2.5	⊢ (x = A → (φ ↔ ψ))
ceqsex2.6	⊢ (y = B → (ψ ↔ χ))

Assertion

Ref	Expression
ceqsex2	⊢ (∃x∃y(x = A ∧ y = B ∧ φ) ↔ χ)

Distinct variable groups:   x,y,A   x,B,y

Allowed substitution hints:   φ(x,y)   ψ(x,y)   χ(x,y)

Proof of Theorem ceqsex2

Step	Hyp	Ref	Expression
1		3anass 938	. . . . 5 ⊢ ((x = A ∧ y = B ∧ φ) ↔ (x = A ∧ (y = B ∧ φ)))
2	1	exbii 1582	. . . 4 ⊢ (∃y(x = A ∧ y = B ∧ φ) ↔ ∃y(x = A ∧ (y = B ∧ φ)))
3		19.42v 1905	. . . 4 ⊢ (∃y(x = A ∧ (y = B ∧ φ)) ↔ (x = A ∧ ∃y(y = B ∧ φ)))
4	2, 3	bitri 240	. . 3 ⊢ (∃y(x = A ∧ y = B ∧ φ) ↔ (x = A ∧ ∃y(y = B ∧ φ)))
5	4	exbii 1582	. 2 ⊢ (∃x∃y(x = A ∧ y = B ∧ φ) ↔ ∃x(x = A ∧ ∃y(y = B ∧ φ)))
6		nfv 1619	. . . . 5 ⊢ Ⅎx y = B
7		ceqsex2.1	. . . . 5 ⊢ Ⅎxψ
8	6, 7	nfan 1824	. . . 4 ⊢ Ⅎx(y = B ∧ ψ)
9	8	nfex 1843	. . 3 ⊢ Ⅎx∃y(y = B ∧ ψ)
10		ceqsex2.3	. . 3 ⊢ A ∈ V
11		ceqsex2.5	. . . . 5 ⊢ (x = A → (φ ↔ ψ))
12	11	anbi2d 684	. . . 4 ⊢ (x = A → ((y = B ∧ φ) ↔ (y = B ∧ ψ)))
13	12	exbidv 1626	. . 3 ⊢ (x = A → (∃y(y = B ∧ φ) ↔ ∃y(y = B ∧ ψ)))
14	9, 10, 13	ceqsex 2894	. 2 ⊢ (∃x(x = A ∧ ∃y(y = B ∧ φ)) ↔ ∃y(y = B ∧ ψ))
15		ceqsex2.2	. . 3 ⊢ Ⅎyχ
16		ceqsex2.4	. . 3 ⊢ B ∈ V
17		ceqsex2.6	. . 3 ⊢ (y = B → (ψ ↔ χ))
18	15, 16, 17	ceqsex 2894	. 2 ⊢ (∃y(y = B ∧ ψ) ↔ χ)
19	5, 14, 18	3bitri 262	1 ⊢ (∃x∃y(x = A ∧ y = B ∧ φ) ↔ χ)

Syntax hints:   → wi 4   ↔ wb 176   ∧ wa 358   ∧ w3a 934  ∃wex 1541  Ⅎwnf 1544   = wceq 1642   ∈ wcel 1710  Vcvv 2860

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-ext 2334

This theorem depends on definitions:  df-bi 177  df-an 360  df-3an 936  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2340  df-cleq 2346  df-clel 2349  df-v 2862

This theorem is referenced by:  ceqsex2v  2897