![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > op2ndg | Structured version Visualization version GIF version |
Description: Extract the second member of an ordered pair. (Contributed by NM, 19-Jul-2005.) |
Ref | Expression |
---|---|
op2ndg | ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (2nd ‘〈𝐴, 𝐵〉) = 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | opeq1 4545 | . . . 4 ⊢ (𝑥 = 𝐴 → 〈𝑥, 𝑦〉 = 〈𝐴, 𝑦〉) | |
2 | 1 | fveq2d 6348 | . . 3 ⊢ (𝑥 = 𝐴 → (2nd ‘〈𝑥, 𝑦〉) = (2nd ‘〈𝐴, 𝑦〉)) |
3 | 2 | eqeq1d 2754 | . 2 ⊢ (𝑥 = 𝐴 → ((2nd ‘〈𝑥, 𝑦〉) = 𝑦 ↔ (2nd ‘〈𝐴, 𝑦〉) = 𝑦)) |
4 | opeq2 4546 | . . . 4 ⊢ (𝑦 = 𝐵 → 〈𝐴, 𝑦〉 = 〈𝐴, 𝐵〉) | |
5 | 4 | fveq2d 6348 | . . 3 ⊢ (𝑦 = 𝐵 → (2nd ‘〈𝐴, 𝑦〉) = (2nd ‘〈𝐴, 𝐵〉)) |
6 | id 22 | . . 3 ⊢ (𝑦 = 𝐵 → 𝑦 = 𝐵) | |
7 | 5, 6 | eqeq12d 2767 | . 2 ⊢ (𝑦 = 𝐵 → ((2nd ‘〈𝐴, 𝑦〉) = 𝑦 ↔ (2nd ‘〈𝐴, 𝐵〉) = 𝐵)) |
8 | vex 3335 | . . 3 ⊢ 𝑥 ∈ V | |
9 | vex 3335 | . . 3 ⊢ 𝑦 ∈ V | |
10 | 8, 9 | op2nd 7334 | . 2 ⊢ (2nd ‘〈𝑥, 𝑦〉) = 𝑦 |
11 | 3, 7, 10 | vtocl2g 3402 | 1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (2nd ‘〈𝐴, 𝐵〉) = 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 = wceq 1624 ∈ wcel 2131 〈cop 4319 ‘cfv 6041 2nd c2nd 7324 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1863 ax-4 1878 ax-5 1980 ax-6 2046 ax-7 2082 ax-8 2133 ax-9 2140 ax-10 2160 ax-11 2175 ax-12 2188 ax-13 2383 ax-ext 2732 ax-sep 4925 ax-nul 4933 ax-pow 4984 ax-pr 5047 ax-un 7106 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3an 1074 df-tru 1627 df-ex 1846 df-nf 1851 df-sb 2039 df-eu 2603 df-mo 2604 df-clab 2739 df-cleq 2745 df-clel 2748 df-nfc 2883 df-ral 3047 df-rex 3048 df-rab 3051 df-v 3334 df-sbc 3569 df-dif 3710 df-un 3712 df-in 3714 df-ss 3721 df-nul 4051 df-if 4223 df-sn 4314 df-pr 4316 df-op 4320 df-uni 4581 df-br 4797 df-opab 4857 df-mpt 4874 df-id 5166 df-xp 5264 df-rel 5265 df-cnv 5266 df-co 5267 df-dm 5268 df-rn 5269 df-iota 6004 df-fun 6043 df-fv 6049 df-2nd 7326 |
This theorem is referenced by: ot2ndg 7340 ot3rdg 7341 br2ndeqg 7348 2ndconst 7426 mpt2sn 7428 curry1 7429 xpmapenlem 8284 axdc4lem 9461 pinq 9933 addpipq 9943 mulpipq 9946 ordpipq 9948 swrdval 13608 ruclem1 15151 eucalg 15494 qnumdenbi 15646 setsstruct 16092 comffval 16552 oppccofval 16569 funcf2 16721 cofuval2 16740 resfval2 16746 resf2nd 16748 funcres 16749 isnat 16800 fucco 16815 homacd 16884 setcco 16926 catcco 16944 estrcco 16963 xpcco 17016 xpchom2 17019 xpcco2 17020 evlf2 17051 curfval 17056 curf1cl 17061 uncf1 17069 uncf2 17070 hof2fval 17088 yonedalem21 17106 yonedalem22 17111 mvmulfval 20542 imasdsf1olem 22371 ovolicc1 23476 ioombl1lem3 23520 ioombl1lem4 23521 brcgr 25971 opiedgfv 26078 fvtransport 32437 bj-elid3 33390 bj-finsumval0 33450 poimirlem17 33731 poimirlem24 33738 poimirlem27 33741 dvhopvadd 36876 dvhopvsca 36885 dvhopaddN 36897 dvhopspN 36898 etransclem44 40990 uspgrsprfo 42258 rngccoALTV 42490 ringccoALTV 42553 lmod1zr 42784 |
Copyright terms: Public domain | W3C validator |