ceqsrexbv

Description: Elimination of a restricted existential quantifier, using implicit substitution. (Contributed by Mario Carneiro, 14-Mar-2014)

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

Step	Hyp	Ref	Expression
1		ceqsrexv.1	$⊢ x = A \to (φ \leftrightarrow ψ)$
2		r19.42v	$⊢ \exists x \in B (A \in B \land (x = A \land φ)) \leftrightarrow (A \in B \land \exists x \in B (x = A \land φ))$
3		eleq1	$⊢ x = A \to (x \in B \leftrightarrow A \in B)$
4	3	adantr	$⊢ (x = A \land φ) \to (x \in B \leftrightarrow A \in B)$
5	4	pm5.32ri	$⊢ (x \in B \land (x = A \land φ)) \leftrightarrow (A \in B \land (x = A \land φ))$
6	5	bicomi	$⊢ (A \in B \land (x = A \land φ)) \leftrightarrow (x \in B \land (x = A \land φ))$
7	6	baib	$⊢ x \in B \to ((A \in B \land (x = A \land φ)) \leftrightarrow (x = A \land φ))$
8	7	rexbiia	$⊢ \exists x \in B (A \in B \land (x = A \land φ)) \leftrightarrow \exists x \in B (x = A \land φ)$
9	1	ceqsrexv	$⊢ A \in B \to (\exists x \in B (x = A \land φ) \leftrightarrow ψ)$
10	9	pm5.32i	$⊢ (A \in B \land \exists x \in B (x = A \land φ)) \leftrightarrow (A \in B \land ψ)$
11	2 8 10	3bitr3i	$⊢ \exists x \in B (x = A \land φ) \leftrightarrow (A \in B \land ψ)$

Metamath Proof Explorer