MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  fvsng Structured version   Unicode version

Theorem fvsng 6086
Description: The value of a singleton of an ordered pair is the second member. (Contributed by NM, 26-Oct-2012.)
Assertion
Ref Expression
fvsng  |-  ( ( A  e.  V  /\  B  e.  W )  ->  ( { <. A ,  B >. } `  A
)  =  B )

Proof of Theorem fvsng
Dummy variables  a 
b are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 opeq1 4206 . . . . 5  |-  ( a  =  A  ->  <. a ,  b >.  =  <. A ,  b >. )
21sneqd 4032 . . . 4  |-  ( a  =  A  ->  { <. a ,  b >. }  =  { <. A ,  b
>. } )
3 id 22 . . . 4  |-  ( a  =  A  ->  a  =  A )
42, 3fveq12d 5863 . . 3  |-  ( a  =  A  ->  ( { <. a ,  b
>. } `  a )  =  ( { <. A ,  b >. } `  A ) )
54eqeq1d 2462 . 2  |-  ( a  =  A  ->  (
( { <. a ,  b >. } `  a )  =  b  <-> 
( { <. A , 
b >. } `  A
)  =  b ) )
6 opeq2 4207 . . . . 5  |-  ( b  =  B  ->  <. A , 
b >.  =  <. A ,  B >. )
76sneqd 4032 . . . 4  |-  ( b  =  B  ->  { <. A ,  b >. }  =  { <. A ,  B >. } )
87fveq1d 5859 . . 3  |-  ( b  =  B  ->  ( { <. A ,  b
>. } `  A )  =  ( { <. A ,  B >. } `  A ) )
9 id 22 . . 3  |-  ( b  =  B  ->  b  =  B )
108, 9eqeq12d 2482 . 2  |-  ( b  =  B  ->  (
( { <. A , 
b >. } `  A
)  =  b  <->  ( { <. A ,  B >. } `
 A )  =  B ) )
11 vex 3109 . . 3  |-  a  e. 
_V
12 vex 3109 . . 3  |-  b  e. 
_V
1311, 12fvsn 6085 . 2  |-  ( {
<. a ,  b >. } `  a )  =  b
145, 10, 13vtocl2g 3168 1  |-  ( ( A  e.  V  /\  B  e.  W )  ->  ( { <. A ,  B >. } `  A
)  =  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    = wceq 1374    e. wcel 1762   {csn 4020   <.cop 4026   ` cfv 5579
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-9 1766  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438  ax-sep 4561  ax-nul 4569  ax-pr 4679
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 970  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-eu 2272  df-mo 2273  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-ne 2657  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3108  df-sbc 3325  df-dif 3472  df-un 3474  df-in 3476  df-ss 3483  df-nul 3779  df-if 3933  df-sn 4021  df-pr 4023  df-op 4027  df-uni 4239  df-br 4441  df-opab 4499  df-id 4788  df-xp 4998  df-rel 4999  df-cnv 5000  df-co 5001  df-dm 5002  df-iota 5542  df-fun 5581  df-fv 5587
This theorem is referenced by:  fsnunfv  6092  fvpr1g  6097  fvpr2g  6098  suppsnop  6905  enfixsn  7616  axdc3lem4  8822  fseq1p1m1  11741  1fv  11778  s1fv  12569  sumsn  13512  seq1st  14048  vdwlem8  14354  setsid  14520  xpsc0  14804  xpsc1  14805  gsumws1  15823  dprdsn  16866  ixpsnbasval  17631  frgpcyg  18372  mat1dimscm  18737  mat1dimmul  18738  mat1rhmelval  18742  m1detdiag  18859  pt1hmeo  20035  vdgr1d  24565  vdgr1b  24566  vdgr1a  24568  eupap1  24638  cvmliftlem7  28362  cvmliftlem13  28367  prodsn  28655  sumsnd  30934  lincvalsng  31965  snlindsntorlem  32019  mnd1  32036  grp1  32037  rng1  32040  lmod1lem2  32045  lmod1lem3  32046
  Copyright terms: Public domain W3C validator