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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   ∈ wcel 2113  {csn 4575  ⟨cop 4581  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 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-12 2182  ax-ext 2705  ax-sep 5236  ax-nul 5246  ax-pr 5372

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-ral 3049  df-rex 3058  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-ss 3915  df-nul 4283  df-if 4475  df-sn 4576  df-pr 4578  df-op 4582  df-uni 4859  df-br 5094  df-opab 5156  df-id 5514  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-iota 6442  df-fun 6488  df-fv 6494

This theorem is referenced by:  fvsn  7121  fvsnun1  7122  fsnunfv  7127  fvpr1g  7130  fsnex  7223  suppsnop  8114  mapsnend  8965  enfixsn  9006  axdc3lem4  10351  fseq1p1m1  13500  1fv  13549  s1fv  14520  sumsnf  15652  prodsn  15871  prodsnf  15873  seq1st  16484  vdwlem8  16902  setsid  17120  mgm1  18568  sgrp1  18639  mnd1  18689  mnd1id  18690  gsumws1  18748  grp1  18962  dprdsn  19952  ring1  20230  ixpsnbasval  21144  frgpcyg  21512  mat1dimscm  22391  mat1dimmul  22392  mat1rhmelval  22396  m1detdiag  22513  pt1hmeo  23722  noextenddif  27608  noextendlt  27609  noextendgt  27610  1loopgrvd0  29485  1hevtxdg0  29486  1hevtxdg1  29487  1egrvtxdg1  29490  wlkl0  30349  actfunsnrndisj  34639  reprsuc  34649  breprexplema  34664  cvmliftlem7  35356  cvmliftlem13  35361  bj-fununsn2  37319  sticksstones9  42267  sticksstones11  42269  frlmsnic  42658  sumsnd  45147  ovnovollem1  46778  nnsum3primesprm  47914  lincvalsng  48541  snlindsntorlem  48595  lmod1lem2  48613  lmod1lem3  48614  0aryfvalelfv  48760  1arympt1fv  48764  ovsng  48982