Theorem fvsng 7136

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114  {csn 4582  ⟨cop 4588  Fun wfun 6494  ‘cfv 6500

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-12 2185  ax-ext 2709  ax-sep 5243  ax-pr 5379

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-id 5527  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-iota 6456  df-fun 6502  df-fv 6508

This theorem is referenced by:  fvsn  7137  fvsnun1  7138  fsnunfv  7143  fvpr1g  7146  fsnex  7239  suppsnop  8130  mapsnend  8985  enfixsn  9026  axdc3lem4  10375  fseq1p1m1  13526  1fv  13575  s1fv  14546  sumsnf  15678  prodsn  15897  prodsnf  15899  seq1st  16510  vdwlem8  16928  setsid  17146  mgm1  18595  sgrp1  18666  mnd1  18716  mnd1id  18717  gsumws1  18775  grp1  18989  dprdsn  19979  ring1  20257  ixpsnbasval  21172  frgpcyg  21540  mat1dimscm  22431  mat1dimmul  22432  mat1rhmelval  22436  m1detdiag  22553  pt1hmeo  23762  noextenddif  27648  noextendlt  27649  noextendgt  27650  1loopgrvd0  29590  1hevtxdg0  29591  1hevtxdg1  29592  1egrvtxdg1  29595  wlkl0  30454  actfunsnrndisj  34782  reprsuc  34792  breprexplema  34807  cvmliftlem7  35504  cvmliftlem13  35509  bj-fununsn2  37503  sticksstones9  42518  sticksstones11  42520  frlmsnic  42904  sumsnd  45380  ovnovollem1  47008  nnsum3primesprm  48144  lincvalsng  48770  snlindsntorlem  48824  lmod1lem2  48842  lmod1lem3  48843  0aryfvalelfv  48989  1arympt1fv  48993  ovsng  49211