Theorem fvsng 7168

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

Step	Hyp	Ref	Expression
1		funsng 6576	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → Fun {⟨𝐴, 𝐵⟩})
2		opex 5436	. . 3 ⊢ ⟨𝐴, 𝐵⟩ ∈ V
3	2	snid 4624	. 2 ⊢ ⟨𝐴, 𝐵⟩ ∈ {⟨𝐴, 𝐵⟩}
4		funopfv 6920	. 2 ⊢ (Fun {⟨𝐴, 𝐵⟩} → (⟨𝐴, 𝐵⟩ ∈ {⟨𝐴, 𝐵⟩} → ({⟨𝐴, 𝐵⟩}‘𝐴) = 𝐵))
5	1, 3, 4	mpisyl 22	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ({⟨𝐴, 𝐵⟩}‘𝐴) = 𝐵)

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1563   ∈ wcel 2145  {csn 4585  ⟨cop 4591  Fun wfun 6519  ‘cfv 6525

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-10 2178  ax-12 2215  ax-ext 2737  ax-sep 5251  ax-pr 5395

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-nf 1807  df-sb 2094  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-ral 3080  df-rex 3090  df-rab 3418  df-v 3459  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-nul 4289  df-if 4484  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4869  df-br 5106  df-opab 5168  df-id 5547  df-xp 5658  df-rel 5659  df-cnv 5660  df-co 5661  df-dm 5662  df-iota 6481  df-fun 6527  df-fv 6533

This theorem is referenced by:  fvsn  7169  fvsnun1  7170  fsnunfv  7175  fvpr1g  7178  fsnex  7271  suppsnop  8162  mapsnend  9021  enfixsn  9062  axdc3lem4  10425  fseq1p1m1  13617  1fv  13666  s1fv  14638  sumsnf  15784  prodsn  16006  prodsnf  16008  seq1st  16619  vdwlem8  17038  setsid  17257  mgm1  18706  sgrp1  18777  mnd1  18827  mnd1id  18828  gsumws1  18887  grp1  19104  dprdsn  20099  ring1  20384  ixpsnbasval  21298  frgpcyg  21683  mat1dimscm  22593  mat1dimmul  22594  mat1rhmelval  22598  m1detdiag  22715  pt1hmeo  23924  noextenddif  27790  noextendlt  27791  noextendgt  27792  1loopgrvd0  29763  1hevtxdg0  29764  1hevtxdg1  29765  1egrvtxdg1  29768  wlkl0  30627  0mplrim  33821  selvply1rhmlemb  33826  actfunsnrndisj  34909  reprsuc  34919  breprexplema  34934  cvmliftlem7  35654  cvmliftlem13  35659  bj-fununsn2  37758  sticksstones9  42783  sticksstones11  42785  frlmsnic  43170  sumsnd  45604  ovnovollem1  47228  nnsum3primesprm  48410  lincvalsng  49047  snlindsntorlem  49101  lmod1lem2  49119  lmod1lem3  49120  0aryfvalelfv  49266  1arympt1fv  49270  ovsng  49487