ceqsrexv

Description: Elimination of a restricted existential quantifier, using implicit substitution. (Contributed by NM, 30-Apr-2004)

		Ref	Expression
	Hypothesis	ceqsrexv.1	$⊢ x = A \to (φ \leftrightarrow ψ)$
	Assertion	ceqsrexv	$⊢ A \in B \to (\exists x \in B (x = A \land φ) \leftrightarrow ψ)$

Step	Hyp	Ref	Expression
1		ceqsrexv.1	$⊢ x = A \to (φ \leftrightarrow ψ)$
2		df-rex	$⊢ \exists x \in B (x = A \land φ) \leftrightarrow \exists x (x \in B \land (x = A \land φ))$
3		an12	$⊢ (x = A \land (x \in B \land φ)) \leftrightarrow (x \in B \land (x = A \land φ))$
4	3	exbii	$⊢ \exists x (x = A \land (x \in B \land φ)) \leftrightarrow \exists x (x \in B \land (x = A \land φ))$
5	2 4	bitr4i	$⊢ \exists x \in B (x = A \land φ) \leftrightarrow \exists x (x = A \land (x \in B \land φ))$
6		eleq1	$⊢ x = A \to (x \in B \leftrightarrow A \in B)$
7	6 1	anbi12d	$⊢ x = A \to ((x \in B \land φ) \leftrightarrow (A \in B \land ψ))$
8	7	ceqsexgv	$⊢ A \in B \to (\exists x (x = A \land (x \in B \land φ)) \leftrightarrow (A \in B \land ψ))$
9	8	bianabs	$⊢ A \in B \to (\exists x (x = A \land (x \in B \land φ)) \leftrightarrow ψ)$
10	5 9	bitrid	$⊢ A \in B \to (\exists x \in B (x = A \land φ) \leftrightarrow ψ)$

Metamath Proof Explorer