Theorem fvsng 7182

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2145  {csn 4587  ⟨cop 4593  Fun wfun 6531  ‘cfv 6537

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-12 2215  ax-ext 2734  ax-sep 5255  ax-pr 5402

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-ral 3079  df-rex 3089  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-opab 5172  df-id 5554  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-iota 6493  df-fun 6539  df-fv 6545

This theorem is used by:  fvsn  7183  fvsnun1  7184  fsnunfv  7189  fvpr1g  7192  fsnex  7288  suppsnop  8180  mapsnend  9047  enfixsn  9088  axdc3lem4  10459  fseq1p1m1  13657  1fv  13706  s1fv  14682  sumsnf  15833  prodsn  16055  prodsnf  16057  seq1st  16667  vdwlem8  17086  setsid  17305  mgm1  18756  sgrp1  18837  mnd1  18892  mnd1id  18893  gsumws1  18953  grp1  19176  dprdsn  20171  ring1  20458  ixpsnbasval  21398  frgpcyg  21792  mat1dimscm  22703  mat1dimmul  22704  mat1rhmelval  22708  m1detdiag  22825  pt1hmeo  24038  noextenddif  27912  noextendlt  27913  noextendgt  27914  1loopgrvd0  29972  1hevtxdg0  29973  1hevtxdg1  29974  1egrvtxdg1  29977  wlkl0  30855  0mplrim  34032  selvply1rhmlemb  34037  actfunsnrndisj  35121  reprsuc  35131  breprexplema  35146  cvmliftlem7  35878  cvmliftlem13  35883  bj-fununsn2  38014  sticksstones9  43028  sticksstones11  43030  frlmsnic  43430  sumsnd  45868  ovnovollem1  47492  nnsum3primesprm  48714  lincvalsng  49354  snlindsntorlem  49408  lmod1lem2  49426  lmod1lem3  49427  0aryfvalelfv  49573  1arympt1fv  49577  ovsng  49794