This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )