| 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 3159 |
. . . . 5
| |
| 2 | 1 | eleq1d 1963 |
. . . 4
|
| 3 | 2 | cla4egv 2365 |
. . 3
|
| 4 | opeldm.1 |
. . . 4
| |
| 5 | 4 | eldm2 4154 |
. . 3
|
| 6 | 3, 5 | syl6ibr 230 |
. 2
|
| 7 | opprc2 3171 |
. . . 4
| |
| 8 | 7 | eleq1d 1963 |
. . 3
|
| 9 | opeq2 3159 |
. . . . . 6
| |
| 10 | 9 | eleq1d 1963 |
. . . . 5
|
| 11 | 4, 10 | cla4ev 2371 |
. . . 4
|
| 12 | 11, 5 | sylibr 217 |
. . 3
|
| 13 | 8, 12 | syl6bi 231 |
. 2
|
| 14 | 6, 13 | pm2.61i 140 |
1
|
| Colors of variables: wff set class |
| Syntax hints: |
| This theorem is referenced by: breldm 4161 elreldm 4185 relssres 4248 iss 4254 imadmrn 4277 dfco2a 4394 funssres 4460 funun 4462 fnrnfv 4718 eqfnfv 4766 tz7.48-1 5165 ecopoprdm 5368 bnj1379 13100 |
| This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 1304 ax-gen 1305 ax-8 1306 ax-9 1307 ax-10 1308 ax-11 1309 ax-12 1310 ax-17 1317 ax-4 1319 ax-5o 1321 ax-6o 1324 ax-9o 1481 ax-10o 1500 ax-16 1580 ax-11o 1588 ax-ext 1865 |
| This theorem depends on definitions: df-bi 164 df-or 241 df-an 242 df-ex 1327 df-sb 1536 df-clab 1872 df-cleq 1877 df-clel 1880 df-ne 2019 df-v 2294 df-dif 2597 df-un 2600 df-nul 2876 df-sn 3049 df-pr 3050 df-op 3053 df-br 3339 df-dm 4004 |