Definition df-f 5063

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 5055	. 2 wff F : A --> B
5	3, 1	wfn 5054	. . 3 wff F Fn A
6	3	crn 4478	. . . 4 class ran F
7	6, 2	wss 3021	. . 3 wff ran F C_ B
8	5, 7	wa 103	. 2 wff ( F Fn A /\ ran F C_ B )
9	4, 8	wb 104	1 wff ( F : A --> B <-> ( F Fn A /\ ran F C_ B ) )

This definition is referenced by:  feq1  5191  feq2  5192  feq3  5193  nff  5205  sbcfg  5207  ffn  5208  dffn2  5210  frn  5217  dffn3  5219  fss  5220  fco  5224  funssxp  5228  fun  5231  fnfco  5233  fssres  5234  fcoi2  5240  fintm  5244  fin  5245  f0  5249  fconst  5254  f1ssr  5271  fof  5281  dff1o2  5306  fun11iun  5322  ffoss  5333  dff2  5496  fmpt  5502  ffnfv  5510  ffvresb  5515  fpr  5534  fprg  5535  idref  5590  dff1o6  5609  fliftf  5632  1stcof  5992  2ndcof  5993  smores  6119  smores2  6121  iordsmo  6124  tfrcllembfn  6184  sbthlemi9  6781  inresflem  6860  frec2uzf1od  10020  frecuzrdgtcl  10026  fclim  10902  ennnfonelemf1  11723  cnrest2  12186  lmss  12196  psmetxrge0  12260  dvfgg  12530  nninfall  12788