Theorem ceqsrex2v 2975

Description: Elimination of a restricted existential quantifier, using implicit substitution. (Contributed by NM, 29-Oct-2005.)

Hypotheses

Ref	Expression
ceqsrex2v.1	⊢ (x = A → (φ ↔ ψ))
ceqsrex2v.2	⊢ (y = B → (ψ ↔ χ))

Assertion

Ref	Expression
ceqsrex2v	⊢ ((A ∈ C ∧ B ∈ D) → (∃x ∈ C ∃y ∈ D ((x = A ∧ y = B) ∧ φ) ↔ χ))

Distinct variable groups:   x,y,A   x,B,y   x,C   x,D,y   ψ,x   χ,y

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

Proof of Theorem ceqsrex2v

Step	Hyp	Ref	Expression
1		anass 630	. . . . . 6 ⊢ (((x = A ∧ y = B) ∧ φ) ↔ (x = A ∧ (y = B ∧ φ)))
2	1	rexbii 2640	. . . . 5 ⊢ (∃y ∈ D ((x = A ∧ y = B) ∧ φ) ↔ ∃y ∈ D (x = A ∧ (y = B ∧ φ)))
3		r19.42v 2766	. . . . 5 ⊢ (∃y ∈ D (x = A ∧ (y = B ∧ φ)) ↔ (x = A ∧ ∃y ∈ D (y = B ∧ φ)))
4	2, 3	bitri 240	. . . 4 ⊢ (∃y ∈ D ((x = A ∧ y = B) ∧ φ) ↔ (x = A ∧ ∃y ∈ D (y = B ∧ φ)))
5	4	rexbii 2640	. . 3 ⊢ (∃x ∈ C ∃y ∈ D ((x = A ∧ y = B) ∧ φ) ↔ ∃x ∈ C (x = A ∧ ∃y ∈ D (y = B ∧ φ)))
6		ceqsrex2v.1	. . . . . 6 ⊢ (x = A → (φ ↔ ψ))
7	6	anbi2d 684	. . . . 5 ⊢ (x = A → ((y = B ∧ φ) ↔ (y = B ∧ ψ)))
8	7	rexbidv 2636	. . . 4 ⊢ (x = A → (∃y ∈ D (y = B ∧ φ) ↔ ∃y ∈ D (y = B ∧ ψ)))
9	8	ceqsrexv 2973	. . 3 ⊢ (A ∈ C → (∃x ∈ C (x = A ∧ ∃y ∈ D (y = B ∧ φ)) ↔ ∃y ∈ D (y = B ∧ ψ)))
10	5, 9	syl5bb 248	. 2 ⊢ (A ∈ C → (∃x ∈ C ∃y ∈ D ((x = A ∧ y = B) ∧ φ) ↔ ∃y ∈ D (y = B ∧ ψ)))
11		ceqsrex2v.2	. . 3 ⊢ (y = B → (ψ ↔ χ))
12	11	ceqsrexv 2973	. 2 ⊢ (B ∈ D → (∃y ∈ D (y = B ∧ ψ) ↔ χ))
13	10, 12	sylan9bb 680	1 ⊢ ((A ∈ C ∧ B ∈ D) → (∃x ∈ C ∃y ∈ D ((x = A ∧ y = B) ∧ φ) ↔ χ))

This proof depends on syntax axioms:   → wi 4   ↔ wb 176   ∧ wa 358   = wceq 1642   ∈ wcel 1710  ∃wrex 2616

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

This proof depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2479  df-rex 2621  df-v 2862

This theorem is used by: (None)