Definition df-f 5258

Description: Define a function (mapping) with domain and codomain. Definition 6.15(3) of [TakeutiZaring] p. 27. (Contributed by NM, 1-Aug-1994.)

Assertion

Ref	Expression
df-f	|- ( F : A --> B <-> ( F Fn A /\ ran F C_ B ) )

Detailed syntax breakdown of Definition df-f

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2		cB	. . 3 class B
3		cF	. . 3 class F
4	1, 2, 3	wf 5250	. 2 wff F : A --> B
5	3, 1	wfn 5249	. . 3 wff F Fn A
6	3	crn 4660	. . . 4 class ran F
7	6, 2	wss 3153	. . 3 wff ran F C_ B
8	5, 7	wa 104	. 2 wff ( F Fn A /\ ran F C_ B )
9	4, 8	wb 105	1 wff ( F : A --> B <-> ( F Fn A /\ ran F C_ B ) )

This definition is referenced by:  feq1  5386  feq2  5387  feq3  5388  nff  5400  sbcfg  5402  ffn  5403  dffn2  5405  frn  5412  dffn3  5414  fss  5415  fco  5419  funssxp  5423  fun  5426  fnfco  5428  fssres  5429  fcoi2  5435  fintm  5439  fin  5440  f0  5444  fconst  5449  f1ssr  5466  fof  5476  dff1o2  5505  fun11iun  5521  ffoss  5532  dff2  5702  fmpt  5708  ffnfv  5716  ffvresb  5721  fpr  5740  fprg  5741  idref  5799  dff1o6  5819  fliftf  5842  1stcof  6216  2ndcof  6217  smores  6345  smores2  6347  iordsmo  6350  tfrcllembfn  6410  sbthlemi9  7024  inresflem  7119  frec2uzf1od  10477  frecuzrdgtcl  10483  fclim  11437  ennnfonelemf1  12575  resmhm2b  13061  srgfcl  13469  cnrest2  14404  lmss  14414  psmetxrge0  14500  dvfgg  14842  nninfall  15499