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

Metamath Proof Explorer

Theorem brralrspcev

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

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

Proof

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