Theorem 1stdm

Description: The first ordered pair component of a member of a relation belongs to the domain of the relation. (Contributed by NM, 17-Sep-2006)

	Ref	Expression
Assertion	1stdm	|- ( ( Rel R /\ A e. R ) -> ( 1st ` A ) e. dom R )

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		1stval2	|- ( A e. ( _V X. _V ) -> ( 1st ` A ) = |^| |^| A )
5	3 4	syl	|- ( ( Rel R /\ A e. R ) -> ( 1st ` A ) = |^| |^| A )
6		elreldm	|- ( ( Rel R /\ A e. R ) -> |^| |^| A e. dom R )
7	5 6	eqeltrd	|- ( ( Rel R /\ A e. R ) -> ( 1st ` A ) e. dom R )