Theorem fvsng 7171

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2108  {csn 4601  ⟨cop 4607  Fun wfun 6524  ‘cfv 6530

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-12 2177  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pr 5402

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-opab 5182  df-id 5548  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-iota 6483  df-fun 6532  df-fv 6538

This theorem is referenced by:  fvsn  7172  fvsnun1  7173  fsnunfv  7178  fvpr1g  7181  fsnex  7275  suppsnop  8175  mapsnend  9048  enfixsn  9093  axdc3lem4  10465  fseq1p1m1  13613  1fv  13662  s1fv  14626  sumsnf  15757  prodsn  15976  prodsnf  15978  seq1st  16588  vdwlem8  17006  setsid  17224  mgm1  18634  sgrp1  18705  mnd1  18755  mnd1id  18756  gsumws1  18814  grp1  19028  dprdsn  20017  ring1  20268  ixpsnbasval  21164  frgpcyg  21532  mat1dimscm  22411  mat1dimmul  22412  mat1rhmelval  22416  m1detdiag  22533  pt1hmeo  23742  noextenddif  27630  noextendlt  27631  noextendgt  27632  1loopgrvd0  29430  1hevtxdg0  29431  1hevtxdg1  29432  1egrvtxdg1  29435  wlkl0  30294  actfunsnrndisj  34583  reprsuc  34593  breprexplema  34608  cvmliftlem7  35259  cvmliftlem13  35264  bj-fununsn2  37218  sticksstones9  42113  sticksstones11  42115  metakunt20  42183  frlmsnic  42510  sumsnd  44998  ovnovollem1  46633  nnsum3primesprm  47752  lincvalsng  48340  snlindsntorlem  48394  lmod1lem2  48412  lmod1lem3  48413  0aryfvalelfv  48563  1arympt1fv  48567  ovsng  48782