Theorem ceqsrex2v 2670

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 ∈ 𝐶 ∧ B ∈ 𝐷) → (∃x ∈ 𝐶 ∃y ∈ 𝐷 ((x = A ∧ y = B) ∧ φ) ↔ χ))

Distinct variable groups:   x,y,A   x,B,y   x,𝐶   x,𝐷,y   ψ,x   χ,y

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

Proof of Theorem ceqsrex2v

Step	Hyp	Ref	Expression
1		anass 381	. . . . . 6 ⊢ (((x = A ∧ y = B) ∧ φ) ↔ (x = A ∧ (y = B ∧ φ)))
2	1	rexbii 2325	. . . . 5 ⊢ (∃y ∈ 𝐷 ((x = A ∧ y = B) ∧ φ) ↔ ∃y ∈ 𝐷 (x = A ∧ (y = B ∧ φ)))
3		r19.42v 2461	. . . . 5 ⊢ (∃y ∈ 𝐷 (x = A ∧ (y = B ∧ φ)) ↔ (x = A ∧ ∃y ∈ 𝐷 (y = B ∧ φ)))
4	2, 3	bitri 173	. . . 4 ⊢ (∃y ∈ 𝐷 ((x = A ∧ y = B) ∧ φ) ↔ (x = A ∧ ∃y ∈ 𝐷 (y = B ∧ φ)))
5	4	rexbii 2325	. . 3 ⊢ (∃x ∈ 𝐶 ∃y ∈ 𝐷 ((x = A ∧ y = B) ∧ φ) ↔ ∃x ∈ 𝐶 (x = A ∧ ∃y ∈ 𝐷 (y = B ∧ φ)))
6		ceqsrex2v.1	. . . . . 6 ⊢ (x = A → (φ ↔ ψ))
7	6	anbi2d 437	. . . . 5 ⊢ (x = A → ((y = B ∧ φ) ↔ (y = B ∧ ψ)))
8	7	rexbidv 2321	. . . 4 ⊢ (x = A → (∃y ∈ 𝐷 (y = B ∧ φ) ↔ ∃y ∈ 𝐷 (y = B ∧ ψ)))
9	8	ceqsrexv 2668	. . 3 ⊢ (A ∈ 𝐶 → (∃x ∈ 𝐶 (x = A ∧ ∃y ∈ 𝐷 (y = B ∧ φ)) ↔ ∃y ∈ 𝐷 (y = B ∧ ψ)))
10	5, 9	syl5bb 181	. 2 ⊢ (A ∈ 𝐶 → (∃x ∈ 𝐶 ∃y ∈ 𝐷 ((x = A ∧ y = B) ∧ φ) ↔ ∃y ∈ 𝐷 (y = B ∧ ψ)))
11		ceqsrex2v.2	. . 3 ⊢ (y = B → (ψ ↔ χ))
12	11	ceqsrexv 2668	. 2 ⊢ (B ∈ 𝐷 → (∃y ∈ 𝐷 (y = B ∧ ψ) ↔ χ))
13	10, 12	sylan9bb 435	1 ⊢ ((A ∈ 𝐶 ∧ B ∈ 𝐷) → (∃x ∈ 𝐶 ∃y ∈ 𝐷 ((x = A ∧ y = B) ∧ φ) ↔ χ))

Syntax hints:   → wi 4   ∧ wa 97   ↔ wb 98   = wceq 1242   ∈ wcel 1390  ∃wrex 2301

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bndl 1396  ax-4 1397  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019

This theorem depends on definitions:  df-bi 110  df-tru 1245  df-nf 1347  df-sb 1643  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-rex 2306  df-v 2553

This theorem is referenced by: (None)