![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > op1stg | Structured version Visualization version GIF version |
Description: Extract the first member of an ordered pair. (Contributed by NM, 19-Jul-2005.) |
Ref | Expression |
---|---|
op1stg | ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (1st ‘〈𝐴, 𝐵〉) = 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | opeq1 4678 | . . . 4 ⊢ (𝑥 = 𝐴 → 〈𝑥, 𝑦〉 = 〈𝐴, 𝑦〉) | |
2 | 1 | fveq2d 6505 | . . 3 ⊢ (𝑥 = 𝐴 → (1st ‘〈𝑥, 𝑦〉) = (1st ‘〈𝐴, 𝑦〉)) |
3 | id 22 | . . 3 ⊢ (𝑥 = 𝐴 → 𝑥 = 𝐴) | |
4 | 2, 3 | eqeq12d 2793 | . 2 ⊢ (𝑥 = 𝐴 → ((1st ‘〈𝑥, 𝑦〉) = 𝑥 ↔ (1st ‘〈𝐴, 𝑦〉) = 𝐴)) |
5 | opeq2 4679 | . . 3 ⊢ (𝑦 = 𝐵 → 〈𝐴, 𝑦〉 = 〈𝐴, 𝐵〉) | |
6 | 5 | fveqeq2d 6509 | . 2 ⊢ (𝑦 = 𝐵 → ((1st ‘〈𝐴, 𝑦〉) = 𝐴 ↔ (1st ‘〈𝐴, 𝐵〉) = 𝐴)) |
7 | vex 3418 | . . 3 ⊢ 𝑥 ∈ V | |
8 | vex 3418 | . . 3 ⊢ 𝑦 ∈ V | |
9 | 7, 8 | op1st 7511 | . 2 ⊢ (1st ‘〈𝑥, 𝑦〉) = 𝑥 |
10 | 4, 6, 9 | vtocl2g 3490 | 1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (1st ‘〈𝐴, 𝐵〉) = 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 387 = wceq 1507 ∈ wcel 2050 〈cop 4448 ‘cfv 6190 1st c1st 7501 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1965 ax-8 2052 ax-9 2059 ax-10 2079 ax-11 2093 ax-12 2106 ax-13 2301 ax-ext 2750 ax-sep 5061 ax-nul 5068 ax-pow 5120 ax-pr 5187 ax-un 7281 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-3an 1070 df-tru 1510 df-ex 1743 df-nf 1747 df-sb 2016 df-mo 2547 df-eu 2583 df-clab 2759 df-cleq 2771 df-clel 2846 df-nfc 2918 df-ral 3093 df-rex 3094 df-rab 3097 df-v 3417 df-sbc 3684 df-dif 3834 df-un 3836 df-in 3838 df-ss 3845 df-nul 4181 df-if 4352 df-sn 4443 df-pr 4445 df-op 4449 df-uni 4714 df-br 4931 df-opab 4993 df-mpt 5010 df-id 5313 df-xp 5414 df-rel 5415 df-cnv 5416 df-co 5417 df-dm 5418 df-rn 5419 df-iota 6154 df-fun 6192 df-fv 6198 df-1st 7503 |
This theorem is referenced by: ot1stg 7517 ot2ndg 7518 br1steqg 7525 1stconst 7605 mposn 7608 curry2 7612 mpoxopn0yelv 7684 mpoxopoveq 7690 xpmapenlem 8482 1stinl 9152 1stinr 9154 fpwwe 9868 addpipq 10159 mulpipq 10162 ordpipq 10164 swrdval 13809 ruclem1 15447 qnumdenbi 15943 setsstruct 16382 oppccofval 16847 funcf2 16999 cofuval2 17018 resfval2 17024 resf1st 17025 isnat 17078 fucco 17093 homadm 17161 setcco 17204 estrcco 17241 xpcco 17294 xpchom2 17297 xpcco2 17298 evlf2 17329 curfval 17334 curf1cl 17339 uncf1 17347 uncf2 17348 diag11 17354 diag12 17355 diag2 17356 hof2fval 17366 yonedalem21 17384 yonedalem22 17389 mvmulfval 20858 imasdsf1olem 22689 ovolicc1 23823 ioombl1lem3 23867 ioombl1lem4 23868 addsqnreup 25724 brcgr 26392 opvtxfv 26495 fgreu 30182 fsuppcurry2 30217 fvtransport 33014 bj-elid3 33940 bj-inftyexpiinv 33959 bj-finsumval0 34030 poimirlem17 34350 poimirlem24 34357 poimirlem27 34360 rngoablo2 34629 dvhopvadd 37674 dvhopvsca 37683 dvhopaddN 37695 dvhopspN 37696 etransclem44 41995 ovnsubaddlem1 42284 ovnlecvr2 42324 ovolval5lem2 42367 rngccoALTV 43624 ringccoALTV 43687 |
Copyright terms: Public domain | W3C validator |