Metamath Proof Explorer

Theorem ceqsrex2v

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

Ref Expression
Hypotheses ceqsrex2v.1 ⊢ x = A → φ ↔ ψ
ceqsrex2v.2 ⊢ y = B → ψ ↔ χ
Assertion ceqsrex2v ⊢ A ∈ C ∧ B ∈ D → ∃ x ∈ C ∃ y ∈ D x = A ∧ y = B ∧ φ ↔ χ

Proof

Step Hyp Ref Expression
1 ceqsrex2v.1 ⊢ x = A → φ ↔ ψ
2 ceqsrex2v.2 ⊢ y = B → ψ ↔ χ
3 anass ⊢ x = A ∧ y = B ∧ φ ↔ x = A ∧ y = B ∧ φ
4 3 rexbii ⊢ ∃ y ∈ D x = A ∧ y = B ∧ φ ↔ ∃ y ∈ D x = A ∧ y = B ∧ φ
5 r19.42v ⊢ ∃ y ∈ D x = A ∧ y = B ∧ φ ↔ x = A ∧ ∃ y ∈ D y = B ∧ φ
6 4 5 bitri ⊢ ∃ y ∈ D x = A ∧ y = B ∧ φ ↔ x = A ∧ ∃ y ∈ D y = B ∧ φ
7 6 rexbii ⊢ ∃ x ∈ C ∃ y ∈ D x = A ∧ y = B ∧ φ ↔ ∃ x ∈ C x = A ∧ ∃ y ∈ D y = B ∧ φ
8 1 anbi2d ⊢ x = A → y = B ∧ φ ↔ y = B ∧ ψ
9 8 rexbidv ⊢ x = A → ∃ y ∈ D y = B ∧ φ ↔ ∃ y ∈ D y = B ∧ ψ
10 9 ceqsrexv ⊢ A ∈ C → ∃ x ∈ C x = A ∧ ∃ y ∈ D y = B ∧ φ ↔ ∃ y ∈ D y = B ∧ ψ
11 7 10 syl5bb ⊢ A ∈ C → ∃ x ∈ C ∃ y ∈ D x = A ∧ y = B ∧ φ ↔ ∃ y ∈ D y = B ∧ ψ
12 2 ceqsrexv ⊢ B ∈ D → ∃ y ∈ D y = B ∧ ψ ↔ χ
13 11 12 sylan9bb ⊢ A ∈ C ∧ B ∈ D → ∃ x ∈ C ∃ y ∈ D x = A ∧ y = B ∧ φ ↔ χ