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

Theorem fvsng 5905
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 4052 . . . . 5  |-  ( a  =  A  ->  <. a ,  b >.  =  <. A ,  b >. )
21sneqd 3882 . . . 4  |-  ( a  =  A  ->  { <. a ,  b >. }  =  { <. A ,  b
>. } )
3 id 22 . . . 4  |-  ( a  =  A  ->  a  =  A )
42, 3fveq12d 5690 . . 3  |-  ( a  =  A  ->  ( { <. a ,  b
>. } `  a )  =  ( { <. A ,  b >. } `  A ) )
54eqeq1d 2445 . 2  |-  ( a  =  A  ->  (
( { <. a ,  b >. } `  a )  =  b  <-> 
( { <. A , 
b >. } `  A
)  =  b ) )
6 opeq2 4053 . . . . 5  |-  ( b  =  B  ->  <. A , 
b >.  =  <. A ,  B >. )
76sneqd 3882 . . . 4  |-  ( b  =  B  ->  { <. A ,  b >. }  =  { <. A ,  B >. } )
87fveq1d 5686 . . 3  |-  ( b  =  B  ->  ( { <. A ,  b
>. } `  A )  =  ( { <. A ,  B >. } `  A ) )
9 id 22 . . 3  |-  ( b  =  B  ->  b  =  B )
108, 9eqeq12d 2451 . 2  |-  ( b  =  B  ->  (
( { <. A , 
b >. } `  A
)  =  b  <->  ( { <. A ,  B >. } `
 A )  =  B ) )
11 vex 2969 . . 3  |-  a  e. 
_V
12 vex 2969 . . 3  |-  b  e. 
_V
1311, 12fvsn 5904 . 2  |-  ( {
<. a ,  b >. } `  a )  =  b
145, 10, 13vtocl2g 3027 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 3870   <.cop 3876   ` cfv 5411
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 2418  ax-sep 4406  ax-nul 4414  ax-pr 4524
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 2256  df-mo 2257  df-clab 2424  df-cleq 2430  df-clel 2433  df-nfc 2562  df-ne 2602  df-ral 2714  df-rex 2715  df-rab 2718  df-v 2968  df-sbc 3180  df-dif 3324  df-un 3326  df-in 3328  df-ss 3335  df-nul 3631  df-if 3785  df-sn 3871  df-pr 3873  df-op 3877  df-uni 4085  df-br 4286  df-opab 4344  df-id 4628  df-xp 4838  df-rel 4839  df-cnv 4840  df-co 4841  df-dm 4842  df-iota 5374  df-fun 5413  df-fv 5419
This theorem is referenced by:  fsnunfv  5911  fvpr1g  5916  fvpr2g  5917  suppsnop  6699  enfixsn  7412  axdc3lem4  8614  1fv  11524  fseq1p1m1  11526  s1fv  12290  sumsn  13209  seq1st  13738  vdwlem8  14041  setsid  14207  xpsc0  14490  xpsc1  14491  gsumws1  15506  dprdsn  16519  ixpsnbasval  17264  frgpcyg  17975  pt1hmeo  19348  vdgr1d  23518  vdgr1b  23519  vdgr1a  23521  eupap1  23542  cvmliftlem7  27128  cvmliftlem13  27133  prodsn  27420  sumsnd  29691  mat1dimscm  30772  mat1dimmul  30773  m1detdiag  30793  lincvalsng  30809  snlindsntorlem  30863  mnd1  30880  grp1  30881  rng1  30884  lmod1lem2  30889  lmod1lem3  30890
  Copyright terms: Public domain W3C validator