Theorem fvsng 7214

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1537   ∈ wcel 2108  {csn 4648  ⟨cop 4654  Fun wfun 6567  ‘cfv 6573

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-12 2178  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pr 5447

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-opab 5229  df-id 5593  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-iota 6525  df-fun 6575  df-fv 6581

This theorem is referenced by:  fvsn  7215  fvsnun1  7216  fsnunfv  7221  fvpr1g  7224  fvpr2gOLD  7226  fsnex  7319  suppsnop  8219  mapsnend  9101  enfixsn  9147  axdc3lem4  10522  fseq1p1m1  13658  1fv  13704  s1fv  14658  sumsnf  15791  prodsn  16010  prodsnf  16012  seq1st  16618  vdwlem8  17035  setsid  17255  mgm1  18696  sgrp1  18767  mnd1  18814  mnd1id  18815  gsumws1  18873  grp1  19087  dprdsn  20080  ring1  20333  ixpsnbasval  21238  frgpcyg  21615  mat1dimscm  22502  mat1dimmul  22503  mat1rhmelval  22507  m1detdiag  22624  pt1hmeo  23835  noextenddif  27731  noextendlt  27732  noextendgt  27733  1loopgrvd0  29540  1hevtxdg0  29541  1hevtxdg1  29542  1egrvtxdg1  29545  wlkl0  30399  actfunsnrndisj  34582  reprsuc  34592  breprexplema  34607  cvmliftlem7  35259  cvmliftlem13  35264  bj-fununsn2  37220  sticksstones9  42111  sticksstones11  42113  metakunt20  42181  frlmsnic  42495  sumsnd  44926  ovnovollem1  46577  nnsum3primesprm  47664  lincvalsng  48145  snlindsntorlem  48199  lmod1lem2  48217  lmod1lem3  48218  0aryfvalelfv  48369  1arympt1fv  48373