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

Theorem fvsng 5915
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 4062 . . . . 5  |-  ( a  =  A  ->  <. a ,  b >.  =  <. A ,  b >. )
21sneqd 3892 . . . 4  |-  ( a  =  A  ->  { <. a ,  b >. }  =  { <. A ,  b
>. } )
3 id 22 . . . 4  |-  ( a  =  A  ->  a  =  A )
42, 3fveq12d 5700 . . 3  |-  ( a  =  A  ->  ( { <. a ,  b
>. } `  a )  =  ( { <. A ,  b >. } `  A ) )
54eqeq1d 2451 . 2  |-  ( a  =  A  ->  (
( { <. a ,  b >. } `  a )  =  b  <-> 
( { <. A , 
b >. } `  A
)  =  b ) )
6 opeq2 4063 . . . . 5  |-  ( b  =  B  ->  <. A , 
b >.  =  <. A ,  B >. )
76sneqd 3892 . . . 4  |-  ( b  =  B  ->  { <. A ,  b >. }  =  { <. A ,  B >. } )
87fveq1d 5696 . . 3  |-  ( b  =  B  ->  ( { <. A ,  b
>. } `  A )  =  ( { <. A ,  B >. } `  A ) )
9 id 22 . . 3  |-  ( b  =  B  ->  b  =  B )
108, 9eqeq12d 2457 . 2  |-  ( b  =  B  ->  (
( { <. A , 
b >. } `  A
)  =  b  <->  ( { <. A ,  B >. } `
 A )  =  B ) )
11 vex 2978 . . 3  |-  a  e. 
_V
12 vex 2978 . . 3  |-  b  e. 
_V
1311, 12fvsn 5914 . 2  |-  ( {
<. a ,  b >. } `  a )  =  b
145, 10, 13vtocl2g 3037 1  |-  ( ( A  e.  V  /\  B  e.  W )  ->  ( { <. A ,  B >. } `  A
)  =  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    = wceq 1369    e. wcel 1756   {csn 3880   <.cop 3886   ` cfv 5421
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4416  ax-nul 4424  ax-pr 4534
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2571  df-ne 2611  df-ral 2723  df-rex 2724  df-rab 2727  df-v 2977  df-sbc 3190  df-dif 3334  df-un 3336  df-in 3338  df-ss 3345  df-nul 3641  df-if 3795  df-sn 3881  df-pr 3883  df-op 3887  df-uni 4095  df-br 4296  df-opab 4354  df-id 4639  df-xp 4849  df-rel 4850  df-cnv 4851  df-co 4852  df-dm 4853  df-iota 5384  df-fun 5423  df-fv 5429
This theorem is referenced by:  fsnunfv  5921  fvpr1g  5926  fvpr2g  5927  suppsnop  6707  enfixsn  7423  axdc3lem4  8625  1fv  11535  fseq1p1m1  11537  s1fv  12301  sumsn  13220  seq1st  13749  vdwlem8  14052  setsid  14218  xpsc0  14501  xpsc1  14502  gsumws1  15520  dprdsn  16536  ixpsnbasval  17293  frgpcyg  18009  pt1hmeo  19382  vdgr1d  23576  vdgr1b  23577  vdgr1a  23579  eupap1  23600  cvmliftlem7  27183  cvmliftlem13  27188  prodsn  27476  sumsnd  29751  mat1dimscm  30874  mat1dimmul  30875  m1detdiag  30937  lincvalsng  30953  snlindsntorlem  31007  mnd1  31024  grp1  31025  rng1  31028  lmod1lem2  31033  lmod1lem3  31034
  Copyright terms: Public domain W3C validator