![]() |
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 4873 | . . . 4 ⊢ (𝑥 = 𝐴 → ⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝑦⟩) | |
2 | 1 | fveq2d 6895 | . . 3 ⊢ (𝑥 = 𝐴 → (1st ‘⟨𝑥, 𝑦⟩) = (1st ‘⟨𝐴, 𝑦⟩)) |
3 | id 22 | . . 3 ⊢ (𝑥 = 𝐴 → 𝑥 = 𝐴) | |
4 | 2, 3 | eqeq12d 2748 | . 2 ⊢ (𝑥 = 𝐴 → ((1st ‘⟨𝑥, 𝑦⟩) = 𝑥 ↔ (1st ‘⟨𝐴, 𝑦⟩) = 𝐴)) |
5 | opeq2 4874 | . . 3 ⊢ (𝑦 = 𝐵 → ⟨𝐴, 𝑦⟩ = ⟨𝐴, 𝐵⟩) | |
6 | 5 | fveqeq2d 6899 | . 2 ⊢ (𝑦 = 𝐵 → ((1st ‘⟨𝐴, 𝑦⟩) = 𝐴 ↔ (1st ‘⟨𝐴, 𝐵⟩) = 𝐴)) |
7 | vex 3478 | . . 3 ⊢ 𝑥 ∈ V | |
8 | vex 3478 | . . 3 ⊢ 𝑦 ∈ V | |
9 | 7, 8 | op1st 7982 | . 2 ⊢ (1st ‘⟨𝑥, 𝑦⟩) = 𝑥 |
10 | 4, 6, 9 | vtocl2g 3562 | 1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (1st ‘⟨𝐴, 𝐵⟩) = 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 = wceq 1541 ∈ wcel 2106 ⟨cop 4634 ‘cfv 6543 1st c1st 7972 |
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 5299 ax-nul 5306 ax-pr 5427 ax-un 7724 |
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 3951 df-un 3953 df-in 3955 df-ss 3965 df-nul 4323 df-if 4529 df-sn 4629 df-pr 4631 df-op 4635 df-uni 4909 df-br 5149 df-opab 5211 df-mpt 5232 df-id 5574 df-xp 5682 df-rel 5683 df-cnv 5684 df-co 5685 df-dm 5686 df-rn 5687 df-iota 6495 df-fun 6545 df-fv 6551 df-1st 7974 |
This theorem is referenced by: ot1stg 7988 ot2ndg 7989 br1steqg 7996 1stconst 8085 mposn 8088 curry2 8092 opco1 8108 mpoxopn0yelv 8197 mpoxopoveq 8203 xpmapenlem 9143 1stinl 9921 1stinr 9923 fpwwe 10640 addpipq 10931 mulpipq 10934 ordpipq 10936 swrdval 14592 ruclem1 16173 qnumdenbi 16679 setsstruct 17108 oppccofval 17660 funcf2 17817 cofuval2 17836 resfval2 17842 resf1st 17843 isnat 17897 fucco 17914 homadm 17989 setcco 18032 estrcco 18080 xpcco 18134 xpchom2 18137 xpcco2 18138 evlf2 18170 curfval 18175 curf1cl 18180 uncf1 18188 uncf2 18189 diag11 18195 diag12 18196 diag2 18197 hof2fval 18207 yonedalem21 18225 yonedalem22 18230 mvmulfval 22043 imasdsf1olem 23878 ovolicc1 25032 ioombl1lem3 25076 ioombl1lem4 25077 addsqnreup 26943 addsval 27443 mulsval 27562 brcgr 28155 opvtxfv 28261 fgreu 31892 fsuppcurry2 31946 sategoelfvb 34405 prv1n 34417 fvtransport 34999 bj-inftyexpiinv 36084 bj-finsumval0 36161 poimirlem17 36500 poimirlem24 36507 poimirlem27 36510 rngoablo2 36772 dvhopvadd 39959 dvhopvsca 39968 dvhopaddN 39980 dvhopspN 39981 etransclem44 44984 ovnsubaddlem1 45276 ovnlecvr2 45316 ovolval5lem2 45359 rngccoALTV 46876 ringccoALTV 46939 |
Copyright terms: Public domain | W3C validator |