Theorem fvsng 7061

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

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1539   ∈ wcel 2107  {csn 4562  ⟨cop 4568  Fun wfun 6431  ‘cfv 6437

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2710  ax-sep 5224  ax-nul 5231  ax-pr 5353

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-ral 3070  df-rex 3071  df-rab 3074  df-v 3435  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4258  df-if 4461  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4841  df-br 5076  df-opab 5138  df-id 5490  df-xp 5596  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-iota 6395  df-fun 6439  df-fv 6445

This theorem is referenced by:  fvsn  7062  fvsnun1  7063  fsnunfv  7068  fvpr1g  7071  fvpr2gOLD  7073  fsnex  7164  suppsnop  8003  mapsnend  8835  enfixsn  8877  axdc3lem4  10218  fseq1p1m1  13339  1fv  13384  s1fv  14324  sumsnf  15464  prodsn  15681  prodsnf  15683  seq1st  16285  vdwlem8  16698  setsid  16918  mgm1  18351  sgrp1  18393  mnd1  18435  mnd1id  18436  gsumws1  18485  grp1  18691  dprdsn  19648  ring1  19850  ixpsnbasval  20489  frgpcyg  20790  mat1dimscm  21633  mat1dimmul  21634  mat1rhmelval  21638  m1detdiag  21755  pt1hmeo  22966  1loopgrvd0  27880  1hevtxdg0  27881  1hevtxdg1  27882  1egrvtxdg1  27885  wlkl0  28740  actfunsnrndisj  32594  reprsuc  32604  breprexplema  32619  cvmliftlem7  33262  cvmliftlem13  33267  noextenddif  33880  noextendlt  33881  noextendgt  33882  bj-fununsn2  35434  sticksstones9  40117  sticksstones11  40119  metakunt20  40151  frlmsnic  40270  sumsnd  42576  ovnovollem1  44201  nnsum3primesprm  45253  lincvalsng  45768  snlindsntorlem  45822  lmod1lem2  45840  lmod1lem3  45841  0aryfvalelfv  45992  1arympt1fv  45996