Definition df-f 5276

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 5268	. 2 wff F : A --> B
5	3, 1	wfn 5267	. . 3 wff F Fn A
6	3	crn 4677	. . . 4 class ran F
7	6, 2	wss 3166	. . 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  5410  feq2  5411  feq3  5412  nff  5424  sbcfg  5426  ffn  5427  dffn2  5429  frn  5436  dffn3  5438  fss  5439  fco  5443  funssxp  5447  fun  5450  fnfco  5452  fssres  5453  fcoi2  5459  fintm  5463  fin  5464  f0  5468  fconst  5473  f1ssr  5490  fof  5500  dff1o2  5529  fun11iun  5545  ffoss  5556  dff2  5726  fmpt  5732  ffnfv  5740  ffvresb  5745  fpr  5768  fprg  5769  idref  5827  dff1o6  5847  fliftf  5870  1stcof  6251  2ndcof  6252  smores  6380  smores2  6382  iordsmo  6385  tfrcllembfn  6445  sbthlemi9  7069  inresflem  7164  frec2uzf1od  10553  frecuzrdgtcl  10559  fclim  11638  ennnfonelemf1  12822  resmhm2b  13354  srgfcl  13768  cnrest2  14741  lmss  14751  psmetxrge0  14837  dvfgg  15193  plyreres  15269  nninfall  15983