Definition df-f 5192

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 5184	. 2 wff F : A --> B
5	3, 1	wfn 5183	. . 3 wff F Fn A
6	3	crn 4605	. . . 4 class ran F
7	6, 2	wss 3116	. . 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  5320  feq2  5321  feq3  5322  nff  5334  sbcfg  5336  ffn  5337  dffn2  5339  frn  5346  dffn3  5348  fss  5349  fco  5353  funssxp  5357  fun  5360  fnfco  5362  fssres  5363  fcoi2  5369  fintm  5373  fin  5374  f0  5378  fconst  5383  f1ssr  5400  fof  5410  dff1o2  5437  fun11iun  5453  ffoss  5464  dff2  5629  fmpt  5635  ffnfv  5643  ffvresb  5648  fpr  5667  fprg  5668  idref  5725  dff1o6  5744  fliftf  5767  1stcof  6131  2ndcof  6132  smores  6260  smores2  6262  iordsmo  6265  tfrcllembfn  6325  sbthlemi9  6930  inresflem  7025  frec2uzf1od  10341  frecuzrdgtcl  10347  fclim  11235  ennnfonelemf1  12351  cnrest2  12876  lmss  12886  psmetxrge0  12972  dvfgg  13297  nninfall  13889