Theorem fvsng 7185

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 6591	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → Fun {⟨𝐴, 𝐵⟩})
2		opex 5431	. . 3 ⊢ ⟨𝐴, 𝐵⟩ ∈ V
3	2	snid 4619	. 2 ⊢ ⟨𝐴, 𝐵⟩ ∈ {⟨𝐴, 𝐵⟩}
4		funopfv 6934	. 2 ⊢ (Fun {⟨𝐴, 𝐵⟩} → (⟨𝐴, 𝐵⟩ ∈ {⟨𝐴, 𝐵⟩} → ({⟨𝐴, 𝐵⟩}‘𝐴) = 𝐵))
5	1, 3, 4	mpisyl 22	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ({⟨𝐴, 𝐵⟩}‘𝐴) = 𝐵)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1569   ∈ wcel 2144  {csn 4584  ⟨cop 4834  Fun wfun 6532  ‘cfv 6538

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-pr 5390

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-opab 5167  df-id 5545  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-iota 6494  df-fun 6540  df-fv 6546

This theorem is used by:  fvsn  7186  fvsnun1  7187  fsnunfv  7192  fvpr1g  7195  fsnex  7291  suppsnop  8198  mapsnend  9067  enfixsn  9108  axdc3lem4  10534  fseq1p1m1  13735  1fv  13784  s1fv  14762  sumsnf  15914  prodsn  16134  prodsnf  16136  seq1st  16751  vdwlem8  17171  setsid  17390  mgm1  18841  sgrp1  18923  mnd1  18978  mnd1id  18979  gsumws1  19039  grp1  19262  dprdsn  20257  ring1  20546  ixpsnbasval  21488  frgpcyg  21884  mat1dimscm  22795  mat1dimmul  22796  mat1rhmelval  22800  m1detdiag  22917  pt1hmeo  24130  noextenddif  28030  noextendlt  28031  noextendgt  28032  1loopgrvd0  30090  1hevtxdg0  30091  1hevtxdg1  30092  1egrvtxdg1  30095  wlkl0  30973  0mplrim  34192  selvply1rhmlemb  34197  actfunsnrndisj  35280  reprsuc  35290  breprexplema  35305  cvmliftlem7  36142  cvmliftlem13  36147  bj-fununsn2  38268  sticksstones9  43297  sticksstones11  43299  frlmsnic  43697  sumsnd  46136  ovnovollem1  47759  nnsum3primesprm  48981  lincvalsng  49621  snlindsntorlem  49675  lmod1lem2  49693  lmod1lem3  49694  0aryfvalelfv  49840  1arympt1fv  49844  ovsng  50062