Theorem fvsng 7200

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2108  {csn 4626  ⟨cop 4632  Fun wfun 6555  ‘cfv 6561

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 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-id 5578  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-iota 6514  df-fun 6563  df-fv 6569

This theorem is referenced by:  fvsn  7201  fvsnun1  7202  fsnunfv  7207  fvpr1g  7210  fsnex  7303  suppsnop  8203  mapsnend  9076  enfixsn  9121  axdc3lem4  10493  fseq1p1m1  13638  1fv  13687  s1fv  14648  sumsnf  15779  prodsn  15998  prodsnf  16000  seq1st  16608  vdwlem8  17026  setsid  17244  mgm1  18671  sgrp1  18742  mnd1  18792  mnd1id  18793  gsumws1  18851  grp1  19065  dprdsn  20056  ring1  20307  ixpsnbasval  21215  frgpcyg  21592  mat1dimscm  22481  mat1dimmul  22482  mat1rhmelval  22486  m1detdiag  22603  pt1hmeo  23814  noextenddif  27713  noextendlt  27714  noextendgt  27715  1loopgrvd0  29522  1hevtxdg0  29523  1hevtxdg1  29524  1egrvtxdg1  29527  wlkl0  30386  actfunsnrndisj  34620  reprsuc  34630  breprexplema  34645  cvmliftlem7  35296  cvmliftlem13  35301  bj-fununsn2  37255  sticksstones9  42155  sticksstones11  42157  metakunt20  42225  frlmsnic  42550  sumsnd  45031  ovnovollem1  46671  nnsum3primesprm  47777  lincvalsng  48333  snlindsntorlem  48387  lmod1lem2  48405  lmod1lem3  48406  0aryfvalelfv  48556  1arympt1fv  48560