Definition df-f 5294

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 5286	. 2 wff F : A --> B
5	3, 1	wfn 5285	. . 3 wff F Fn A
6	3	crn 4694	. . . 4 class ran F
7	6, 2	wss 3174	. . 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  5428  feq2  5429  feq3  5430  nff  5442  sbcfg  5444  ffn  5445  dffn2  5447  frn  5454  dffn3  5456  fss  5457  fco  5461  funssxp  5465  fun  5469  fnfco  5472  fssres  5473  fcoi2  5479  fintm  5483  fin  5484  f0  5488  fconst  5493  f1ssr  5510  fof  5520  dff1o2  5549  fun11iun  5565  ffoss  5576  dff2  5747  fmpt  5753  ffnfv  5761  ffvresb  5766  fpr  5789  fprg  5790  idref  5848  dff1o6  5868  fliftf  5891  1stcof  6272  2ndcof  6273  smores  6401  smores2  6403  iordsmo  6406  tfrcllembfn  6466  sbthlemi9  7093  inresflem  7188  frec2uzf1od  10588  frecuzrdgtcl  10594  fclim  11720  ennnfonelemf1  12904  resmhm2b  13436  srgfcl  13850  cnrest2  14823  lmss  14833  psmetxrge0  14919  dvfgg  15275  plyreres  15351  nninfall  16148