Theorem opeldmd

Description: Membership of first of an ordered pair in a domain. Deduction version of opeldm . (Contributed by AV, 11-Mar-2021)

	Ref	Expression
Hypotheses	opeldmd.1	|- ( ph -> A e. V )
	opeldmd.2	|- ( ph -> B e. W )
Assertion	opeldmd	|- ( ph -> ( <. A , B >. e. C -> A e. dom C ) )

Proof

Step	Hyp	Ref	Expression
1		opeldmd.1	|- ( ph -> A e. V )
2		opeldmd.2	|- ( ph -> B e. W )
3		opeq2	|- ( y = B -> <. A , y >. = <. A , B >. )
4	3	eleq1d	|- ( y = B -> ( <. A , y >. e. C <-> <. A , B >. e. C ) )
5	4	spcegv	|- ( B e. W -> ( <. A , B >. e. C -> E. y <. A , y >. e. C ) )
6	2 5	syl	|- ( ph -> ( <. A , B >. e. C -> E. y <. A , y >. e. C ) )
7		eldm2g	|- ( A e. V -> ( A e. dom C <-> E. y <. A , y >. e. C ) )
8	1 7	syl	|- ( ph -> ( A e. dom C <-> E. y <. A , y >. e. C ) )
9	6 8	sylibrd	|- ( ph -> ( <. A , B >. e. C -> A e. dom C ) )