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

Proof

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