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  10517  frecuzrdgtcl  10523  fclim  11478  ennnfonelemf1  12662  resmhm2b  13193  srgfcl  13607  cnrest2  14580  lmss  14590  psmetxrge0  14676  dvfgg  15032  plyreres  15108  nninfall  15764