Theorem elopabrOLD

Description: Obsolete version of elopabr as of 11-Dec-2024. (Contributed by AV, 16-Feb-2021) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	elopabrOLD	|- ( 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	imbitrrid	|- ( 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 )