Definition df-f 5239

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 5231	. 2 wff F : A --> B
5	3, 1	wfn 5230	. . 3 wff F Fn A
6	3	crn 4645	. . . 4 class ran F
7	6, 2	wss 3144	. . 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  5367  feq2  5368  feq3  5369  nff  5381  sbcfg  5383  ffn  5384  dffn2  5386  frn  5393  dffn3  5395  fss  5396  fco  5400  funssxp  5404  fun  5407  fnfco  5409  fssres  5410  fcoi2  5416  fintm  5420  fin  5421  f0  5425  fconst  5430  f1ssr  5447  fof  5457  dff1o2  5485  fun11iun  5501  ffoss  5512  dff2  5681  fmpt  5687  ffnfv  5695  ffvresb  5700  fpr  5719  fprg  5720  idref  5778  dff1o6  5798  fliftf  5821  1stcof  6189  2ndcof  6190  smores  6318  smores2  6320  iordsmo  6323  tfrcllembfn  6383  sbthlemi9  6995  inresflem  7090  frec2uzf1od  10439  frecuzrdgtcl  10445  fclim  11337  ennnfonelemf1  12472  resmhm2b  12956  srgfcl  13344  cnrest2  14213  lmss  14223  psmetxrge0  14309  dvfgg  14634  nninfall  15237