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

Theorem fvsng 6085
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 4159 . . . . 5  |-  ( a  =  A  ->  <. a ,  b >.  =  <. A ,  b >. )
21sneqd 3984 . . . 4  |-  ( a  =  A  ->  { <. a ,  b >. }  =  { <. A ,  b
>. } )
3 id 22 . . . 4  |-  ( a  =  A  ->  a  =  A )
42, 3fveq12d 5855 . . 3  |-  ( a  =  A  ->  ( { <. a ,  b
>. } `  a )  =  ( { <. A ,  b >. } `  A ) )
54eqeq1d 2404 . 2  |-  ( a  =  A  ->  (
( { <. a ,  b >. } `  a )  =  b  <-> 
( { <. A , 
b >. } `  A
)  =  b ) )
6 opeq2 4160 . . . . 5  |-  ( b  =  B  ->  <. A , 
b >.  =  <. A ,  B >. )
76sneqd 3984 . . . 4  |-  ( b  =  B  ->  { <. A ,  b >. }  =  { <. A ,  B >. } )
87fveq1d 5851 . . 3  |-  ( b  =  B  ->  ( { <. A ,  b
>. } `  A )  =  ( { <. A ,  B >. } `  A ) )
9 id 22 . . 3  |-  ( b  =  B  ->  b  =  B )
108, 9eqeq12d 2424 . 2  |-  ( b  =  B  ->  (
( { <. A , 
b >. } `  A
)  =  b  <->  ( { <. A ,  B >. } `
 A )  =  B ) )
11 vex 3062 . . 3  |-  a  e. 
_V
12 vex 3062 . . 3  |-  b  e. 
_V
1311, 12fvsn 6084 . 2  |-  ( {
<. a ,  b >. } `  a )  =  b
145, 10, 13vtocl2g 3121 1  |-  ( ( A  e.  V  /\  B  e.  W )  ->  ( { <. A ,  B >. } `  A
)  =  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367    = wceq 1405    e. wcel 1842   {csn 3972   <.cop 3978   ` cfv 5569
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-9 1846  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380  ax-sep 4517  ax-nul 4525  ax-pr 4630
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 976  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-eu 2242  df-mo 2243  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-ne 2600  df-ral 2759  df-rex 2760  df-rab 2763  df-v 3061  df-sbc 3278  df-dif 3417  df-un 3419  df-in 3421  df-ss 3428  df-nul 3739  df-if 3886  df-sn 3973  df-pr 3975  df-op 3979  df-uni 4192  df-br 4396  df-opab 4454  df-id 4738  df-xp 4829  df-rel 4830  df-cnv 4831  df-co 4832  df-dm 4833  df-iota 5533  df-fun 5571  df-fv 5577
This theorem is referenced by:  fsnunfv  6091  fvpr1g  6096  fvpr2g  6097  fsnex  6169  suppsnop  6916  enfixsn  7664  axdc3lem4  8865  fseq1p1m1  11807  1fv  11847  s1fv  12673  sumsn  13712  prodsn  13919  seq1st  14409  vdwlem8  14715  setsid  14884  xpsc0  15174  xpsc1  15175  mgm1  16208  sgrp1  16242  mnd1  16285  mnd1OLD  16286  mnd1id  16287  gsumws1  16331  grp1  16466  dprdsn  17403  ring1  17568  ixpsnbasval  18175  frgpcyg  18910  mat1dimscm  19269  mat1dimmul  19270  mat1rhmelval  19274  m1detdiag  19391  pt1hmeo  20599  vdgr1d  25320  vdgr1b  25321  vdgr1a  25323  eupap1  25393  cvmliftlem7  29588  cvmliftlem13  29593  sumsnd  36781  sumsnf  36938  prodsnf  36955  nnsum3primesprm  37838  lincvalsng  38528  snlindsntorlem  38582  lmod1lem2  38600  lmod1lem3  38601
  Copyright terms: Public domain W3C validator