Definition df-f 5217

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 5209	. 2 wff F : A --> B
5	3, 1	wfn 5208	. . 3 wff F Fn A
6	3	crn 4625	. . . 4 class ran F
7	6, 2	wss 3129	. . 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  5345  feq2  5346  feq3  5347  nff  5359  sbcfg  5361  ffn  5362  dffn2  5364  frn  5371  dffn3  5373  fss  5374  fco  5378  funssxp  5382  fun  5385  fnfco  5387  fssres  5388  fcoi2  5394  fintm  5398  fin  5399  f0  5403  fconst  5408  f1ssr  5425  fof  5435  dff1o2  5463  fun11iun  5479  ffoss  5490  dff2  5657  fmpt  5663  ffnfv  5671  ffvresb  5676  fpr  5695  fprg  5696  idref  5753  dff1o6  5772  fliftf  5795  1stcof  6159  2ndcof  6160  smores  6288  smores2  6290  iordsmo  6293  tfrcllembfn  6353  sbthlemi9  6959  inresflem  7054  frec2uzf1od  10399  frecuzrdgtcl  10405  fclim  11293  ennnfonelemf1  12409  srgfcl  13056  cnrest2  13518  lmss  13528  psmetxrge0  13614  dvfgg  13939  nninfall  14529