Theorem fvsng 6763

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

Syntax hints:   → wi 4   ∧ wa 387   = wceq 1507   ∈ wcel 2048  {csn 4439  ⟨cop 4445  Fun wfun 6180  ‘cfv 6186

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1964  ax-8 2050  ax-9 2057  ax-10 2077  ax-11 2091  ax-12 2104  ax-13 2299  ax-ext 2747  ax-sep 5058  ax-nul 5065  ax-pr 5184

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2014  df-mo 2544  df-eu 2580  df-clab 2756  df-cleq 2768  df-clel 2843  df-nfc 2915  df-ral 3090  df-rex 3091  df-rab 3094  df-v 3414  df-sbc 3681  df-dif 3831  df-un 3833  df-in 3835  df-ss 3842  df-nul 4178  df-if 4349  df-sn 4440  df-pr 4442  df-op 4446  df-uni 4711  df-br 4928  df-opab 4990  df-id 5309  df-xp 5410  df-rel 5411  df-cnv 5412  df-co 5413  df-dm 5414  df-iota 6150  df-fun 6188  df-fv 6194

This theorem is referenced by:  fvsn  6764  fvsnun1  6767  fsnunfv  6774  fvpr1g  6779  fvpr2g  6780  fsnex  6862  suppsnop  7644  mapsnend  8381  enfixsn  8418  axdc3lem4  9669  fseq1p1m1  12794  1fv  12839  s1fv  13767  sumsnf  14953  prodsn  15170  prodsnf  15172  seq1st  15765  vdwlem8  16174  setsid  16388  xpsc0  16683  xpsc1  16684  mgm1  17719  sgrp1  17755  mnd1  17793  mnd1id  17794  gsumws1  17838  grp1  17987  dprdsn  18902  ring1  19069  ixpsnbasval  19697  frgpcyg  20416  mat1dimscm  20782  mat1dimmul  20783  mat1rhmelval  20787  m1detdiag  20904  pt1hmeo  22112  1loopgrvd0  26983  1hevtxdg0  26984  1hevtxdg1  26985  1egrvtxdg1  26988  wlkl0  27914  actfunsnrndisj  31515  reprsuc  31525  breprexplema  31540  cvmliftlem7  32113  cvmliftlem13  32118  noextenddif  32666  noextendlt  32667  noextendgt  32668  bj-fununsn2  33970  frlmsnic  38564  sumsnd  40679  ovnovollem1  42348  nnsum3primesprm  43297  lincvalsng  43812  snlindsntorlem  43866  lmod1lem2  43884  lmod1lem3  43885