This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
Assertion ceqsrexv ( 𝐴 ∈ 𝐵 → ( ∃ 𝑥 ∈ 𝐵 ( 𝑥 = 𝐴 ∧ 𝜑 ) ↔ 𝜓 ) )

Proof

Step Hyp Ref Expression
1 ceqsrexv.1 ⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
2 df-rex ⊢ ( ∃ 𝑥 ∈ 𝐵 ( 𝑥 = 𝐴 ∧ 𝜑 ) ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐵 ∧ ( 𝑥 = 𝐴 ∧ 𝜑 ) ) )
3 an12 ⊢ ( ( 𝑥 = 𝐴 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝜑 ) ) ↔ ( 𝑥 ∈ 𝐵 ∧ ( 𝑥 = 𝐴 ∧ 𝜑 ) ) )
4 3 exbii ⊢ ( ∃ 𝑥 ( 𝑥 = 𝐴 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝜑 ) ) ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐵 ∧ ( 𝑥 = 𝐴 ∧ 𝜑 ) ) )
5 2 4 bitr4i ⊢ ( ∃ 𝑥 ∈ 𝐵 ( 𝑥 = 𝐴 ∧ 𝜑 ) ↔ ∃ 𝑥 ( 𝑥 = 𝐴 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝜑 ) ) )
6 eleq1 ⊢ ( 𝑥 = 𝐴 → ( 𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵 ) )
7 6 1 anbi12d ⊢ ( 𝑥 = 𝐴 → ( ( 𝑥 ∈ 𝐵 ∧ 𝜑 ) ↔ ( 𝐴 ∈ 𝐵 ∧ 𝜓 ) ) )
8 7 ceqsexgv ⊢ ( 𝐴 ∈ 𝐵 → ( ∃ 𝑥 ( 𝑥 = 𝐴 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝜑 ) ) ↔ ( 𝐴 ∈ 𝐵 ∧ 𝜓 ) ) )
9 8 bianabs ⊢ ( 𝐴 ∈ 𝐵 → ( ∃ 𝑥 ( 𝑥 = 𝐴 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝜑 ) ) ↔ 𝜓 ) )
10 5 9 bitrid ⊢ ( 𝐴 ∈ 𝐵 → ( ∃ 𝑥 ∈ 𝐵 ( 𝑥 = 𝐴 ∧ 𝜑 ) ↔ 𝜓 ) )