Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > op2ndd | Structured version Visualization version Unicode version |
Description: Extract the second member of an ordered pair. (Contributed by Mario Carneiro, 31-Aug-2015.) |
Ref | Expression |
---|---|
op1st.1 | |
op1st.2 |
Ref | Expression |
---|---|
op2ndd |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fveq2 6191 | . 2 | |
2 | op1st.1 | . . 3 | |
3 | op1st.2 | . . 3 | |
4 | 2, 3 | op2nd 7177 | . 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 c2nd 7167 |
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-2nd 7169 |
This theorem is referenced by: 2nd2val 7195 xp2nd 7199 sbcopeq1a 7220 csbopeq1a 7221 eloprabi 7232 mpt2mptsx 7233 dmmpt2ssx 7235 fmpt2x 7236 ovmptss 7258 fmpt2co 7260 df2nd2 7264 frxp 7287 xporderlem 7288 fnwelem 7292 xpf1o 8122 mapunen 8129 xpwdomg 8490 hsmexlem2 9249 nqereu 9751 uzrdgfni 12757 fsumcom2 14505 fsumcom2OLD 14506 fprodcom2 14714 fprodcom2OLD 14715 qredeu 15372 comfeq 16366 isfuncd 16525 cofucl 16548 funcres2b 16557 funcpropd 16560 xpcco2nd 16825 xpccatid 16828 1stf2 16833 2ndf2 16836 1stfcl 16837 2ndfcl 16838 prf2fval 16841 prfcl 16843 evlf2 16858 evlfcl 16862 curf12 16867 curf1cl 16868 curf2 16869 curfcl 16872 hof2fval 16895 hofcl 16899 txbas 21370 cnmpt2nd 21472 txhmeo 21606 ptuncnv 21610 ptunhmeo 21611 xpstopnlem1 21612 xkohmeo 21618 prdstmdd 21927 ucnimalem 22084 fmucndlem 22095 fsum2cn 22674 ovoliunlem1 23270 fcnvgreu 29472 fsumiunle 29575 gsummpt2co 29780 fimaproj 29900 esumiun 30156 eulerpartlemgs2 30442 hgt750lemb 30734 msubrsub 31423 msubco 31428 msubvrs 31457 filnetlem4 32376 finixpnum 33394 poimirlem4 33413 poimirlem15 33424 poimirlem20 33429 poimirlem26 33435 heicant 33444 heiborlem4 33613 heiborlem6 33615 dicelvalN 36467 rmxypairf1o 37476 unxpwdom3 37665 fgraphxp 37789 elcnvlem 37907 dvnprodlem2 40162 etransclem46 40497 ovnsubaddlem1 40784 uspgrsprf 41754 uspgrsprf1 41755 dmmpt2ssx2 42115 lmod1zr 42282 |
Copyright terms: Public domain | W3C validator |