![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > op1std | Structured version Visualization version GIF version |
Description: Extract the first member of an ordered pair. (Contributed by Mario Carneiro, 31-Aug-2015.) |
Ref | Expression |
---|---|
op1st.1 | ⊢ 𝐴 ∈ V |
op1st.2 | ⊢ 𝐵 ∈ V |
Ref | Expression |
---|---|
op1std | ⊢ (𝐶 = 〈𝐴, 𝐵〉 → (1st ‘𝐶) = 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fveq2 6888 | . 2 ⊢ (𝐶 = 〈𝐴, 𝐵〉 → (1st ‘𝐶) = (1st ‘〈𝐴, 𝐵〉)) | |
2 | op1st.1 | . . 3 ⊢ 𝐴 ∈ V | |
3 | op1st.2 | . . 3 ⊢ 𝐵 ∈ V | |
4 | 2, 3 | op1st 7979 | . 2 ⊢ (1st ‘〈𝐴, 𝐵〉) = 𝐴 |
5 | 1, 4 | eqtrdi 2788 | 1 ⊢ (𝐶 = 〈𝐴, 𝐵〉 → (1st ‘𝐶) = 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1541 ∈ wcel 2106 Vcvv 3474 〈cop 4633 ‘cfv 6540 1st c1st 7969 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 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 2703 ax-sep 5298 ax-nul 5305 ax-pr 5426 ax-un 7721 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2534 df-eu 2563 df-clab 2710 df-cleq 2724 df-clel 2810 df-nfc 2885 df-ral 3062 df-rex 3071 df-rab 3433 df-v 3476 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-1st 7971 |
This theorem is referenced by: 1st2val 7999 xp1st 8003 sbcopeq1a 8031 csbopeq1a 8032 eloprabi 8045 mpomptsx 8046 dmmpossx 8048 fmpox 8049 ovmptss 8075 fmpoco 8077 df1st2 8080 fsplit 8099 frxp 8108 xporderlem 8109 fnwelem 8113 fimaproj 8117 xpord2lem 8124 naddcllem 8671 xpf1o 9135 mapunen 9142 xpwdomg 9576 hsmexlem2 10418 fsumcom2 15716 fprodcom2 15924 qredeu 16591 isfuncd 17811 cofucl 17834 funcres2b 17843 funcpropd 17847 xpcco1st 18132 xpccatid 18136 1stf1 18140 2ndf1 18143 1stfcl 18145 prf1 18148 prfcl 18151 prf1st 18152 prf2nd 18153 evlf1 18169 evlfcl 18171 curf1fval 18173 curf11 18175 curf1cl 18177 curfcl 18181 hof1fval 18202 txbas 23062 cnmpt1st 23163 txhmeo 23298 ptuncnv 23302 ptunhmeo 23303 xpstopnlem1 23304 xkohmeo 23310 prdstmdd 23619 ucnimalem 23776 fmucndlem 23787 fsum2cn 24378 ovoliunlem1 25010 lgsquadlem1 26872 lgsquadlem2 26873 2sqreuop 26954 2sqreuopnn 26955 2sqreuoplt 26956 2sqreuopltb 26957 2sqreuopnnlt 26958 2sqreuopnnltb 26959 clwlkclwwlkfolem 29249 wlkl0 29609 gsumhashmul 32195 eulerpartlemgs2 33367 hgt750lemb 33656 cvmliftlem15 34277 satfv1 34342 satfdmlem 34347 fmlasuc 34365 msubty 34506 msubco 34510 msubvrs 34539 filnetlem4 35254 finixpnum 36461 poimirlem4 36480 poimirlem15 36491 poimirlem20 36496 poimirlem26 36502 poimirlem28 36504 heicant 36511 dicelvalN 40037 aks6d1c2p1 40944 fmpocos 41053 rmxypairf1o 41635 unxpwdom3 41822 fgraphxp 41938 elcnvlem 42337 dvnprodlem2 44649 etransclem46 44982 ovnsubaddlem1 45272 dmmpossx2 46965 2arymaptf 47291 rrx2plordisom 47362 funcf2lem 47591 |
Copyright terms: Public domain | W3C validator |