Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > op1std | Structured version Visualization version Unicode version |
Description: Extract the first member of an ordered pair. (Contributed by Mario Carneiro, 31-Aug-2015.) |
Ref | Expression |
---|---|
op1st.1 | |
op1st.2 |
Ref | Expression |
---|---|
op1std |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fveq2 6191 | . 2 | |
2 | op1st.1 | . . 3 | |
3 | op1st.2 | . . 3 | |
4 | 2, 3 | op1st 7176 | . 2 |
5 | 1, 4 | syl6eq 2672 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wceq 1483 wcel 1990 cvv 3200 cop 4183 cfv 5888 c1st 7166 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ral 2917 df-rex 2918 df-rab 2921 df-v 3202 df-sbc 3436 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-nul 3916 df-if 4087 df-sn 4178 df-pr 4180 df-op 4184 df-uni 4437 df-br 4654 df-opab 4713 df-mpt 4730 df-id 5024 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-iota 5851 df-fun 5890 df-fv 5896 df-1st 7168 |
This theorem is referenced by: 1st2val 7194 xp1st 7198 sbcopeq1a 7220 csbopeq1a 7221 eloprabi 7232 mpt2mptsx 7233 dmmpt2ssx 7235 fmpt2x 7236 ovmptss 7258 fmpt2co 7260 df1st2 7263 fsplit 7282 frxp 7287 xporderlem 7288 fnwelem 7292 xpf1o 8122 mapunen 8129 xpwdomg 8490 hsmexlem2 9249 fsumcom2 14505 fsumcom2OLD 14506 fprodcom2 14714 fprodcom2OLD 14715 qredeu 15372 isfuncd 16525 cofucl 16548 funcres2b 16557 funcpropd 16560 xpcco1st 16824 xpccatid 16828 1stf1 16832 2ndf1 16835 1stfcl 16837 prf1 16840 prfcl 16843 prf1st 16844 prf2nd 16845 evlf1 16860 evlfcl 16862 curf1fval 16864 curf11 16866 curf1cl 16868 curfcl 16872 hof1fval 16893 txbas 21370 cnmpt1st 21471 txhmeo 21606 ptuncnv 21610 ptunhmeo 21611 xpstopnlem1 21612 xkohmeo 21618 prdstmdd 21927 ucnimalem 22084 fmucndlem 22095 fsum2cn 22674 ovoliunlem1 23270 lgsquadlem1 25105 lgsquadlem2 25106 fimaproj 29900 eulerpartlemgs2 30442 hgt750lemb 30734 cvmliftlem15 31280 msubty 31424 msubco 31428 msubvrs 31457 filnetlem4 32376 finixpnum 33394 poimirlem4 33413 poimirlem15 33424 poimirlem20 33429 poimirlem26 33435 poimirlem28 33437 heicant 33444 dicelvalN 36467 rmxypairf1o 37476 unxpwdom3 37665 fgraphxp 37789 elcnvlem 37907 dvnprodlem2 40162 etransclem46 40497 ovnsubaddlem1 40784 dmmpt2ssx2 42115 |
Copyright terms: Public domain | W3C validator |