New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  df-f GIF version

Definition df-f 4791
 Description: Define a function (mapping) with domain and codomain. Definition 6.15(3) of [TakeutiZaring] p. 27. For alternate definitions, see dff2 5419, dff3 5420, and dff4 5421. (Contributed by SF, 5-Jan-2015.)
Assertion
Ref Expression
df-f (F:A–→B ↔ (F Fn A ran F B))

Detailed syntax breakdown of Definition df-f
StepHypRef Expression
1 cA . . 3 class A
2 cB . . 3 class B
3 cF . . 3 class F
41, 2, 3wf 4777 . 2 wff F:A–→B
53, 1wfn 4776 . . 3 wff F Fn A
63crn 4773 . . . 4 class ran F
76, 2wss 3257 . . 3 wff ran F B
85, 7wa 358 . 2 wff (F Fn A ran F B)
94, 8wb 176 1 wff (F:A–→B ↔ (F Fn A ran F B))
 Colors of variables: wff setvar class This definition is referenced by:  feq1  5210  feq2  5211  feq3  5212  nff  5221  ffn  5223  dffn2  5224  frn  5228  dffn3  5229  fss  5230  fco  5231  funssxp  5233  fun  5236  fnfco  5237  fssres  5238  fint  5245  fin  5246  f0  5248  fconst  5250  f1funfun  5263  fof  5269  dff1o2  5291  fun11iun  5305  ffoss  5314  dff2  5419  dff3  5420  ffnfv  5427  ffvresb  5431  fpr  5437  dff1o6  5475  fmpt  5692  fmpt2d  5695  mapexi  6003  map0e  6023  ovcelem1  6171  ceex  6174  fce  6188  sbthlem1  6203
 Copyright terms: Public domain W3C validator