| Metamath Proof Explorer |
< Previous
Next >
Related theorems Unicode version |
| Description: Membership of first of an ordered pair in a domain. |
| Ref | Expression |
|---|---|
| opeldm.1 |
|
| Ref | Expression |
|---|---|
| opeldm |
|
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | opeq2 2542 |
. . . . 5
| |
| 2 | 1 | eleq1d 1587 |
. . . 4
|
| 3 | 2 | cla4egv 1910 |
. . 3
|
| 4 | opeldm.1 |
. . . 4
| |
| 5 | 4 | eldm2 3365 |
. . 3
|
| 6 | 3, 5 | syl6ibr 220 |
. 2
|
| 7 | opprc2 2553 |
. . . 4
| |
| 8 | 7 | eleq1d 1587 |
. . 3
|
| 9 | opeq2 2542 |
. . . . . 6
| |
| 10 | 9 | eleq1d 1587 |
. . . . 5
|
| 11 | 4, 10 | cla4ev 1916 |
. . . 4
|
| 12 | 11, 5 | sylibr 207 |
. . 3
|
| 13 | 8, 12 | syl6bi 221 |
. 2
|
| 14 | 6, 13 | pm2.61i 132 |
1
|
| Colors of variables: wff set class |
| Syntax hints: |
| This theorem is referenced by: breldm 3372 elreldm 3395 relssres 3449 imadmrn 3471 funssres 3609 funun 3611 fnrnfv 3816 eqfnfv 3854 tz7.48-1 4014 ecopoprdm 4370 domintreflem 10562 domintref 10563 |
| This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 1003 ax-gen 1004 ax-8 1005 ax-10 1007 ax-12 1009 ax-17 1012 ax-4 1014 ax-5o 1016 ax-6o 1019 ax-9o 1164 ax-10o 1182 ax-16 1252 ax-11o 1260 ax-ext 1504 |
| This theorem depends on definitions: df-bi 154 df-or 231 df-an 232 df-ex 1022 df-sb 1214 df-clab 1510 df-cleq 1515 df-clel 1518 df-ne 1634 df-v 1859 df-dif 2100 df-un 2101 df-nul 2332 df-sn 2464 df-pr 2465 df-op 2468 df-br 2675 df-dm 3245 |