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 4795 | . . . 4 ⊢ (𝑥 = 𝐴 → 〈𝑥, 𝑦〉 = 〈𝐴, 𝑦〉) | |
2 | 1 | fveq2d 6667 | . . 3 ⊢ (𝑥 = 𝐴 → (1st ‘〈𝑥, 𝑦〉) = (1st ‘〈𝐴, 𝑦〉)) |
3 | id 22 | . . 3 ⊢ (𝑥 = 𝐴 → 𝑥 = 𝐴) | |
4 | 2, 3 | eqeq12d 2834 | . 2 ⊢ (𝑥 = 𝐴 → ((1st ‘〈𝑥, 𝑦〉) = 𝑥 ↔ (1st ‘〈𝐴, 𝑦〉) = 𝐴)) |
5 | opeq2 4796 | . . 3 ⊢ (𝑦 = 𝐵 → 〈𝐴, 𝑦〉 = 〈𝐴, 𝐵〉) | |
6 | 5 | fveqeq2d 6671 | . 2 ⊢ (𝑦 = 𝐵 → ((1st ‘〈𝐴, 𝑦〉) = 𝐴 ↔ (1st ‘〈𝐴, 𝐵〉) = 𝐴)) |
7 | vex 3495 | . . 3 ⊢ 𝑥 ∈ V | |
8 | vex 3495 | . . 3 ⊢ 𝑦 ∈ V | |
9 | 7, 8 | op1st 7686 | . 2 ⊢ (1st ‘〈𝑥, 𝑦〉) = 𝑥 |
10 | 4, 6, 9 | vtocl2g 3569 | 1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (1st ‘〈𝐴, 𝐵〉) = 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 = wceq 1528 ∈ wcel 2105 〈cop 4563 ‘cfv 6348 1st c1st 7676 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2790 ax-sep 5194 ax-nul 5201 ax-pow 5257 ax-pr 5320 ax-un 7450 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-3an 1081 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-mo 2615 df-eu 2647 df-clab 2797 df-cleq 2811 df-clel 2890 df-nfc 2960 df-ral 3140 df-rex 3141 df-rab 3144 df-v 3494 df-sbc 3770 df-dif 3936 df-un 3938 df-in 3940 df-ss 3949 df-nul 4289 df-if 4464 df-sn 4558 df-pr 4560 df-op 4564 df-uni 4831 df-br 5058 df-opab 5120 df-mpt 5138 df-id 5453 df-xp 5554 df-rel 5555 df-cnv 5556 df-co 5557 df-dm 5558 df-rn 5559 df-iota 6307 df-fun 6350 df-fv 6356 df-1st 7678 |
This theorem is referenced by: ot1stg 7692 ot2ndg 7693 br1steqg 7700 1stconst 7784 mposn 7787 curry2 7791 mpoxopn0yelv 7868 mpoxopoveq 7874 xpmapenlem 8672 1stinl 9344 1stinr 9346 fpwwe 10056 addpipq 10347 mulpipq 10350 ordpipq 10352 swrdval 13993 ruclem1 15572 qnumdenbi 16072 setsstruct 16511 oppccofval 16974 funcf2 17126 cofuval2 17145 resfval2 17151 resf1st 17152 isnat 17205 fucco 17220 homadm 17288 setcco 17331 estrcco 17368 xpcco 17421 xpchom2 17424 xpcco2 17425 evlf2 17456 curfval 17461 curf1cl 17466 uncf1 17474 uncf2 17475 diag11 17481 diag12 17482 diag2 17483 hof2fval 17493 yonedalem21 17511 yonedalem22 17516 mvmulfval 21079 imasdsf1olem 22910 ovolicc1 24044 ioombl1lem3 24088 ioombl1lem4 24089 addsqnreup 25946 brcgr 26613 opvtxfv 26716 fgreu 30345 fsuppcurry2 30388 sategoelfvb 32563 prv1n 32575 fvtransport 33390 bj-inftyexpiinv 34382 bj-finsumval0 34455 poimirlem17 34790 poimirlem24 34797 poimirlem27 34800 rngoablo2 35068 dvhopvadd 38109 dvhopvsca 38118 dvhopaddN 38130 dvhopspN 38131 etransclem44 42440 ovnsubaddlem1 42729 ovnlecvr2 42769 ovolval5lem2 42812 rngccoALTV 44187 ringccoALTV 44250 |
Copyright terms: Public domain | W3C validator |