Theorem elrel

Description: A member of a relation is an ordered pair. (Contributed by NM, 17-Sep-2006)

	Ref	Expression
Assertion	elrel	|- ( ( Rel R /\ A e. R ) -> E. x E. y A = <. x , y >. )

Proof

Step	Hyp	Ref	Expression
1		df-rel	|- ( Rel R <-> R C_ ( _V X. _V ) )
2	1	biimpi	|- ( Rel R -> R C_ ( _V X. _V ) )
3	2	sselda	|- ( ( Rel R /\ A e. R ) -> A e. ( _V X. _V ) )
4		elvv	|- ( A e. ( _V X. _V ) <-> E. x E. y A = <. x , y >. )
5	3 4	sylib	|- ( ( Rel R /\ A e. R ) -> E. x E. y A = <. x , y >. )