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

Theorem fnsnfv 5753
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 2414 . . . 4  |-  ( y  =  ( F `  B )  <->  ( F `  B )  =  y )
2 fnbrfvb 5734 . . . 4  |-  ( ( F  Fn  A  /\  B  e.  A )  ->  ( ( F `  B )  =  y  <-> 
B F y ) )
31, 2syl5bb 249 . . 3  |-  ( ( F  Fn  A  /\  B  e.  A )  ->  ( y  =  ( F `  B )  <-> 
B F y ) )
43abbidv 2526 . 2  |-  ( ( F  Fn  A  /\  B  e.  A )  ->  { y  |  y  =  ( F `  B ) }  =  { y  |  B F y } )
5 df-sn 3788 . . 3  |-  { ( F `  B ) }  =  { y  |  y  =  ( F `  B ) }
65a1i 11 . 2  |-  ( ( F  Fn  A  /\  B  e.  A )  ->  { ( F `  B ) }  =  { y  |  y  =  ( F `  B ) } )
7 fnrel 5510 . . . 4  |-  ( F  Fn  A  ->  Rel  F )
8 relimasn 5194 . . . 4  |-  ( Rel 
F  ->  ( F " { B } )  =  { y  |  B F y } )
97, 8syl 16 . . 3  |-  ( F  Fn  A  ->  ( F " { B }
)  =  { y  |  B F y } )
109adantr 452 . 2  |-  ( ( F  Fn  A  /\  B  e.  A )  ->  ( F " { B } )  =  {
y  |  B F y } )
114, 6, 103eqtr4d 2454 1  |-  ( ( F  Fn  A  /\  B  e.  A )  ->  { ( F `  B ) }  =  ( F " { B } ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    = wceq 1649    e. wcel 1721   {cab 2398   {csn 3782   class class class wbr 4180   "cima 4848   Rel wrel 4850    Fn wfn 5416   ` cfv 5421
This theorem is referenced by:  fnimapr  5754  funfv  5757  fvco2  5765  fvimacnvi  5811  fvimacnvALT  5816  fsn2  5875  fparlem3  6415  fparlem4  6416  domunsncan  7175  phplem4  7256  domunfican  7346  fiint  7350  infdifsn  7575  cantnfp1lem3  7600  dprdf1o  15553  cnt1  17376  xkohaus  17646  xkoptsub  17647  ustuqtop3  18234  2pthlem2  21557  eupath2lem3  21662  grpokerinj  26458  frlmlbs  27125  f1lindf  27168  funcoressn  27866
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2393  ax-sep 4298  ax-nul 4306  ax-pr 4371
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2266  df-mo 2267  df-clab 2399  df-cleq 2405  df-clel 2408  df-nfc 2537  df-ne 2577  df-ral 2679  df-rex 2680  df-rab 2683  df-v 2926  df-sbc 3130  df-dif 3291  df-un 3293  df-in 3295  df-ss 3302  df-nul 3597  df-if 3708  df-sn 3788  df-pr 3789  df-op 3791  df-uni 3984  df-br 4181  df-opab 4235  df-id 4466  df-xp 4851  df-rel 4852  df-cnv 4853  df-co 4854  df-dm 4855  df-rn 4856  df-res 4857  df-ima 4858  df-iota 5385  df-fun 5423  df-fn 5424  df-fv 5429
  Copyright terms: Public domain W3C validator