Theorem fvsng 7180

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

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1570   ∈ wcel 2143  {csn 4590  ⟨cop 4596  Fun wfun 6532  ‘cfv 6538

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-12 2213  ax-ext 2735  ax-sep 5258  ax-pr 5406

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4489  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-br 5111  df-opab 5175  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-iota 6494  df-fun 6540  df-fv 6546

This theorem is referenced by:  fvsn  7181  fvsnun1  7182  fsnunfv  7187  fvpr1g  7190  fsnex  7283  suppsnop  8175  mapsnend  9034  enfixsn  9075  axdc3lem4  10438  fseq1p1m1  13628  1fv  13677  s1fv  14650  sumsnf  15796  prodsn  16018  prodsnf  16020  seq1st  16630  vdwlem8  17049  setsid  17268  mgm1  18717  sgrp1  18788  mnd1  18838  mnd1id  18839  gsumws1  18898  grp1  19114  dprdsn  20109  ring1  20394  ixpsnbasval  21310  frgpcyg  21704  mat1dimscm  22613  mat1dimmul  22614  mat1rhmelval  22618  m1detdiag  22735  pt1hmeo  23944  noextenddif  27810  noextendlt  27811  noextendgt  27812  1loopgrvd0  29832  1hevtxdg0  29833  1hevtxdg1  29834  1egrvtxdg1  29837  wlkl0  30696  0mplrim  33882  selvply1rhmlemb  33887  actfunsnrndisj  34970  reprsuc  34980  breprexplema  34995  cvmliftlem7  35761  cvmliftlem13  35766  bj-fununsn2  37876  sticksstones9  42899  sticksstones11  42901  frlmsnic  43288  sumsnd  45726  ovnovollem1  47350  nnsum3primesprm  48532  lincvalsng  49173  snlindsntorlem  49227  lmod1lem2  49245  lmod1lem3  49246  0aryfvalelfv  49392  1arympt1fv  49396  ovsng  49613