Definition df-f 5263

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 5255	. 2 wff F : A --> B
5	3, 1	wfn 5254	. . 3 wff F Fn A
6	3	crn 4665	. . . 4 class ran F
7	6, 2	wss 3157	. . 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  5393  feq2  5394  feq3  5395  nff  5407  sbcfg  5409  ffn  5410  dffn2  5412  frn  5419  dffn3  5421  fss  5422  fco  5426  funssxp  5430  fun  5433  fnfco  5435  fssres  5436  fcoi2  5442  fintm  5446  fin  5447  f0  5451  fconst  5456  f1ssr  5473  fof  5483  dff1o2  5512  fun11iun  5528  ffoss  5539  dff2  5709  fmpt  5715  ffnfv  5723  ffvresb  5728  fpr  5747  fprg  5748  idref  5806  dff1o6  5826  fliftf  5849  1stcof  6230  2ndcof  6231  smores  6359  smores2  6361  iordsmo  6364  tfrcllembfn  6424  sbthlemi9  7040  inresflem  7135  frec2uzf1od  10515  frecuzrdgtcl  10521  fclim  11476  ennnfonelemf1  12660  resmhm2b  13191  srgfcl  13605  cnrest2  14556  lmss  14566  psmetxrge0  14652  dvfgg  15008  plyreres  15084  nninfall  15740