Metamath Proof Explorer

Theorem rspceaimv

Description: Restricted existential specialization of a universally quantified implication. (Contributed by BJ, 24-Aug-2022)

		Ref	Expression
	Hypothesis	rspceaimv.1	$⊢ x = A \to (φ \leftrightarrow ψ)$
	Assertion	rspceaimv	$⊢ (A \in B \land \forall y \in C (ψ \to χ)) \to \exists x \in B \forall y \in C (φ \to χ)$

Step	Hyp	Ref	Expression
1		rspceaimv.1	$⊢ x = A \to (φ \leftrightarrow ψ)$
2	1	imbi1d	$⊢ x = A \to ((φ \to χ) \leftrightarrow (ψ \to χ))$
3	2	ralbidv	$⊢ x = A \to (\forall y \in C (φ \to χ) \leftrightarrow \forall y \in C (ψ \to χ))$
4	3	rspcev	$⊢ (A \in B \land \forall y \in C (ψ \to χ)) \to \exists x \in B \forall y \in C (φ \to χ)$