MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  fvsng Structured version   Visualization version   GIF version

Theorem fvsng 7127
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.)
Assertion
Ref Expression
fvsng ((𝐴𝑉𝐵𝑊) → ({⟨𝐴, 𝐵⟩}‘𝐴) = 𝐵)

Proof of Theorem fvsng
StepHypRef Expression
1 funsng 6553 . 2 ((𝐴𝑉𝐵𝑊) → Fun {⟨𝐴, 𝐵⟩})
2 opex 5422 . . 3 𝐴, 𝐵⟩ ∈ V
32snid 4623 . 2 𝐴, 𝐵⟩ ∈ {⟨𝐴, 𝐵⟩}
4 funopfv 6895 . 2 (Fun {⟨𝐴, 𝐵⟩} → (⟨𝐴, 𝐵⟩ ∈ {⟨𝐴, 𝐵⟩} → ({⟨𝐴, 𝐵⟩}‘𝐴) = 𝐵))
51, 3, 4mpisyl 21 1 ((𝐴𝑉𝐵𝑊) → ({⟨𝐴, 𝐵⟩}‘𝐴) = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397   = wceq 1542  wcel 2107  {csn 4587  cop 4593  Fun wfun 6491  cfv 6497
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-12 2172  ax-ext 2704  ax-sep 5257  ax-nul 5264  ax-pr 5385
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-ral 3062  df-rex 3071  df-rab 3407  df-v 3446  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  df-br 5107  df-opab 5169  df-id 5532  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-iota 6449  df-fun 6499  df-fv 6505
This theorem is referenced by:  fvsn  7128  fvsnun1  7129  fsnunfv  7134  fvpr1g  7137  fvpr2gOLD  7139  fsnex  7230  suppsnop  8110  mapsnend  8983  enfixsn  9028  axdc3lem4  10394  fseq1p1m1  13521  1fv  13566  s1fv  14504  sumsnf  15633  prodsn  15850  prodsnf  15852  seq1st  16452  vdwlem8  16865  setsid  17085  mgm1  18518  sgrp1  18560  mnd1  18602  mnd1id  18603  gsumws1  18653  grp1  18859  dprdsn  19820  ring1  20031  ixpsnbasval  20695  frgpcyg  20996  mat1dimscm  21840  mat1dimmul  21841  mat1rhmelval  21845  m1detdiag  21962  pt1hmeo  23173  noextenddif  27032  noextendlt  27033  noextendgt  27034  1loopgrvd0  28494  1hevtxdg0  28495  1hevtxdg1  28496  1egrvtxdg1  28499  wlkl0  29353  actfunsnrndisj  33275  reprsuc  33285  breprexplema  33300  cvmliftlem7  33942  cvmliftlem13  33947  bj-fununsn2  35771  sticksstones9  40608  sticksstones11  40610  metakunt20  40642  frlmsnic  40771  sumsnd  43319  ovnovollem1  44983  nnsum3primesprm  46068  lincvalsng  46583  snlindsntorlem  46637  lmod1lem2  46655  lmod1lem3  46656  0aryfvalelfv  46807  1arympt1fv  46811
  Copyright terms: Public domain W3C validator