Theorem fvsng 7177

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2145  {csn 4584  ⟨cop 4590  Fun wfun 6525  ‘cfv 6531

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-pr 5391

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 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-iota 6487  df-fun 6533  df-fv 6539

This theorem is used by:  fvsn  7178  fvsnun1  7179  fsnunfv  7184  fvpr1g  7187  fsnex  7283  suppsnop  8179  mapsnend  9048  enfixsn  9089  axdc3lem4  10512  fseq1p1m1  13712  1fv  13761  s1fv  14738  sumsnf  15889  prodsn  16109  prodsnf  16111  seq1st  16726  vdwlem8  17146  setsid  17365  mgm1  18816  sgrp1  18898  mnd1  18953  mnd1id  18954  gsumws1  19014  grp1  19237  dprdsn  20232  ring1  20521  ixpsnbasval  21463  frgpcyg  21859  mat1dimscm  22770  mat1dimmul  22771  mat1rhmelval  22775  m1detdiag  22892  pt1hmeo  24105  noextenddif  28007  noextendlt  28008  noextendgt  28009  1loopgrvd0  30067  1hevtxdg0  30068  1hevtxdg1  30069  1egrvtxdg1  30072  wlkl0  30950  0mplrim  34128  selvply1rhmlemb  34133  actfunsnrndisj  35217  reprsuc  35227  breprexplema  35242  cvmliftlem7  36025  cvmliftlem13  36030  bj-fununsn2  38143  sticksstones9  43172  sticksstones11  43174  frlmsnic  43566  sumsnd  45986  ovnovollem1  47610  nnsum3primesprm  48832  lincvalsng  49472  snlindsntorlem  49526  lmod1lem2  49544  lmod1lem3  49545  0aryfvalelfv  49691  1arympt1fv  49695  ovsng  49912