Definition df-f 5379

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 5371	. 2 wff F : A --> B
5	3, 1	wfn 5370	. . 3 wff F Fn A
6	3	crn 4773	. . . 4 class ran F
7	6, 2	wss 3220	. . 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  5514  feq2  5515  feq3  5516  nff  5528  sbcfg  5530  ffn  5531  dffn2  5533  frn  5540  dffn3  5542  fss  5544  fco  5550  funssxp  5555  fun  5559  fnfco  5562  fssres  5563  fcoi2  5571  fintm  5575  fin  5576  f0  5581  fconst  5586  f1ssr  5603  fof  5613  dff1o2  5642  fun11iun  5658  ffoss  5670  dff2  5846  fmpt  5852  ffnfv  5860  ffvresb  5865  fcof  5888  fpr  5891  fprg  5892  idref  5955  dff1o6  5975  fliftf  5998  fdmrn  6027  1stcof  6390  2ndcof  6391  smores  6556  smores2  6558  iordsmo  6561  tfrcllembfn  6621  sbthlemi9  7275  inresflem  7393  frec2uzf1od  10824  frecuzrdgtcl  10830  fclim  12041  ennnfonelemf1  13290  resmhm2b  13776  srgfcl  14254  cnrest2  15263  lmss  15273  psmetxrge0  15359  dvfgg  15715  plyreres  15791  ausgrusgrben  16326  ausgrumgrien  16328  subuhgr  16430  subupgr  16431  subumgr  16432  subusgr  16433  nninfall  16960