Definition df-f 5221

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 5213	. 2 wff F : A --> B
5	3, 1	wfn 5212	. . 3 wff F Fn A
6	3	crn 4628	. . . 4 class ran F
7	6, 2	wss 3130	. . 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  5349  feq2  5350  feq3  5351  nff  5363  sbcfg  5365  ffn  5366  dffn2  5368  frn  5375  dffn3  5377  fss  5378  fco  5382  funssxp  5386  fun  5389  fnfco  5391  fssres  5392  fcoi2  5398  fintm  5402  fin  5403  f0  5407  fconst  5412  f1ssr  5429  fof  5439  dff1o2  5467  fun11iun  5483  ffoss  5494  dff2  5661  fmpt  5667  ffnfv  5675  ffvresb  5680  fpr  5699  fprg  5700  idref  5758  dff1o6  5777  fliftf  5800  1stcof  6164  2ndcof  6165  smores  6293  smores2  6295  iordsmo  6298  tfrcllembfn  6358  sbthlemi9  6964  inresflem  7059  frec2uzf1od  10406  frecuzrdgtcl  10412  fclim  11302  ennnfonelemf1  12419  srgfcl  13156  cnrest2  13739  lmss  13749  psmetxrge0  13835  dvfgg  14160  nninfall  14761