Definition df-f 4973

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 4965	. 2 wff F : A --> B
5	3, 1	wfn 4964	. . 3 wff F Fn A
6	3	crn 4402	. . . 4 class ran F
7	6, 2	wss 2984	. . 3 wff ran F C_ B
8	5, 7	wa 102	. 2 wff ( F Fn A /\ ran F C_ B )
9	4, 8	wb 103	1 wff ( F : A --> B <-> ( F Fn A /\ ran F C_ B ) )

This definition is referenced by:  feq1  5098  feq2  5099  feq3  5100  nff  5111  sbcfg  5113  ffn  5114  dffn2  5116  frn  5121  dffn3  5122  fss  5123  fco  5125  funssxp  5129  fun  5132  fnfco  5134  fssres  5135  fcoi2  5140  fintm  5144  fin  5145  f0  5149  fconst  5154  f1ssr  5171  fof  5181  dff1o2  5206  fun11iun  5222  ffoss  5233  dff2  5388  fmpt  5394  ffnfv  5398  ffvresb  5403  fpr  5421  fprg  5422  idref  5476  dff1o6  5495  fliftf  5518  1stcof  5869  2ndcof  5870  smores  5989  smores2  5991  iordsmo  5994  tfrcllembfn  6054  inresflem  6659  frec2uzf1od  9702  frecuzrdgtcl  9708  fclim  10507  nninfall  11241