Definition df-f 4985

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 4977	. 2 wff F : A --> B
5	3, 1	wfn 4976	. . 3 wff F Fn A
6	3	crn 4412	. . . 4 class ran F
7	6, 2	wss 2988	. . 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  5110  feq2  5111  feq3  5112  nff  5123  sbcfg  5125  ffn  5126  dffn2  5128  frn  5134  dffn3  5135  fss  5136  fco  5140  funssxp  5144  fun  5147  fnfco  5149  fssres  5150  fcoi2  5155  fintm  5159  fin  5160  f0  5164  fconst  5169  f1ssr  5186  fof  5196  dff1o2  5221  fun11iun  5237  ffoss  5248  dff2  5406  fmpt  5412  ffnfv  5419  ffvresb  5424  fpr  5442  fprg  5443  idref  5497  dff1o6  5516  fliftf  5539  1stcof  5891  2ndcof  5892  smores  6011  smores2  6013  iordsmo  6016  tfrcllembfn  6076  sbthlemi9  6618  inresflem  6696  frec2uzf1od  9741  frecuzrdgtcl  9747  fclim  10577  nninfall  11345