Theorem fvsng 7128

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114  {csn 4568  ⟨cop 4574  Fun wfun 6486  ‘cfv 6492

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-12 2185  ax-ext 2709  ax-sep 5231  ax-pr 5370

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-iota 6448  df-fun 6494  df-fv 6500

This theorem is referenced by:  fvsn  7129  fvsnun1  7130  fsnunfv  7135  fvpr1g  7138  fsnex  7231  suppsnop  8121  mapsnend  8976  enfixsn  9017  axdc3lem4  10366  fseq1p1m1  13543  1fv  13592  s1fv  14564  sumsnf  15696  prodsn  15918  prodsnf  15920  seq1st  16531  vdwlem8  16950  setsid  17168  mgm1  18617  sgrp1  18688  mnd1  18738  mnd1id  18739  gsumws1  18797  grp1  19014  dprdsn  20004  ring1  20282  ixpsnbasval  21195  frgpcyg  21563  mat1dimscm  22450  mat1dimmul  22451  mat1rhmelval  22455  m1detdiag  22572  pt1hmeo  23781  noextenddif  27646  noextendlt  27647  noextendgt  27648  1loopgrvd0  29588  1hevtxdg0  29589  1hevtxdg1  29590  1egrvtxdg1  29593  wlkl0  30452  actfunsnrndisj  34765  reprsuc  34775  breprexplema  34790  cvmliftlem7  35489  cvmliftlem13  35494  bj-fununsn2  37584  sticksstones9  42607  sticksstones11  42609  frlmsnic  42999  sumsnd  45475  ovnovollem1  47102  nnsum3primesprm  48278  lincvalsng  48904  snlindsntorlem  48958  lmod1lem2  48976  lmod1lem3  48977  0aryfvalelfv  49123  1arympt1fv  49127  ovsng  49345