Metamath Proof Explorer

Theorem ceqsrexv

Description: Elimination of a restricted existential quantifier, using implicit substitution. (Contributed by NM, 30-Apr-2004)

Ref Expression
Hypothesis ceqsrexv.1 ⊢ x = A → φ ↔ ψ
Assertion ceqsrexv ⊢ A ∈ B → ∃ x ∈ B x = A ∧ φ ↔ ψ

Proof

Step Hyp Ref Expression
1 ceqsrexv.1 ⊢ x = A → φ ↔ ψ
2 df-rex ⊢ ∃ x ∈ B x = A ∧ φ ↔ ∃ x x ∈ B ∧ x = A ∧ φ
3 an12 ⊢ x = A ∧ x ∈ B ∧ φ ↔ x ∈ B ∧ x = A ∧ φ
4 3 exbii ⊢ ∃ x x = A ∧ x ∈ B ∧ φ ↔ ∃ x x ∈ B ∧ x = A ∧ φ
5 2 4 bitr4i ⊢ ∃ x ∈ B x = A ∧ φ ↔ ∃ x x = A ∧ x ∈ B ∧ φ
6 eleq1 ⊢ x = A → x ∈ B ↔ A ∈ B
7 6 1 anbi12d ⊢ x = A → x ∈ B ∧ φ ↔ A ∈ B ∧ ψ
8 7 ceqsexgv ⊢ A ∈ B → ∃ x x = A ∧ x ∈ B ∧ φ ↔ A ∈ B ∧ ψ
9 8 bianabs ⊢ A ∈ B → ∃ x x = A ∧ x ∈ B ∧ φ ↔ ψ
10 5 9 syl5bb ⊢ A ∈ B → ∃ x ∈ B x = A ∧ φ ↔ ψ