Metamath Proof Explorer

Theorem brimralrspcev

Description: Restricted existential specialization with a restricted universal quantifier over an implication with a relation in the antecedent, closed form. (Contributed by AV, 20-Aug-2022)

		Ref	Expression
	Assertion	brimralrspcev	$⊢ (B \in X \land \forall y \in Y ((φ \land A R B) \to ψ)) \to \exists x \in X \forall y \in Y ((φ \land A R x) \to ψ)$

Proof

Step	Hyp	Ref	Expression
1		breq2	$⊢ x = B \to (A R x \leftrightarrow A R B)$
2	1	anbi2d	$⊢ x = B \to ((φ \land A R x) \leftrightarrow (φ \land A R B))$
3	2	rspceaimv	$⊢ (B \in X \land \forall y \in Y ((φ \land A R B) \to ψ)) \to \exists x \in X \forall y \in Y ((φ \land A R x) \to ψ)$