![]() |
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 6888 | . 2 ⊢ (𝐶 = 〈𝐴, 𝐵〉 → (2nd ‘𝐶) = (2nd ‘〈𝐴, 𝐵〉)) | |
2 | op1st.1 | . . 3 ⊢ 𝐴 ∈ V | |
3 | op1st.2 | . . 3 ⊢ 𝐵 ∈ V | |
4 | 2, 3 | op2nd 7979 | . 2 ⊢ (2nd ‘〈𝐴, 𝐵〉) = 𝐵 |
5 | 1, 4 | eqtrdi 2789 | 1 ⊢ (𝐶 = 〈𝐴, 𝐵〉 → (2nd ‘𝐶) = 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1542 ∈ wcel 2107 Vcvv 3475 〈cop 4633 ‘cfv 6540 2nd c2nd 7969 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2704 ax-sep 5298 ax-nul 5305 ax-pr 5426 ax-un 7720 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2535 df-eu 2564 df-clab 2711 df-cleq 2725 df-clel 2811 df-nfc 2886 df-ral 3063 df-rex 3072 df-rab 3434 df-v 3477 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-nul 4322 df-if 4528 df-sn 4628 df-pr 4630 df-op 4634 df-uni 4908 df-br 5148 df-opab 5210 df-mpt 5231 df-id 5573 df-xp 5681 df-rel 5682 df-cnv 5683 df-co 5684 df-dm 5685 df-rn 5686 df-iota 6492 df-fun 6542 df-fv 6548 df-2nd 7971 |
This theorem is referenced by: 2nd2val 7999 xp2nd 8003 sbcopeq1a 8030 csbopeq1a 8031 eloprabi 8044 mpomptsx 8045 dmmpossx 8047 fmpox 8048 ovmptss 8074 fmpoco 8076 df2nd2 8080 frxp 8107 xporderlem 8108 fnwelem 8112 fimaproj 8116 xpord2lem 8123 naddcllem 8671 xpf1o 9135 mapunen 9142 xpwdomg 9576 hsmexlem2 10418 nqereu 10920 uzrdgfni 13919 fsumcom2 15716 fprodcom2 15924 qredeu 16591 comfeq 17646 isfuncd 17811 cofucl 17834 funcres2b 17843 funcpropd 17847 xpcco2nd 18133 xpccatid 18136 1stf2 18141 2ndf2 18144 1stfcl 18145 2ndfcl 18146 prf2fval 18149 prfcl 18151 evlf2 18167 evlfcl 18171 curf12 18176 curf1cl 18177 curf2 18178 curfcl 18181 hof2fval 18204 hofcl 18208 txbas 23053 cnmpt2nd 23155 txhmeo 23289 ptuncnv 23293 ptunhmeo 23294 xpstopnlem1 23295 xkohmeo 23301 prdstmdd 23610 ucnimalem 23767 fmucndlem 23778 fsum2cn 24369 ovoliunlem1 25001 2sqreuop 26945 2sqreuopnn 26946 2sqreuoplt 26947 2sqreuopltb 26948 2sqreuopnnlt 26949 2sqreuopnnltb 26950 wlkl0 29600 fcnvgreu 31876 fsumiunle 32013 gsummpt2co 32178 gsumhashmul 32186 esumiun 33030 eulerpartlemgs2 33317 hgt750lemb 33606 satfv1 34292 satefvfmla0 34347 msubrsub 34455 msubco 34460 msubvrs 34489 filnetlem4 35204 finixpnum 36411 poimirlem4 36430 poimirlem15 36441 poimirlem20 36446 poimirlem26 36452 heicant 36461 heiborlem4 36620 heiborlem6 36622 dicelvalN 39987 aks6d1c2p1 40894 fmpocos 41005 rmxypairf1o 41583 unxpwdom3 41770 fgraphxp 41886 elcnvlem 42285 dvnprodlem2 44598 etransclem46 44931 ovnsubaddlem1 45221 uspgrsprf 46459 uspgrsprf1 46460 dmmpossx2 46914 lmod1zr 47076 2arymaptf 47240 rrx2plordisom 47311 funcf2lem 47540 |
Copyright terms: Public domain | W3C validator |