Theorem fvsng 7120

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109  {csn 4579  ⟨cop 4585  Fun wfun 6480  ‘cfv 6486

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 5238  ax-nul 5248  ax-pr 5374

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 3397  df-v 3440  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-br 5096  df-opab 5158  df-id 5518  df-xp 5629  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-iota 6442  df-fun 6488  df-fv 6494

This theorem is referenced by:  fvsn  7121  fvsnun1  7122  fsnunfv  7127  fvpr1g  7130  fsnex  7224  suppsnop  8118  mapsnend  8968  enfixsn  9010  axdc3lem4  10366  fseq1p1m1  13519  1fv  13568  s1fv  14535  sumsnf  15668  prodsn  15887  prodsnf  15889  seq1st  16500  vdwlem8  16918  setsid  17136  mgm1  18550  sgrp1  18621  mnd1  18671  mnd1id  18672  gsumws1  18730  grp1  18944  dprdsn  19935  ring1  20213  ixpsnbasval  21130  frgpcyg  21498  mat1dimscm  22378  mat1dimmul  22379  mat1rhmelval  22383  m1detdiag  22500  pt1hmeo  23709  noextenddif  27596  noextendlt  27597  noextendgt  27598  1loopgrvd0  29468  1hevtxdg0  29469  1hevtxdg1  29470  1egrvtxdg1  29473  wlkl0  30329  actfunsnrndisj  34572  reprsuc  34582  breprexplema  34597  cvmliftlem7  35263  cvmliftlem13  35268  bj-fununsn2  37227  sticksstones9  42127  sticksstones11  42129  frlmsnic  42513  sumsnd  45004  ovnovollem1  46638  nnsum3primesprm  47775  lincvalsng  48402  snlindsntorlem  48456  lmod1lem2  48474  lmod1lem3  48475  0aryfvalelfv  48621  1arympt1fv  48625  ovsng  48843