Definition df-f 5127

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 5119	. 2 wff F : A --> B
5	3, 1	wfn 5118	. . 3 wff F Fn A
6	3	crn 4540	. . . 4 class ran F
7	6, 2	wss 3071	. . 3 wff ran F C_ B
8	5, 7	wa 103	. 2 wff ( F Fn A /\ ran F C_ B )
9	4, 8	wb 104	1 wff ( F : A --> B <-> ( F Fn A /\ ran F C_ B ) )

This definition is referenced by:  feq1  5255  feq2  5256  feq3  5257  nff  5269  sbcfg  5271  ffn  5272  dffn2  5274  frn  5281  dffn3  5283  fss  5284  fco  5288  funssxp  5292  fun  5295  fnfco  5297  fssres  5298  fcoi2  5304  fintm  5308  fin  5309  f0  5313  fconst  5318  f1ssr  5335  fof  5345  dff1o2  5372  fun11iun  5388  ffoss  5399  dff2  5564  fmpt  5570  ffnfv  5578  ffvresb  5583  fpr  5602  fprg  5603  idref  5658  dff1o6  5677  fliftf  5700  1stcof  6061  2ndcof  6062  smores  6189  smores2  6191  iordsmo  6194  tfrcllembfn  6254  sbthlemi9  6853  inresflem  6945  frec2uzf1od  10179  frecuzrdgtcl  10185  fclim  11063  ennnfonelemf1  11931  cnrest2  12405  lmss  12415  psmetxrge0  12501  dvfgg  12826  nninfall  13204