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