Theorem fvsng 7135

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114  {csn 4567  ⟨cop 4573  Fun wfun 6492  ‘cfv 6498

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 2708  ax-sep 5231  ax-pr 5375

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 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-opab 5148  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-iota 6454  df-fun 6500  df-fv 6506

This theorem is referenced by:  fvsn  7136  fvsnun1  7137  fsnunfv  7142  fvpr1g  7145  fsnex  7238  suppsnop  8128  mapsnend  8983  enfixsn  9024  axdc3lem4  10375  fseq1p1m1  13552  1fv  13601  s1fv  14573  sumsnf  15705  prodsn  15927  prodsnf  15929  seq1st  16540  vdwlem8  16959  setsid  17177  mgm1  18626  sgrp1  18697  mnd1  18747  mnd1id  18748  gsumws1  18806  grp1  19023  dprdsn  20013  ring1  20291  ixpsnbasval  21203  frgpcyg  21553  mat1dimscm  22440  mat1dimmul  22441  mat1rhmelval  22445  m1detdiag  22562  pt1hmeo  23771  noextenddif  27632  noextendlt  27633  noextendgt  27634  1loopgrvd0  29573  1hevtxdg0  29574  1hevtxdg1  29575  1egrvtxdg1  29578  wlkl0  30437  actfunsnrndisj  34749  reprsuc  34759  breprexplema  34774  cvmliftlem7  35473  cvmliftlem13  35478  bj-fununsn2  37568  sticksstones9  42593  sticksstones11  42595  frlmsnic  42985  sumsnd  45457  ovnovollem1  47084  nnsum3primesprm  48266  lincvalsng  48892  snlindsntorlem  48946  lmod1lem2  48964  lmod1lem3  48965  0aryfvalelfv  49111  1arympt1fv  49115  ovsng  49333