Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > op2ndd | Structured version Visualization version GIF version |
Description: Extract the second member of an ordered pair. (Contributed by Mario Carneiro, 31-Aug-2015.) |
Ref | Expression |
---|---|
op1st.1 | ⊢ 𝐴 ∈ V |
op1st.2 | ⊢ 𝐵 ∈ V |
Ref | Expression |
---|---|
op2ndd | ⊢ (𝐶 = 〈𝐴, 𝐵〉 → (2nd ‘𝐶) = 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fveq2 6663 | . 2 ⊢ (𝐶 = 〈𝐴, 𝐵〉 → (2nd ‘𝐶) = (2nd ‘〈𝐴, 𝐵〉)) | |
2 | op1st.1 | . . 3 ⊢ 𝐴 ∈ V | |
3 | op1st.2 | . . 3 ⊢ 𝐵 ∈ V | |
4 | 2, 3 | op2nd 7690 | . 2 ⊢ (2nd ‘〈𝐴, 𝐵〉) = 𝐵 |
5 | 1, 4 | syl6eq 2870 | 1 ⊢ (𝐶 = 〈𝐴, 𝐵〉 → (2nd ‘𝐶) = 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1531 ∈ wcel 2108 Vcvv 3493 〈cop 4565 ‘cfv 6348 2nd c2nd 7680 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1905 ax-6 1964 ax-7 2009 ax-8 2110 ax-9 2118 ax-10 2139 ax-11 2154 ax-12 2170 ax-ext 2791 ax-sep 5194 ax-nul 5201 ax-pow 5257 ax-pr 5320 ax-un 7453 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3an 1084 df-tru 1534 df-ex 1775 df-nf 1779 df-sb 2064 df-mo 2616 df-eu 2648 df-clab 2798 df-cleq 2812 df-clel 2891 df-nfc 2961 df-ral 3141 df-rex 3142 df-rab 3145 df-v 3495 df-sbc 3771 df-dif 3937 df-un 3939 df-in 3941 df-ss 3950 df-nul 4290 df-if 4466 df-sn 4560 df-pr 4562 df-op 4566 df-uni 4831 df-br 5058 df-opab 5120 df-mpt 5138 df-id 5453 df-xp 5554 df-rel 5555 df-cnv 5556 df-co 5557 df-dm 5558 df-rn 5559 df-iota 6307 df-fun 6350 df-fv 6356 df-2nd 7682 |
This theorem is referenced by: 2nd2val 7710 xp2nd 7714 sbcopeq1a 7740 csbopeq1a 7741 eloprabi 7753 mpomptsx 7754 dmmpossx 7756 fmpox 7757 ovmptss 7780 fmpoco 7782 df2nd2 7786 frxp 7812 xporderlem 7813 fnwelem 7817 fimaproj 7821 xpf1o 8671 mapunen 8678 xpwdomg 9041 hsmexlem2 9841 nqereu 10343 uzrdgfni 13318 fsumcom2 15121 fprodcom2 15330 qredeu 15994 comfeq 16968 isfuncd 17127 cofucl 17150 funcres2b 17159 funcpropd 17162 xpcco2nd 17427 xpccatid 17430 1stf2 17435 2ndf2 17438 1stfcl 17439 2ndfcl 17440 prf2fval 17443 prfcl 17445 evlf2 17460 evlfcl 17464 curf12 17469 curf1cl 17470 curf2 17471 curfcl 17474 hof2fval 17497 hofcl 17501 txbas 22167 cnmpt2nd 22269 txhmeo 22403 ptuncnv 22407 ptunhmeo 22408 xpstopnlem1 22409 xkohmeo 22415 prdstmdd 22724 ucnimalem 22881 fmucndlem 22892 fsum2cn 23471 ovoliunlem1 24095 2sqreuop 26030 2sqreuopnn 26031 2sqreuoplt 26032 2sqreuopltb 26033 2sqreuopnnlt 26034 2sqreuopnnltb 26035 wlkl0 28138 fcnvgreu 30410 fsumiunle 30538 gsummpt2co 30679 esumiun 31346 eulerpartlemgs2 31631 hgt750lemb 31920 satfv1 32603 satefvfmla0 32658 msubrsub 32766 msubco 32771 msubvrs 32800 filnetlem4 33722 finixpnum 34869 poimirlem4 34888 poimirlem15 34899 poimirlem20 34904 poimirlem26 34910 heicant 34919 heiborlem4 35084 heiborlem6 35086 dicelvalN 38306 rmxypairf1o 39499 unxpwdom3 39686 fgraphxp 39802 elcnvlem 39952 dvnprodlem2 42222 etransclem46 42556 ovnsubaddlem1 42843 uspgrsprf 44012 uspgrsprf1 44013 dmmpossx2 44376 lmod1zr 44539 rrx2plordisom 44701 |
Copyright terms: Public domain | W3C validator |