Metamath Proof Explorer

Theorem rspce

Description: Restricted existential specialization, using implicit substitution. (Contributed by NM, 26-May-1998) (Revised by Mario Carneiro, 11-Oct-2016)

		Ref	Expression
	Hypotheses	rspc.1	$⊢ Ⅎ x ψ$
		rspc.2	$⊢ x = A \to (φ \leftrightarrow ψ)$
	Assertion	rspce	$⊢ (A \in B \land ψ) \to \exists x \in B φ$

Proof

Step	Hyp	Ref	Expression
1		rspc.1	$⊢ Ⅎ x ψ$
2		rspc.2	$⊢ x = A \to (φ \leftrightarrow ψ)$
3		nfcv	$⊢ \underline{Ⅎ} x A$
4		nfv	$⊢ Ⅎ x A \in B$
5	4 1	nfan	$⊢ Ⅎ x (A \in B \land ψ)$
6		eleq1	$⊢ x = A \to (x \in B \leftrightarrow A \in B)$
7	6 2	anbi12d	$⊢ x = A \to ((x \in B \land φ) \leftrightarrow (A \in B \land ψ))$
8	3 5 7	spcegf	$⊢ A \in B \to ((A \in B \land ψ) \to \exists x (x \in B \land φ))$
9	8	anabsi5	$⊢ (A \in B \land ψ) \to \exists x (x \in B \land φ)$
10		df-rex	$⊢ \exists x \in B φ \leftrightarrow \exists x (x \in B \land φ)$
11	9 10	sylibr	$⊢ (A \in B \land ψ) \to \exists x \in B φ$