Theorem fvsng 6488

Description: The value of a singleton of an ordered pair is the second member. (Contributed by NM, 26-Oct-2012.)

Assertion

Ref	Expression
fvsng	⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ({⟨𝐴, 𝐵⟩}‘𝐴) = 𝐵)

Proof of Theorem fvsng

Dummy variables 𝑎 𝑏 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		opeq1 4433	. . . . 5 ⊢ (𝑎 = 𝐴 → ⟨𝑎, 𝑏⟩ = ⟨𝐴, 𝑏⟩)
2	1	sneqd 4222	. . . 4 ⊢ (𝑎 = 𝐴 → {⟨𝑎, 𝑏⟩} = {⟨𝐴, 𝑏⟩})
3		id 22	. . . 4 ⊢ (𝑎 = 𝐴 → 𝑎 = 𝐴)
4	2, 3	fveq12d 6235	. . 3 ⊢ (𝑎 = 𝐴 → ({⟨𝑎, 𝑏⟩}‘𝑎) = ({⟨𝐴, 𝑏⟩}‘𝐴))
5	4	eqeq1d 2653	. 2 ⊢ (𝑎 = 𝐴 → (({⟨𝑎, 𝑏⟩}‘𝑎) = 𝑏 ↔ ({⟨𝐴, 𝑏⟩}‘𝐴) = 𝑏))
6		opeq2 4434	. . . . 5 ⊢ (𝑏 = 𝐵 → ⟨𝐴, 𝑏⟩ = ⟨𝐴, 𝐵⟩)
7	6	sneqd 4222	. . . 4 ⊢ (𝑏 = 𝐵 → {⟨𝐴, 𝑏⟩} = {⟨𝐴, 𝐵⟩})
8	7	fveq1d 6231	. . 3 ⊢ (𝑏 = 𝐵 → ({⟨𝐴, 𝑏⟩}‘𝐴) = ({⟨𝐴, 𝐵⟩}‘𝐴))
9		id 22	. . 3 ⊢ (𝑏 = 𝐵 → 𝑏 = 𝐵)
10	8, 9	eqeq12d 2666	. 2 ⊢ (𝑏 = 𝐵 → (({⟨𝐴, 𝑏⟩}‘𝐴) = 𝑏 ↔ ({⟨𝐴, 𝐵⟩}‘𝐴) = 𝐵))
11		vex 3234	. . 3 ⊢ 𝑎 ∈ V
12		vex 3234	. . 3 ⊢ 𝑏 ∈ V
13	11, 12	fvsn 6487	. 2 ⊢ ({⟨𝑎, 𝑏⟩}‘𝑎) = 𝑏
14	5, 10, 13	vtocl2g 3301	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ({⟨𝐴, 𝐵⟩}‘𝐴) = 𝐵)

Syntax hints:   → wi 4   ∧ wa 383   = wceq 1523   ∈ wcel 2030  {csn 4210  ⟨cop 4216  ‘cfv 5926

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pr 4936

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ral 2946  df-rex 2947  df-rab 2950  df-v 3233  df-sbc 3469  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-br 4686  df-opab 4746  df-id 5053  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-iota 5889  df-fun 5928  df-fv 5934

This theorem is referenced by:  fsnunfv  6494  fvpr1g  6499  fvpr2g  6500  fsnex  6578  suppsnop  7354  enfixsn  8110  axdc3lem4  9313  fseq1p1m1  12452  1fv  12497  s1fv  13427  sumsnf  14517  sumsn  14519  prodsn  14736  prodsnf  14738  seq1st  15331  vdwlem8  15739  setsid  15961  xpsc0  16267  xpsc1  16268  mgm1  17304  sgrp1  17340  mnd1  17378  mnd1id  17379  gsumws1  17423  grp1  17569  dprdsn  18481  ring1  18648  ixpsnbasval  19257  frgpcyg  19970  mat1dimscm  20329  mat1dimmul  20330  mat1rhmelval  20334  m1detdiag  20451  pt1hmeo  21657  1loopgrvd0  26456  1hevtxdg0  26457  1hevtxdg1  26458  1egrvtxdg1  26461  actfunsnrndisj  30811  reprsuc  30821  breprexplema  30836  cvmliftlem7  31399  cvmliftlem13  31404  noextenddif  31946  noextendlt  31947  noextendgt  31948  sumsnd  39499  mapsnend  39705  ovnovollem1  41191  nnsum3primesprm  42003  lincvalsng  42530  snlindsntorlem  42584  lmod1lem2  42602  lmod1lem3  42603