![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > op1st | Structured version Visualization version Unicode version |
Description: Extract the first member of an ordered pair. (Contributed by NM, 5-Oct-2004.) |
Ref | Expression |
---|---|
op1st.1 |
![]() ![]() ![]() ![]() |
op1st.2 |
![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
op1st |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 1stval 6792 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | op1st.1 |
. . 3
![]() ![]() ![]() ![]() | |
3 | op1st.2 |
. . 3
![]() ![]() ![]() ![]() | |
4 | 2, 3 | op1sta 5317 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 1, 4 | eqtri 2472 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1668 ax-4 1681 ax-5 1757 ax-6 1804 ax-7 1850 ax-8 1888 ax-9 1895 ax-10 1914 ax-11 1919 ax-12 1932 ax-13 2090 ax-ext 2430 ax-sep 4524 ax-nul 4533 ax-pow 4580 ax-pr 4638 ax-un 6580 |
This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3an 986 df-tru 1446 df-ex 1663 df-nf 1667 df-sb 1797 df-eu 2302 df-mo 2303 df-clab 2437 df-cleq 2443 df-clel 2446 df-nfc 2580 df-ne 2623 df-ral 2741 df-rex 2742 df-rab 2745 df-v 3046 df-sbc 3267 df-dif 3406 df-un 3408 df-in 3410 df-ss 3417 df-nul 3731 df-if 3881 df-sn 3968 df-pr 3970 df-op 3974 df-uni 4198 df-br 4402 df-opab 4461 df-mpt 4462 df-id 4748 df-xp 4839 df-rel 4840 df-cnv 4841 df-co 4842 df-dm 4843 df-rn 4844 df-iota 5545 df-fun 5583 df-fv 5589 df-1st 6790 |
This theorem is referenced by: op1std 6800 op1stg 6802 1stval2 6807 fo1stres 6814 eloprabi 6852 algrflem 6902 xpmapenlem 7736 fseqenlem2 8453 archnq 9402 ruclem8 14282 idfu1st 15777 cofu1st 15781 xpccatid 16066 prf1st 16082 yonedalem21 16151 yonedalem22 16156 2ndcctbss 20463 upxp 20631 uptx 20633 cnheiborlem 21975 ovollb2lem 22434 ovolctb 22436 ovoliunlem2 22449 ovolshftlem1 22455 ovolscalem1 22459 ovolicc1 22462 usgraexmplvtx 25123 wlknwwlknsur 25433 wlkiswwlksur 25440 clwlkfoclwwlk 25566 ex-1st 25887 cnnvg 26302 cnnvs 26305 h2hva 26620 h2hsm 26621 hhssva 26903 hhsssm 26904 hhshsslem1 26911 eulerpartlemgvv 29202 eulerpartlemgh 29204 br1steq 30407 filnetlem3 31029 poimirlem17 31950 heiborlem8 32143 dvhvaddass 34659 dvhlveclem 34670 diblss 34732 pellexlem5 35671 pellex 35673 dvnprodlem1 37815 hoicvr 38364 hoicvrrex 38372 ovn0lem 38381 ovnhoilem1 38417 vtxvalsnop 39127 usgfis 39745 usgfisALT 39749 |
Copyright terms: Public domain | W3C validator |