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 φAV
opeldmd.2 φBW
Assertion opeldmd φABCAdomC

Proof

Step Hyp Ref Expression
1 opeldmd.1 φAV
2 opeldmd.2 φBW
3 opeq2 y=BAy=AB
4 3 eleq1d y=BAyCABC
5 4 spcegv BWABCyAyC
6 2 5 syl φABCyAyC
7 eldm2g AVAdomCyAyC
8 1 7 syl φAdomCyAyC
9 6 8 sylibrd φABCAdomC