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

Metamath Proof Explorer

Theorem rspcdf

Description: Restricted specialization, using implicit substitution. (Contributed by Emmett Weisz, 16-Jan-2020)

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

Step	Hyp	Ref	Expression
1		rspcdf.1	$⊢ Ⅎ x φ$
2		rspcdf.2	$⊢ Ⅎ x χ$
3		rspcdf.3	$⊢ φ \to A \in B$
4		rspcdf.4	$⊢ (φ \land x = A) \to (ψ \leftrightarrow χ)$
5	4	ex	$⊢ φ \to (x = A \to (ψ \leftrightarrow χ))$
6	1 5	alrimi	$⊢ φ \to \forall x (x = A \to (ψ \leftrightarrow χ))$
7	2	rspct	$⊢ \forall x (x = A \to (ψ \leftrightarrow χ)) \to (A \in B \to (\forall x \in B ψ \to χ))$
8	6 3 7	sylc	$⊢ φ \to (\forall x \in B ψ \to χ)$