![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > op1st | Structured version Visualization version GIF version |
Description: Extract the first member of an ordered pair. (Contributed by NM, 5-Oct-2004.) |
Ref | Expression |
---|---|
op1st.1 | ⊢ 𝐴 ∈ V |
op1st.2 | ⊢ 𝐵 ∈ V |
Ref | Expression |
---|---|
op1st | ⊢ (1st ‘〈𝐴, 𝐵〉) = 𝐴 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 1stval 8014 | . 2 ⊢ (1st ‘〈𝐴, 𝐵〉) = ∪ dom {〈𝐴, 𝐵〉} | |
2 | op1st.1 | . . 3 ⊢ 𝐴 ∈ V | |
3 | op1st.2 | . . 3 ⊢ 𝐵 ∈ V | |
4 | 2, 3 | op1sta 6246 | . 2 ⊢ ∪ dom {〈𝐴, 𝐵〉} = 𝐴 |
5 | 1, 4 | eqtri 2762 | 1 ⊢ (1st ‘〈𝐴, 𝐵〉) = 𝐴 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1536 ∈ wcel 2105 Vcvv 3477 {csn 4630 〈cop 4636 ∪ cuni 4911 dom cdm 5688 ‘cfv 6562 1st c1st 8010 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1791 ax-4 1805 ax-5 1907 ax-6 1964 ax-7 2004 ax-8 2107 ax-9 2115 ax-10 2138 ax-11 2154 ax-12 2174 ax-ext 2705 ax-sep 5301 ax-nul 5311 ax-pr 5437 ax-un 7753 |
This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1539 df-fal 1549 df-ex 1776 df-nf 1780 df-sb 2062 df-mo 2537 df-eu 2566 df-clab 2712 df-cleq 2726 df-clel 2813 df-nfc 2889 df-ral 3059 df-rex 3068 df-rab 3433 df-v 3479 df-dif 3965 df-un 3967 df-in 3969 df-ss 3979 df-nul 4339 df-if 4531 df-sn 4631 df-pr 4633 df-op 4637 df-uni 4912 df-br 5148 df-opab 5210 df-mpt 5231 df-id 5582 df-xp 5694 df-rel 5695 df-cnv 5696 df-co 5697 df-dm 5698 df-rn 5699 df-iota 6515 df-fun 6564 df-fv 6570 df-1st 8012 |
This theorem is referenced by: op1std 8022 op1stg 8024 1stval2 8029 fo1stres 8038 opreuopreu 8057 eloprabi 8086 xpmapenlem 9182 fseqenlem2 10062 archnq 11017 ruclem8 16269 idfu1st 17929 cofu1st 17933 xpccatid 18243 prf1st 18259 yonedalem21 18329 yonedalem22 18334 2ndcctbss 23478 upxp 23646 uptx 23648 cnheiborlem 24999 ovollb2lem 25536 ovolctb 25538 ovoliunlem2 25551 ovolshftlem1 25557 ovolscalem1 25561 ovolicc1 25564 addsqnreup 27501 2sqreuop 27520 2sqreuopnn 27521 2sqreuoplt 27522 2sqreuopltb 27523 2sqreuopnnlt 27524 2sqreuopnnltb 27525 precsexlem1 28245 precsexlem4 28248 ex-1st 30472 cnnvg 30706 cnnvs 30708 h2hva 31002 h2hsm 31003 hhssva 31285 hhsssm 31286 hhshsslem1 31295 gsumhashmul 33046 rlocf1 33259 fracfld 33289 eulerpartlemgvv 34357 eulerpartlemgh 34359 satfv0fvfmla0 35397 filnetlem3 36362 poimirlem17 37623 heiborlem8 37804 dvhvaddass 41079 dvhlveclem 41090 diblss 41152 aks6d1c3 42104 pellexlem5 42820 pellex 42822 dvnprodlem1 45901 hoicvr 46503 hoicvrrex 46511 ovn0lem 46520 ovnhoilem1 46556 gpgedgvtx0 47953 gpgedgvtx1 47954 thincciso 48848 |
Copyright terms: Public domain | W3C validator |