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

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

Proof

Step Hyp Ref Expression
1 ceqsrexv.1 ⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
2 r19.42v ⊢ ( ∃ 𝑥 ∈ 𝐵 ( 𝐴 ∈ 𝐵 ∧ ( 𝑥 = 𝐴 ∧ 𝜑 ) ) ↔ ( 𝐴 ∈ 𝐵 ∧ ∃ 𝑥 ∈ 𝐵 ( 𝑥 = 𝐴 ∧ 𝜑 ) ) )
3 eleq1 ⊢ ( 𝑥 = 𝐴 → ( 𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵 ) )
4 3 adantr ⊢ ( ( 𝑥 = 𝐴 ∧ 𝜑 ) → ( 𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵 ) )
5 4 pm5.32ri ⊢ ( ( 𝑥 ∈ 𝐵 ∧ ( 𝑥 = 𝐴 ∧ 𝜑 ) ) ↔ ( 𝐴 ∈ 𝐵 ∧ ( 𝑥 = 𝐴 ∧ 𝜑 ) ) )
6 5 bicomi ⊢ ( ( 𝐴 ∈ 𝐵 ∧ ( 𝑥 = 𝐴 ∧ 𝜑 ) ) ↔ ( 𝑥 ∈ 𝐵 ∧ ( 𝑥 = 𝐴 ∧ 𝜑 ) ) )
7 6 baib ⊢ ( 𝑥 ∈ 𝐵 → ( ( 𝐴 ∈ 𝐵 ∧ ( 𝑥 = 𝐴 ∧ 𝜑 ) ) ↔ ( 𝑥 = 𝐴 ∧ 𝜑 ) ) )
8 7 rexbiia ⊢ ( ∃ 𝑥 ∈ 𝐵 ( 𝐴 ∈ 𝐵 ∧ ( 𝑥 = 𝐴 ∧ 𝜑 ) ) ↔ ∃ 𝑥 ∈ 𝐵 ( 𝑥 = 𝐴 ∧ 𝜑 ) )
9 1 ceqsrexv ⊢ ( 𝐴 ∈ 𝐵 → ( ∃ 𝑥 ∈ 𝐵 ( 𝑥 = 𝐴 ∧ 𝜑 ) ↔ 𝜓 ) )
10 9 pm5.32i ⊢ ( ( 𝐴 ∈ 𝐵 ∧ ∃ 𝑥 ∈ 𝐵 ( 𝑥 = 𝐴 ∧ 𝜑 ) ) ↔ ( 𝐴 ∈ 𝐵 ∧ 𝜓 ) )
11 2 8 10 3bitr3i ⊢ ( ∃ 𝑥 ∈ 𝐵 ( 𝑥 = 𝐴 ∧ 𝜑 ) ↔ ( 𝐴 ∈ 𝐵 ∧ 𝜓 ) )