![]() |
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 6618 | . 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → Fun {〈𝐴, 𝐵〉}) | |
2 | opex 5474 | . . 3 ⊢ 〈𝐴, 𝐵〉 ∈ V | |
3 | 2 | snid 4666 | . 2 ⊢ 〈𝐴, 𝐵〉 ∈ {〈𝐴, 𝐵〉} |
4 | funopfv 6958 | . 2 ⊢ (Fun {〈𝐴, 𝐵〉} → (〈𝐴, 𝐵〉 ∈ {〈𝐴, 𝐵〉} → ({〈𝐴, 𝐵〉}‘𝐴) = 𝐵)) | |
5 | 1, 3, 4 | mpisyl 21 | 1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ({〈𝐴, 𝐵〉}‘𝐴) = 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 395 = wceq 1536 ∈ wcel 2105 {csn 4630 〈cop 4636 Fun wfun 6556 ‘cfv 6562 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1791 ax-4 1805 ax-5 1907 ax-6 1964 ax-7 2004 ax-8 2107 ax-9 2115 ax-10 2138 ax-12 2174 ax-ext 2705 ax-sep 5301 ax-nul 5311 ax-pr 5437 |
This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1539 df-fal 1549 df-ex 1776 df-nf 1780 df-sb 2062 df-mo 2537 df-eu 2566 df-clab 2712 df-cleq 2726 df-clel 2813 df-ral 3059 df-rex 3068 df-rab 3433 df-v 3479 df-dif 3965 df-un 3967 df-ss 3979 df-nul 4339 df-if 4531 df-sn 4631 df-pr 4633 df-op 4637 df-uni 4912 df-br 5148 df-opab 5210 df-id 5582 df-xp 5694 df-rel 5695 df-cnv 5696 df-co 5697 df-dm 5698 df-iota 6515 df-fun 6564 df-fv 6570 |
This theorem is referenced by: fvsn 7200 fvsnun1 7201 fsnunfv 7206 fvpr1g 7209 fsnex 7302 suppsnop 8201 mapsnend 9074 enfixsn 9119 axdc3lem4 10490 fseq1p1m1 13634 1fv 13683 s1fv 14644 sumsnf 15775 prodsn 15994 prodsnf 15996 seq1st 16604 vdwlem8 17021 setsid 17241 mgm1 18683 sgrp1 18754 mnd1 18804 mnd1id 18805 gsumws1 18863 grp1 19077 dprdsn 20070 ring1 20323 ixpsnbasval 21232 frgpcyg 21609 mat1dimscm 22496 mat1dimmul 22497 mat1rhmelval 22501 m1detdiag 22618 pt1hmeo 23829 noextenddif 27727 noextendlt 27728 noextendgt 27729 1loopgrvd0 29536 1hevtxdg0 29537 1hevtxdg1 29538 1egrvtxdg1 29541 wlkl0 30395 actfunsnrndisj 34598 reprsuc 34608 breprexplema 34623 cvmliftlem7 35275 cvmliftlem13 35280 bj-fununsn2 37236 sticksstones9 42135 sticksstones11 42137 metakunt20 42205 frlmsnic 42526 sumsnd 44963 ovnovollem1 46611 nnsum3primesprm 47714 lincvalsng 48261 snlindsntorlem 48315 lmod1lem2 48333 lmod1lem3 48334 0aryfvalelfv 48484 1arympt1fv 48488 |
Copyright terms: Public domain | W3C validator |