Theorem fvsng 7174

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

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1541   ∈ wcel 2106  {csn 4627  ⟨cop 4633  Fun wfun 6534  ‘cfv 6540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-12 2171  ax-ext 2703  ax-sep 5298  ax-nul 5305  ax-pr 5426

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-opab 5210  df-id 5573  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-iota 6492  df-fun 6542  df-fv 6548

This theorem is referenced by:  fvsn  7175  fvsnun1  7176  fsnunfv  7181  fvpr1g  7184  fvpr2gOLD  7186  fsnex  7277  suppsnop  8159  mapsnend  9032  enfixsn  9077  axdc3lem4  10444  fseq1p1m1  13571  1fv  13616  s1fv  14556  sumsnf  15685  prodsn  15902  prodsnf  15904  seq1st  16504  vdwlem8  16917  setsid  17137  mgm1  18573  sgrp1  18616  mnd1  18663  mnd1id  18664  gsumws1  18715  grp1  18926  dprdsn  19900  ring1  20115  ixpsnbasval  20824  frgpcyg  21120  mat1dimscm  21968  mat1dimmul  21969  mat1rhmelval  21973  m1detdiag  22090  pt1hmeo  23301  noextenddif  27160  noextendlt  27161  noextendgt  27162  1loopgrvd0  28750  1hevtxdg0  28751  1hevtxdg1  28752  1egrvtxdg1  28755  wlkl0  29609  actfunsnrndisj  33605  reprsuc  33615  breprexplema  33630  cvmliftlem7  34270  cvmliftlem13  34275  bj-fununsn2  36123  sticksstones9  40958  sticksstones11  40960  metakunt20  40992  frlmsnic  41107  sumsnd  43695  ovnovollem1  45358  nnsum3primesprm  46444  lincvalsng  47050  snlindsntorlem  47104  lmod1lem2  47122  lmod1lem3  47123  0aryfvalelfv  47274  1arympt1fv  47278