Theorem fvsng 7208

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2147  {csn 4588  ⟨cop 4838  Fun wfun 6552  ‘cfv 6558

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-12 2216  ax-ext 2735  ax-sep 5252  ax-pr 5395

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 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-opab 5171  df-id 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-iota 6512  df-fun 6560  df-fv 6566

This theorem is used by:  fvsn  7209  fvsnun1  7210  fsnunfv  7215  fvpr1g  7218  fsnex  7314  suppsnop  8223  mapsnend  9092  enfixsn  9133  axdc3lem4  10558  fseq1p1m1  13759  1fv  13808  s1fv  14786  sumsnf  15938  prodsn  16158  prodsnf  16160  seq1st  16775  vdwlem8  17195  setsid  17414  mgm1  18865  sgrp1  18947  mnd1  19002  mnd1id  19003  gsumws1  19063  grp1  19286  dprdsn  20282  ring1  20571  ixpsnbasval  21513  frgpcyg  21909  mat1dimscm  22820  mat1dimmul  22821  mat1rhmelval  22825  m1detdiag  22942  pt1hmeo  24155  noextenddif  28055  noextendlt  28056  noextendgt  28057  1loopgrvd0  30115  1hevtxdg0  30116  1hevtxdg1  30117  1egrvtxdg1  30120  wlkl0  30998  0mplrim  34216  selvply1rhmlemb  34221  actfunsnrndisj  35304  reprsuc  35314  breprexplema  35329  cvmliftlem7  36223  cvmliftlem13  36228  bj-fununsn2  38367  sticksstones9  43396  sticksstones11  43398  frlmsnic  43797  sumsnd  46248  ovnovollem1  47871  nnsum3primesprm  49093  lincvalsng  49733  snlindsntorlem  49787  lmod1lem2  49805  lmod1lem3  49806  0aryfvalelfv  49952  1arympt1fv  49956  ovsng  50174