Definition df-f 5186

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 5178	. 2 wff F : A --> B
5	3, 1	wfn 5177	. . 3 wff F Fn A
6	3	crn 4599	. . . 4 class ran F
7	6, 2	wss 3111	. . 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  5314  feq2  5315  feq3  5316  nff  5328  sbcfg  5330  ffn  5331  dffn2  5333  frn  5340  dffn3  5342  fss  5343  fco  5347  funssxp  5351  fun  5354  fnfco  5356  fssres  5357  fcoi2  5363  fintm  5367  fin  5368  f0  5372  fconst  5377  f1ssr  5394  fof  5404  dff1o2  5431  fun11iun  5447  ffoss  5458  dff2  5623  fmpt  5629  ffnfv  5637  ffvresb  5642  fpr  5661  fprg  5662  idref  5719  dff1o6  5738  fliftf  5761  1stcof  6123  2ndcof  6124  smores  6251  smores2  6253  iordsmo  6256  tfrcllembfn  6316  sbthlemi9  6921  inresflem  7016  frec2uzf1od  10331  frecuzrdgtcl  10337  fclim  11221  ennnfonelemf1  12288  cnrest2  12777  lmss  12787  psmetxrge0  12873  dvfgg  13198  nninfall  13723