![]() |
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 7989 | . 2 ⊢ (1st ‘〈𝐴, 𝐵〉) = ∪ dom {〈𝐴, 𝐵〉} | |
2 | op1st.1 | . . 3 ⊢ 𝐴 ∈ V | |
3 | op1st.2 | . . 3 ⊢ 𝐵 ∈ V | |
4 | 2, 3 | op1sta 6223 | . 2 ⊢ ∪ dom {〈𝐴, 𝐵〉} = 𝐴 |
5 | 1, 4 | eqtri 2755 | 1 ⊢ (1st ‘〈𝐴, 𝐵〉) = 𝐴 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1534 ∈ wcel 2099 Vcvv 3469 {csn 4624 〈cop 4630 ∪ cuni 4903 dom cdm 5672 ‘cfv 6542 1st c1st 7985 |
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 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-10 2130 ax-11 2147 ax-12 2164 ax-ext 2698 ax-sep 5293 ax-nul 5300 ax-pr 5423 ax-un 7734 |
This theorem depends on definitions: df-bi 206 df-an 396 df-or 847 df-3an 1087 df-tru 1537 df-fal 1547 df-ex 1775 df-nf 1779 df-sb 2061 df-mo 2529 df-eu 2558 df-clab 2705 df-cleq 2719 df-clel 2805 df-nfc 2880 df-ral 3057 df-rex 3066 df-rab 3428 df-v 3471 df-dif 3947 df-un 3949 df-in 3951 df-ss 3961 df-nul 4319 df-if 4525 df-sn 4625 df-pr 4627 df-op 4631 df-uni 4904 df-br 5143 df-opab 5205 df-mpt 5226 df-id 5570 df-xp 5678 df-rel 5679 df-cnv 5680 df-co 5681 df-dm 5682 df-rn 5683 df-iota 6494 df-fun 6544 df-fv 6550 df-1st 7987 |
This theorem is referenced by: op1std 7997 op1stg 7999 1stval2 8004 fo1stres 8013 opreuopreu 8032 eloprabi 8061 xpmapenlem 9160 fseqenlem2 10040 archnq 10995 ruclem8 16205 idfu1st 17856 cofu1st 17860 xpccatid 18170 prf1st 18186 yonedalem21 18256 yonedalem22 18261 2ndcctbss 23346 upxp 23514 uptx 23516 cnheiborlem 24867 ovollb2lem 25404 ovolctb 25406 ovoliunlem2 25419 ovolshftlem1 25425 ovolscalem1 25429 ovolicc1 25432 addsqnreup 27363 2sqreuop 27382 2sqreuopnn 27383 2sqreuoplt 27384 2sqreuopltb 27385 2sqreuopnnlt 27386 2sqreuopnnltb 27387 precsexlem1 28092 precsexlem4 28095 ex-1st 30241 cnnvg 30475 cnnvs 30477 h2hva 30771 h2hsm 30772 hhssva 31054 hhsssm 31055 hhshsslem1 31064 gsumhashmul 32748 eulerpartlemgvv 33932 eulerpartlemgh 33934 satfv0fvfmla0 34959 filnetlem3 35800 poimirlem17 37045 heiborlem8 37226 dvhvaddass 40507 dvhlveclem 40518 diblss 40580 aks6d1c3 41527 pellexlem5 42175 pellex 42177 dvnprodlem1 45257 hoicvr 45859 hoicvrrex 45867 ovn0lem 45876 ovnhoilem1 45912 thincciso 47978 |
Copyright terms: Public domain | W3C validator |