Theorem fvsng 7034

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 6469	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → Fun {⟨𝐴, 𝐵⟩})
2		opex 5373	. . 3 ⊢ ⟨𝐴, 𝐵⟩ ∈ V
3	2	snid 4594	. 2 ⊢ ⟨𝐴, 𝐵⟩ ∈ {⟨𝐴, 𝐵⟩}
4		funopfv 6803	. 2 ⊢ (Fun {⟨𝐴, 𝐵⟩} → (⟨𝐴, 𝐵⟩ ∈ {⟨𝐴, 𝐵⟩} → ({⟨𝐴, 𝐵⟩}‘𝐴) = 𝐵))
5	1, 3, 4	mpisyl 21	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ({⟨𝐴, 𝐵⟩}‘𝐴) = 𝐵)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1539   ∈ wcel 2108  {csn 4558  ⟨cop 4564  Fun wfun 6412  ‘cfv 6418

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-opab 5133  df-id 5480  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-iota 6376  df-fun 6420  df-fv 6426

This theorem is referenced by:  fvsn  7035  fvsnun1  7036  fsnunfv  7041  fvpr1g  7044  fvpr2gOLD  7046  fsnex  7135  suppsnop  7965  mapsnend  8780  enfixsn  8821  axdc3lem4  10140  fseq1p1m1  13259  1fv  13304  s1fv  14243  sumsnf  15383  prodsn  15600  prodsnf  15602  seq1st  16204  vdwlem8  16617  setsid  16837  mgm1  18257  sgrp1  18299  mnd1  18341  mnd1id  18342  gsumws1  18391  grp1  18597  dprdsn  19554  ring1  19756  ixpsnbasval  20393  frgpcyg  20693  mat1dimscm  21532  mat1dimmul  21533  mat1rhmelval  21537  m1detdiag  21654  pt1hmeo  22865  1loopgrvd0  27774  1hevtxdg0  27775  1hevtxdg1  27776  1egrvtxdg1  27779  wlkl0  28632  actfunsnrndisj  32485  reprsuc  32495  breprexplema  32510  cvmliftlem7  33153  cvmliftlem13  33158  noextenddif  33798  noextendlt  33799  noextendgt  33800  bj-fununsn2  35352  sticksstones9  40038  sticksstones11  40040  metakunt20  40072  frlmsnic  40188  sumsnd  42458  ovnovollem1  44084  nnsum3primesprm  45130  lincvalsng  45645  snlindsntorlem  45699  lmod1lem2  45717  lmod1lem3  45718  0aryfvalelfv  45869  1arympt1fv  45873