![]() |
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 4829 | . . 3 ⊢ (𝑥 = 𝐴 → 〈𝑥, 𝑦〉 = 〈𝐴, 𝑦〉) | |
2 | 1 | fveqeq2d 6848 | . 2 ⊢ (𝑥 = 𝐴 → ((2nd ‘〈𝑥, 𝑦〉) = 𝑦 ↔ (2nd ‘〈𝐴, 𝑦〉) = 𝑦)) |
3 | opeq2 4830 | . . . 4 ⊢ (𝑦 = 𝐵 → 〈𝐴, 𝑦〉 = 〈𝐴, 𝐵〉) | |
4 | 3 | fveq2d 6844 | . . 3 ⊢ (𝑦 = 𝐵 → (2nd ‘〈𝐴, 𝑦〉) = (2nd ‘〈𝐴, 𝐵〉)) |
5 | id 22 | . . 3 ⊢ (𝑦 = 𝐵 → 𝑦 = 𝐵) | |
6 | 4, 5 | eqeq12d 2752 | . 2 ⊢ (𝑦 = 𝐵 → ((2nd ‘〈𝐴, 𝑦〉) = 𝑦 ↔ (2nd ‘〈𝐴, 𝐵〉) = 𝐵)) |
7 | vex 3448 | . . 3 ⊢ 𝑥 ∈ V | |
8 | vex 3448 | . . 3 ⊢ 𝑦 ∈ V | |
9 | 7, 8 | op2nd 7927 | . 2 ⊢ (2nd ‘〈𝑥, 𝑦〉) = 𝑦 |
10 | 2, 6, 9 | vtocl2g 3530 | 1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (2nd ‘〈𝐴, 𝐵〉) = 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 = wceq 1541 ∈ wcel 2106 〈cop 4591 ‘cfv 6494 2nd c2nd 7917 |
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 2707 ax-sep 5255 ax-nul 5262 ax-pr 5383 ax-un 7669 |
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 2538 df-eu 2567 df-clab 2714 df-cleq 2728 df-clel 2814 df-nfc 2888 df-ral 3064 df-rex 3073 df-rab 3407 df-v 3446 df-dif 3912 df-un 3914 df-in 3916 df-ss 3926 df-nul 4282 df-if 4486 df-sn 4586 df-pr 4588 df-op 4592 df-uni 4865 df-br 5105 df-opab 5167 df-mpt 5188 df-id 5530 df-xp 5638 df-rel 5639 df-cnv 5640 df-co 5641 df-dm 5642 df-rn 5643 df-iota 6446 df-fun 6496 df-fv 6502 df-2nd 7919 |
This theorem is referenced by: ot2ndg 7933 ot3rdg 7934 br2ndeqg 7941 2ndconst 8030 mposn 8032 curry1 8033 opco2 8053 xpmapenlem 9085 2ndinl 9861 2ndinr 9863 axdc4lem 10388 pinq 10860 addpipq 10870 mulpipq 10873 ordpipq 10875 swrdval 14528 ruclem1 16110 eucalg 16460 qnumdenbi 16616 setsstruct 17045 comffval 17576 oppccofval 17594 funcf2 17751 cofuval2 17770 resfval2 17776 resf2nd 17778 funcres 17779 isnat 17831 fucco 17848 homacd 17924 setcco 17966 catcco 17988 estrcco 18014 xpcco 18068 xpchom2 18071 xpcco2 18072 evlf2 18104 curfval 18109 curf1cl 18114 uncf1 18122 uncf2 18123 hof2fval 18141 yonedalem21 18159 yonedalem22 18164 mvmulfval 21887 imasdsf1olem 23722 ovolicc1 24876 ioombl1lem3 24920 ioombl1lem4 24921 addsqnreup 26787 brcgr 27747 opiedgfv 27856 fsuppcurry1 31537 sategoelfvb 33904 prv1n 33916 addsval 34300 mulsval 34397 fvtransport 34606 bj-finsumval0 35745 poimirlem17 36084 poimirlem24 36091 poimirlem27 36094 dvhopvadd 39545 dvhopvsca 39554 dvhopaddN 39566 dvhopspN 39567 etransclem44 44489 uspgrsprfo 46020 rngccoALTV 46256 ringccoALTV 46319 lmod1zr 46544 |
Copyright terms: Public domain | W3C validator |