Theorem elopabr

Description: Membership in an ordered-pair class abstraction defined by a binary relation. (Contributed by AV, 16-Feb-2021)

	Ref	Expression
Assertion	elopabr	|- ( A e. { <. x , y >. | x R y } -> A e. R )

Proof

Step	Hyp	Ref	Expression
1		elopab	|- ( A e. { <. x , y >. | x R y } <-> E. x E. y ( A = <. x , y >. /\ x R y ) )
2		df-br	|- ( x R y <-> <. x , y >. e. R )
3	2	biimpi	|- ( x R y -> <. x , y >. e. R )
4		eleq1	|- ( A = <. x , y >. -> ( A e. R <-> <. x , y >. e. R ) )
5	3 4	syl5ibr	|- ( A = <. x , y >. -> ( x R y -> A e. R ) )
6	5	imp	|- ( ( A = <. x , y >. /\ x R y ) -> A e. R )
7	6	exlimivv	|- ( E. x E. y ( A = <. x , y >. /\ x R y ) -> A e. R )
8	1 7	sylbi	|- ( A e. { <. x , y >. | x R y } -> A e. R )