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

Theorem fnsnfv 5772
Description: Singleton of function value. (Contributed by NM, 22-May-1998.)
Assertion
Ref Expression
fnsnfv  |-  ( ( F  Fn  A  /\  B  e.  A )  ->  { ( F `  B ) }  =  ( F " { B } ) )

Proof of Theorem fnsnfv
Dummy variable  y is distinct from all other variables.
StepHypRef Expression
1 eqcom 2445 . . . 4  |-  ( y  =  ( F `  B )  <->  ( F `  B )  =  y )
2 fnbrfvb 5753 . . . 4  |-  ( ( F  Fn  A  /\  B  e.  A )  ->  ( ( F `  B )  =  y  <-> 
B F y ) )
31, 2syl5bb 257 . . 3  |-  ( ( F  Fn  A  /\  B  e.  A )  ->  ( y  =  ( F `  B )  <-> 
B F y ) )
43abbidv 2563 . 2  |-  ( ( F  Fn  A  /\  B  e.  A )  ->  { y  |  y  =  ( F `  B ) }  =  { y  |  B F y } )
5 df-sn 3899 . . 3  |-  { ( F `  B ) }  =  { y  |  y  =  ( F `  B ) }
65a1i 11 . 2  |-  ( ( F  Fn  A  /\  B  e.  A )  ->  { ( F `  B ) }  =  { y  |  y  =  ( F `  B ) } )
7 fnrel 5530 . . . 4  |-  ( F  Fn  A  ->  Rel  F )
8 relimasn 5213 . . . 4  |-  ( Rel 
F  ->  ( F " { B } )  =  { y  |  B F y } )
97, 8syl 16 . . 3  |-  ( F  Fn  A  ->  ( F " { B }
)  =  { y  |  B F y } )
109adantr 465 . 2  |-  ( ( F  Fn  A  /\  B  e.  A )  ->  ( F " { B } )  =  {
y  |  B F y } )
114, 6, 103eqtr4d 2485 1  |-  ( ( F  Fn  A  /\  B  e.  A )  ->  { ( F `  B ) }  =  ( F " { B } ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    = wceq 1369    e. wcel 1756   {cab 2429   {csn 3898   class class class wbr 4313   "cima 4864   Rel wrel 4866    Fn wfn 5434   ` cfv 5439
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 4434  ax-nul 4442  ax-pr 4552
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 2577  df-ne 2622  df-ral 2741  df-rex 2742  df-rab 2745  df-v 2995  df-sbc 3208  df-dif 3352  df-un 3354  df-in 3356  df-ss 3363  df-nul 3659  df-if 3813  df-sn 3899  df-pr 3901  df-op 3905  df-uni 4113  df-br 4314  df-opab 4372  df-id 4657  df-xp 4867  df-rel 4868  df-cnv 4869  df-co 4870  df-dm 4871  df-rn 4872  df-res 4873  df-ima 4874  df-iota 5402  df-fun 5441  df-fn 5442  df-fv 5447
This theorem is referenced by:  fnimapr  5776  funfv  5779  fvco2  5787  fvimacnvi  5838  fvimacnvALT  5843  fsn2  5904  fparlem3  6695  fparlem4  6696  suppval1  6717  suppsnop  6725  domunsncan  7432  phplem4  7514  domunfican  7605  fiint  7609  infdifsn  7883  cantnfp1lem3  7909  cantnfp1lem3OLD  7935  symgfixelsi  15961  dprdf1o  16551  frlmlbs  18247  f1lindf  18273  cnt1  18976  xkohaus  19248  xkoptsub  19249  ustuqtop3  19840  2pthlem2  23517  eupath2lem3  23622  eulerpartlemmf  26780  grpokerinj  28776  funcoressn  30059
  Copyright terms: Public domain W3C validator