![]() |
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 4874 | . . . 4 ⊢ (𝑥 = 𝐴 → ⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝑦⟩) | |
2 | 1 | fveq2d 6896 | . . 3 ⊢ (𝑥 = 𝐴 → (1st ‘⟨𝑥, 𝑦⟩) = (1st ‘⟨𝐴, 𝑦⟩)) |
3 | id 22 | . . 3 ⊢ (𝑥 = 𝐴 → 𝑥 = 𝐴) | |
4 | 2, 3 | eqeq12d 2749 | . 2 ⊢ (𝑥 = 𝐴 → ((1st ‘⟨𝑥, 𝑦⟩) = 𝑥 ↔ (1st ‘⟨𝐴, 𝑦⟩) = 𝐴)) |
5 | opeq2 4875 | . . 3 ⊢ (𝑦 = 𝐵 → ⟨𝐴, 𝑦⟩ = ⟨𝐴, 𝐵⟩) | |
6 | 5 | fveqeq2d 6900 | . 2 ⊢ (𝑦 = 𝐵 → ((1st ‘⟨𝐴, 𝑦⟩) = 𝐴 ↔ (1st ‘⟨𝐴, 𝐵⟩) = 𝐴)) |
7 | vex 3479 | . . 3 ⊢ 𝑥 ∈ V | |
8 | vex 3479 | . . 3 ⊢ 𝑦 ∈ V | |
9 | 7, 8 | op1st 7983 | . 2 ⊢ (1st ‘⟨𝑥, 𝑦⟩) = 𝑥 |
10 | 4, 6, 9 | vtocl2g 3563 | 1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (1st ‘⟨𝐴, 𝐵⟩) = 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 397 = wceq 1542 ∈ wcel 2107 ⟨cop 4635 ‘cfv 6544 1st c1st 7973 |
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 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2704 ax-sep 5300 ax-nul 5307 ax-pr 5428 ax-un 7725 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2535 df-eu 2564 df-clab 2711 df-cleq 2725 df-clel 2811 df-nfc 2886 df-ral 3063 df-rex 3072 df-rab 3434 df-v 3477 df-dif 3952 df-un 3954 df-in 3956 df-ss 3966 df-nul 4324 df-if 4530 df-sn 4630 df-pr 4632 df-op 4636 df-uni 4910 df-br 5150 df-opab 5212 df-mpt 5233 df-id 5575 df-xp 5683 df-rel 5684 df-cnv 5685 df-co 5686 df-dm 5687 df-rn 5688 df-iota 6496 df-fun 6546 df-fv 6552 df-1st 7975 |
This theorem is referenced by: ot1stg 7989 ot2ndg 7990 br1steqg 7997 1stconst 8086 mposn 8089 curry2 8093 opco1 8109 mpoxopn0yelv 8198 mpoxopoveq 8204 xpmapenlem 9144 1stinl 9922 1stinr 9924 fpwwe 10641 addpipq 10932 mulpipq 10935 ordpipq 10937 swrdval 14593 ruclem1 16174 qnumdenbi 16680 setsstruct 17109 oppccofval 17661 funcf2 17818 cofuval2 17837 resfval2 17843 resf1st 17844 isnat 17898 fucco 17915 homadm 17990 setcco 18033 estrcco 18081 xpcco 18135 xpchom2 18138 xpcco2 18139 evlf2 18171 curfval 18176 curf1cl 18181 uncf1 18189 uncf2 18190 diag11 18196 diag12 18197 diag2 18198 hof2fval 18208 yonedalem21 18226 yonedalem22 18231 mvmulfval 22044 imasdsf1olem 23879 ovolicc1 25033 ioombl1lem3 25077 ioombl1lem4 25078 addsqnreup 26946 addsval 27446 mulsval 27565 brcgr 28158 opvtxfv 28264 fgreu 31897 fsuppcurry2 31951 sategoelfvb 34410 prv1n 34422 fvtransport 35004 bj-inftyexpiinv 36089 bj-finsumval0 36166 poimirlem17 36505 poimirlem24 36512 poimirlem27 36515 rngoablo2 36777 dvhopvadd 39964 dvhopvsca 39973 dvhopaddN 39985 dvhopspN 39986 etransclem44 44994 ovnsubaddlem1 45286 ovnlecvr2 45326 ovolval5lem2 45369 rngccoALTV 46886 ringccoALTV 46949 |
Copyright terms: Public domain | W3C validator |