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.) (Proof shortened by BJ, 25-Feb-2023.) |
Ref | Expression |
---|---|
fvsng | ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ({〈𝐴, 𝐵〉}‘𝐴) = 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | funsng 6400 | . 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → Fun {〈𝐴, 𝐵〉}) | |
2 | opex 5349 | . . 3 ⊢ 〈𝐴, 𝐵〉 ∈ V | |
3 | 2 | snid 4595 | . 2 ⊢ 〈𝐴, 𝐵〉 ∈ {〈𝐴, 𝐵〉} |
4 | funopfv 6712 | . 2 ⊢ (Fun {〈𝐴, 𝐵〉} → (〈𝐴, 𝐵〉 ∈ {〈𝐴, 𝐵〉} → ({〈𝐴, 𝐵〉}‘𝐴) = 𝐵)) | |
5 | 1, 3, 4 | mpisyl 21 | 1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ({〈𝐴, 𝐵〉}‘𝐴) = 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 398 = wceq 1533 ∈ wcel 2110 {csn 4561 〈cop 4567 Fun wfun 6344 ‘cfv 6350 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1907 ax-6 1966 ax-7 2011 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2156 ax-12 2172 ax-ext 2793 ax-sep 5196 ax-nul 5203 ax-pr 5322 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3an 1085 df-tru 1536 df-ex 1777 df-nf 1781 df-sb 2066 df-mo 2618 df-eu 2650 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ral 3143 df-rex 3144 df-rab 3147 df-v 3497 df-sbc 3773 df-dif 3939 df-un 3941 df-in 3943 df-ss 3952 df-nul 4292 df-if 4468 df-sn 4562 df-pr 4564 df-op 4568 df-uni 4833 df-br 5060 df-opab 5122 df-id 5455 df-xp 5556 df-rel 5557 df-cnv 5558 df-co 5559 df-dm 5560 df-iota 6309 df-fun 6352 df-fv 6358 |
This theorem is referenced by: fvsn 6938 fvsnun1 6939 fsnunfv 6944 fvpr1g 6949 fvpr2g 6950 fsnex 7033 suppsnop 7838 mapsnend 8582 enfixsn 8620 axdc3lem4 9869 fseq1p1m1 12975 1fv 13020 s1fv 13958 sumsnf 15093 prodsn 15310 prodsnf 15312 seq1st 15909 vdwlem8 16318 setsid 16532 mgm1 17862 sgrp1 17904 mnd1 17946 mnd1id 17947 gsumws1 17996 grp1 18200 dprdsn 19152 ring1 19346 ixpsnbasval 19976 frgpcyg 20714 mat1dimscm 21078 mat1dimmul 21079 mat1rhmelval 21083 m1detdiag 21200 pt1hmeo 22408 1loopgrvd0 27280 1hevtxdg0 27281 1hevtxdg1 27282 1egrvtxdg1 27285 wlkl0 28140 actfunsnrndisj 31871 reprsuc 31881 breprexplema 31896 cvmliftlem7 32533 cvmliftlem13 32538 noextenddif 33170 noextendlt 33171 noextendgt 33172 bj-fununsn2 34530 frlmsnic 39142 sumsnd 41276 ovnovollem1 42931 nnsum3primesprm 43948 lincvalsng 44464 snlindsntorlem 44518 lmod1lem2 44536 lmod1lem3 44537 |
Copyright terms: Public domain | W3C validator |