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 e. X /\ A. y e. Y A R B ) -> E. x e. X A. y e. Y A R x )

Proof

Step	Hyp	Ref	Expression
1		breq2	|- ( x = B -> ( A R x <-> A R B ) )
2	1	ralbidv	|- ( x = B -> ( A. y e. Y A R x <-> A. y e. Y A R B ) )
3	2	rspcev	|- ( ( B e. X /\ A. y e. Y A R B ) -> E. x e. X A. y e. Y A R x )