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 7833 | . 2 ⊢ (1st ‘〈𝐴, 𝐵〉) = ∪ dom {〈𝐴, 𝐵〉} | |
2 | op1st.1 | . . 3 ⊢ 𝐴 ∈ V | |
3 | op1st.2 | . . 3 ⊢ 𝐵 ∈ V | |
4 | 2, 3 | op1sta 6128 | . 2 ⊢ ∪ dom {〈𝐴, 𝐵〉} = 𝐴 |
5 | 1, 4 | eqtri 2766 | 1 ⊢ (1st ‘〈𝐴, 𝐵〉) = 𝐴 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1539 ∈ wcel 2106 Vcvv 3432 {csn 4561 〈cop 4567 ∪ cuni 4839 dom cdm 5589 ‘cfv 6433 1st c1st 7829 |
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 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2709 ax-sep 5223 ax-nul 5230 ax-pr 5352 ax-un 7588 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1783 df-nf 1787 df-sb 2068 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2816 df-nfc 2889 df-ral 3069 df-rex 3070 df-rab 3073 df-v 3434 df-dif 3890 df-un 3892 df-in 3894 df-ss 3904 df-nul 4257 df-if 4460 df-sn 4562 df-pr 4564 df-op 4568 df-uni 4840 df-br 5075 df-opab 5137 df-mpt 5158 df-id 5489 df-xp 5595 df-rel 5596 df-cnv 5597 df-co 5598 df-dm 5599 df-rn 5600 df-iota 6391 df-fun 6435 df-fv 6441 df-1st 7831 |
This theorem is referenced by: op1std 7841 op1stg 7843 1stval2 7848 fo1stres 7857 opreuopreu 7876 eloprabi 7903 xpmapenlem 8931 fseqenlem2 9781 archnq 10736 ruclem8 15946 idfu1st 17594 cofu1st 17598 xpccatid 17905 prf1st 17921 yonedalem21 17991 yonedalem22 17996 2ndcctbss 22606 upxp 22774 uptx 22776 cnheiborlem 24117 ovollb2lem 24652 ovolctb 24654 ovoliunlem2 24667 ovolshftlem1 24673 ovolscalem1 24677 ovolicc1 24680 addsqnreup 26591 2sqreuop 26610 2sqreuopnn 26611 2sqreuoplt 26612 2sqreuopltb 26613 2sqreuopnnlt 26614 2sqreuopnnltb 26615 ex-1st 28808 cnnvg 29040 cnnvs 29042 h2hva 29336 h2hsm 29337 hhssva 29619 hhsssm 29620 hhshsslem1 29629 gsumhashmul 31316 eulerpartlemgvv 32343 eulerpartlemgh 32345 satfv0fvfmla0 33375 ot21std 33680 filnetlem3 34569 poimirlem17 35794 heiborlem8 35976 dvhvaddass 39111 dvhlveclem 39122 diblss 39184 pellexlem5 40655 pellex 40657 dvnprodlem1 43487 hoicvr 44086 hoicvrrex 44094 ovn0lem 44103 ovnhoilem1 44139 thincciso 46330 |
Copyright terms: Public domain | W3C validator |