Metamath Proof Explorer

Theorem ceqsrexbv

Description: Elimination of a restricted existential quantifier, using implicit substitution. (Contributed by Mario Carneiro, 14-Mar-2014)

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

Proof

Step Hyp Ref Expression
1 ceqsrexv.1 ⊢ x = A → φ ↔ ψ
2 r19.42v ⊢ ∃ x ∈ B A ∈ B ∧ x = A ∧ φ ↔ A ∈ B ∧ ∃ x ∈ B x = A ∧ φ
3 eleq1 ⊢ x = A → x ∈ B ↔ A ∈ B
4 3 adantr ⊢ x = A ∧ φ → x ∈ B ↔ A ∈ B
5 4 pm5.32ri ⊢ x ∈ B ∧ x = A ∧ φ ↔ A ∈ B ∧ x = A ∧ φ
6 5 bicomi ⊢ A ∈ B ∧ x = A ∧ φ ↔ x ∈ B ∧ x = A ∧ φ
7 6 baib ⊢ x ∈ B → A ∈ B ∧ x = A ∧ φ ↔ x = A ∧ φ
8 7 rexbiia ⊢ ∃ x ∈ B A ∈ B ∧ x = A ∧ φ ↔ ∃ x ∈ B x = A ∧ φ
9 1 ceqsrexv ⊢ A ∈ B → ∃ x ∈ B x = A ∧ φ ↔ ψ
10 9 pm5.32i ⊢ A ∈ B ∧ ∃ x ∈ B x = A ∧ φ ↔ A ∈ B ∧ ψ
11 2 8 10 3bitr3i ⊢ ∃ x ∈ B x = A ∧ φ ↔ A ∈ B ∧ ψ