![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > op2nd | Structured version Visualization version GIF version |
Description: Extract the second member of an ordered pair. (Contributed by NM, 5-Oct-2004.) |
Ref | Expression |
---|---|
op1st.1 | ⊢ 𝐴 ∈ V |
op1st.2 | ⊢ 𝐵 ∈ V |
Ref | Expression |
---|---|
op2nd | ⊢ (2nd ‘〈𝐴, 𝐵〉) = 𝐵 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 2ndval 7503 | . 2 ⊢ (2nd ‘〈𝐴, 𝐵〉) = ∪ ran {〈𝐴, 𝐵〉} | |
2 | op1st.1 | . . 3 ⊢ 𝐴 ∈ V | |
3 | op1st.2 | . . 3 ⊢ 𝐵 ∈ V | |
4 | 2, 3 | op2nda 5922 | . 2 ⊢ ∪ ran {〈𝐴, 𝐵〉} = 𝐵 |
5 | 1, 4 | eqtri 2797 | 1 ⊢ (2nd ‘〈𝐴, 𝐵〉) = 𝐵 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1508 ∈ wcel 2051 Vcvv 3410 {csn 4436 〈cop 4442 ∪ cuni 4709 ran crn 5405 ‘cfv 6186 2nd c2nd 7499 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1759 ax-4 1773 ax-5 1870 ax-6 1929 ax-7 1966 ax-8 2053 ax-9 2060 ax-10 2080 ax-11 2094 ax-12 2107 ax-13 2302 ax-ext 2745 ax-sep 5057 ax-nul 5064 ax-pow 5116 ax-pr 5183 ax-un 7278 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 835 df-3an 1071 df-tru 1511 df-ex 1744 df-nf 1748 df-sb 2017 df-mo 2548 df-eu 2585 df-clab 2754 df-cleq 2766 df-clel 2841 df-nfc 2913 df-ral 3088 df-rex 3089 df-rab 3092 df-v 3412 df-sbc 3677 df-dif 3827 df-un 3829 df-in 3831 df-ss 3838 df-nul 4174 df-if 4346 df-sn 4437 df-pr 4439 df-op 4443 df-uni 4710 df-br 4927 df-opab 4989 df-mpt 5006 df-id 5309 df-xp 5410 df-rel 5411 df-cnv 5412 df-co 5413 df-dm 5414 df-rn 5415 df-iota 6150 df-fun 6188 df-fv 6194 df-2nd 7501 |
This theorem is referenced by: op2ndd 7511 op2ndg 7513 2ndval2 7518 fo2ndres 7527 opreuopreu 7545 eloprabi 7568 fo2ndf 7621 f1o2ndf1 7622 seqomlem1 7888 seqomlem2 7889 xpmapenlem 8479 fseqenlem2 9244 axdc4lem 9674 iunfo 9758 archnq 10199 om2uzrdg 13138 uzrdgsuci 13142 fsum2dlem 14984 fprod2dlem 15193 ruclem8 15449 ruclem11 15452 eucalglt 15784 idfu2nd 17018 idfucl 17022 cofu2nd 17026 cofucl 17029 xpccatid 17309 prf2nd 17326 curf2ndf 17368 yonedalem22 17399 gaid 18213 2ndcctbss 21783 upxp 21951 uptx 21953 txkgen 21980 cnheiborlem 23277 ovollb2lem 23808 ovolctb 23810 ovoliunlem2 23823 ovolshftlem1 23829 ovolscalem1 23833 ovolicc1 23836 addsqnreup 25737 2sqreuop 25756 2sqreuopnn 25757 2sqreuoplt 25758 2sqreuopltb 25759 2sqreuopnnlt 25760 2sqreuopnnltb 25761 wlkswwlksf1o 27381 clwlkclwwlkfoOLD 27535 clwlkclwwlkfo 27539 ex-2nd 28018 cnnvs 28250 cnnvnm 28251 h2hsm 28547 h2hnm 28548 hhsssm 28830 hhssnm 28831 aciunf1lem 30187 eulerpartlemgvv 31312 eulerpartlemgh 31314 msubff1 32356 msubvrs 32360 poimirlem17 34383 heiborlem7 34570 heiborlem8 34571 dvhvaddass 37711 dvhlveclem 37722 diblss 37784 pellexlem5 38860 pellex 38862 dvnprodlem1 41691 hoicvr 42291 hoicvrrex 42299 ovn0lem 42308 ovnhoilem1 42344 ovnlecvr2 42353 ovolval5lem2 42396 |
Copyright terms: Public domain | W3C validator |