Theorem fvsng 7154

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109  {csn 4589  ⟨cop 4595  Fun wfun 6505  ‘cfv 6511

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 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-12 2178  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387

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 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-id 5533  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-iota 6464  df-fun 6513  df-fv 6519

This theorem is referenced by:  fvsn  7155  fvsnun1  7156  fsnunfv  7161  fvpr1g  7164  fsnex  7258  suppsnop  8157  mapsnend  9007  enfixsn  9050  axdc3lem4  10406  fseq1p1m1  13559  1fv  13608  s1fv  14575  sumsnf  15709  prodsn  15928  prodsnf  15930  seq1st  16541  vdwlem8  16959  setsid  17177  mgm1  18585  sgrp1  18656  mnd1  18706  mnd1id  18707  gsumws1  18765  grp1  18979  dprdsn  19968  ring1  20219  ixpsnbasval  21115  frgpcyg  21483  mat1dimscm  22362  mat1dimmul  22363  mat1rhmelval  22367  m1detdiag  22484  pt1hmeo  23693  noextenddif  27580  noextendlt  27581  noextendgt  27582  1loopgrvd0  29432  1hevtxdg0  29433  1hevtxdg1  29434  1egrvtxdg1  29437  wlkl0  30296  actfunsnrndisj  34596  reprsuc  34606  breprexplema  34621  cvmliftlem7  35278  cvmliftlem13  35283  bj-fununsn2  37242  sticksstones9  42142  sticksstones11  42144  frlmsnic  42528  sumsnd  45020  ovnovollem1  46654  nnsum3primesprm  47791  lincvalsng  48405  snlindsntorlem  48459  lmod1lem2  48477  lmod1lem3  48478  0aryfvalelfv  48624  1arympt1fv  48628  ovsng  48846