This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem rspcedvd

Description: Restricted existential specialization, using implicit substitution. Variant of rspcedv . (Contributed by AV, 27-Nov-2019)

	Ref	Expression
Hypotheses	rspcedvd.1	$⊢ φ \to A \in B$
	rspcedvd.2	$⊢ (φ \land x = A) \to (ψ \leftrightarrow χ)$
	rspcedvd.3	$⊢ φ \to χ$
Assertion	rspcedvd	$⊢ φ \to \exists x \in B ψ$

Step	Hyp	Ref	Expression
1		rspcedvd.1	$⊢ φ \to A \in B$
2		rspcedvd.2	$⊢ (φ \land x = A) \to (ψ \leftrightarrow χ)$
3		rspcedvd.3	$⊢ φ \to χ$
4	1 2	rspcedv	$⊢ φ \to (χ \to \exists x \in B ψ)$
5	3 4	mpd	$⊢ φ \to \exists x \in B ψ$