![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > fvsng | Structured version Visualization version GIF version |
Description: The value of a singleton of an ordered pair is the second member. (Contributed by NM, 26-Oct-2012.) |
Ref | Expression |
---|---|
fvsng | ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ({〈𝐴, 𝐵〉}‘𝐴) = 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | opeq1 4433 | . . . . 5 ⊢ (𝑎 = 𝐴 → 〈𝑎, 𝑏〉 = 〈𝐴, 𝑏〉) | |
2 | 1 | sneqd 4222 | . . . 4 ⊢ (𝑎 = 𝐴 → {〈𝑎, 𝑏〉} = {〈𝐴, 𝑏〉}) |
3 | id 22 | . . . 4 ⊢ (𝑎 = 𝐴 → 𝑎 = 𝐴) | |
4 | 2, 3 | fveq12d 6235 | . . 3 ⊢ (𝑎 = 𝐴 → ({〈𝑎, 𝑏〉}‘𝑎) = ({〈𝐴, 𝑏〉}‘𝐴)) |
5 | 4 | eqeq1d 2653 | . 2 ⊢ (𝑎 = 𝐴 → (({〈𝑎, 𝑏〉}‘𝑎) = 𝑏 ↔ ({〈𝐴, 𝑏〉}‘𝐴) = 𝑏)) |
6 | opeq2 4434 | . . . . 5 ⊢ (𝑏 = 𝐵 → 〈𝐴, 𝑏〉 = 〈𝐴, 𝐵〉) | |
7 | 6 | sneqd 4222 | . . . 4 ⊢ (𝑏 = 𝐵 → {〈𝐴, 𝑏〉} = {〈𝐴, 𝐵〉}) |
8 | 7 | fveq1d 6231 | . . 3 ⊢ (𝑏 = 𝐵 → ({〈𝐴, 𝑏〉}‘𝐴) = ({〈𝐴, 𝐵〉}‘𝐴)) |
9 | id 22 | . . 3 ⊢ (𝑏 = 𝐵 → 𝑏 = 𝐵) | |
10 | 8, 9 | eqeq12d 2666 | . 2 ⊢ (𝑏 = 𝐵 → (({〈𝐴, 𝑏〉}‘𝐴) = 𝑏 ↔ ({〈𝐴, 𝐵〉}‘𝐴) = 𝐵)) |
11 | vex 3234 | . . 3 ⊢ 𝑎 ∈ V | |
12 | vex 3234 | . . 3 ⊢ 𝑏 ∈ V | |
13 | 11, 12 | fvsn 6487 | . 2 ⊢ ({〈𝑎, 𝑏〉}‘𝑎) = 𝑏 |
14 | 5, 10, 13 | vtocl2g 3301 | 1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ({〈𝐴, 𝐵〉}‘𝐴) = 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 = wceq 1523 ∈ wcel 2030 {csn 4210 〈cop 4216 ‘cfv 5926 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1762 ax-4 1777 ax-5 1879 ax-6 1945 ax-7 1981 ax-9 2039 ax-10 2059 ax-11 2074 ax-12 2087 ax-13 2282 ax-ext 2631 ax-sep 4814 ax-nul 4822 ax-pr 4936 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3an 1056 df-tru 1526 df-ex 1745 df-nf 1750 df-sb 1938 df-eu 2502 df-mo 2503 df-clab 2638 df-cleq 2644 df-clel 2647 df-nfc 2782 df-ral 2946 df-rex 2947 df-rab 2950 df-v 3233 df-sbc 3469 df-dif 3610 df-un 3612 df-in 3614 df-ss 3621 df-nul 3949 df-if 4120 df-sn 4211 df-pr 4213 df-op 4217 df-uni 4469 df-br 4686 df-opab 4746 df-id 5053 df-xp 5149 df-rel 5150 df-cnv 5151 df-co 5152 df-dm 5153 df-iota 5889 df-fun 5928 df-fv 5934 |
This theorem is referenced by: fsnunfv 6494 fvpr1g 6499 fvpr2g 6500 fsnex 6578 suppsnop 7354 enfixsn 8110 axdc3lem4 9313 fseq1p1m1 12452 1fv 12497 s1fv 13427 sumsnf 14517 sumsn 14519 prodsn 14736 prodsnf 14738 seq1st 15331 vdwlem8 15739 setsid 15961 xpsc0 16267 xpsc1 16268 mgm1 17304 sgrp1 17340 mnd1 17378 mnd1id 17379 gsumws1 17423 grp1 17569 dprdsn 18481 ring1 18648 ixpsnbasval 19257 frgpcyg 19970 mat1dimscm 20329 mat1dimmul 20330 mat1rhmelval 20334 m1detdiag 20451 pt1hmeo 21657 1loopgrvd0 26456 1hevtxdg0 26457 1hevtxdg1 26458 1egrvtxdg1 26461 actfunsnrndisj 30811 reprsuc 30821 breprexplema 30836 cvmliftlem7 31399 cvmliftlem13 31404 noextenddif 31946 noextendlt 31947 noextendgt 31948 sumsnd 39499 mapsnend 39705 ovnovollem1 41191 nnsum3primesprm 42003 lincvalsng 42530 snlindsntorlem 42584 lmod1lem2 42602 lmod1lem3 42603 |
Copyright terms: Public domain | W3C validator |