Definition df-f 5322

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 5314	. 2 wff F : A --> B
5	3, 1	wfn 5313	. . 3 wff F Fn A
6	3	crn 4720	. . . 4 class ran F
7	6, 2	wss 3197	. . 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  5456  feq2  5457  feq3  5458  nff  5470  sbcfg  5472  ffn  5473  dffn2  5475  frn  5482  dffn3  5484  fss  5485  fco  5489  funssxp  5493  fun  5497  fnfco  5500  fssres  5501  fcoi2  5507  fintm  5511  fin  5512  f0  5516  fconst  5521  f1ssr  5538  fof  5548  dff1o2  5577  fun11iun  5593  ffoss  5604  dff2  5779  fmpt  5785  ffnfv  5793  ffvresb  5798  fpr  5821  fprg  5822  idref  5880  dff1o6  5900  fliftf  5923  1stcof  6309  2ndcof  6310  smores  6438  smores2  6440  iordsmo  6443  tfrcllembfn  6503  sbthlemi9  7132  inresflem  7227  frec2uzf1od  10628  frecuzrdgtcl  10634  fclim  11805  ennnfonelemf1  12989  resmhm2b  13522  srgfcl  13936  cnrest2  14910  lmss  14920  psmetxrge0  15006  dvfgg  15362  plyreres  15438  ausgrusgrben  15966  ausgrumgrien  15968  nninfall  16375