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