Theorem opeldm

Description: Membership of first of an ordered pair in a domain. (Contributed by NM, 30-Jul-1995)

	Ref	Expression
Hypotheses	opeldm.1	|- A e. _V
	opeldm.2	|- B e. _V
Assertion	opeldm	|- ( <. A , B >. e. C -> A e. dom C )

Proof

Step	Hyp	Ref	Expression
1		opeldm.1	|- A e. _V
2		opeldm.2	|- B e. _V
3		opeq2	|- ( y = B -> <. A , y >. = <. A , B >. )
4	3	eleq1d	|- ( y = B -> ( <. A , y >. e. C <-> <. A , B >. e. C ) )
5	2 4	spcev	|- ( <. A , B >. e. C -> E. y <. A , y >. e. C )
6	1	eldm2	|- ( A e. dom C <-> E. y <. A , y >. e. C )
7	5 6	sylibr	|- ( <. A , B >. e. C -> A e. dom C )