Metamath Proof Explorer

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 V
opeldm.2 B V
Assertion opeldm A B C A dom C


Step Hyp Ref Expression
1 opeldm.1 A V
2 opeldm.2 B V
3 opeq2 y = B A y = A B
4 3 eleq1d y = B A y C A B C
5 2 4 spcev A B C y A y C
6 1 eldm2 A dom C y A y C
7 5 6 sylibr A B C A dom C