Definition df-f 5262

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 5254	. 2 wff F : A --> B
5	3, 1	wfn 5253	. . 3 wff F Fn A
6	3	crn 4664	. . . 4 class ran F
7	6, 2	wss 3157	. . 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  5390  feq2  5391  feq3  5392  nff  5404  sbcfg  5406  ffn  5407  dffn2  5409  frn  5416  dffn3  5418  fss  5419  fco  5423  funssxp  5427  fun  5430  fnfco  5432  fssres  5433  fcoi2  5439  fintm  5443  fin  5444  f0  5448  fconst  5453  f1ssr  5470  fof  5480  dff1o2  5509  fun11iun  5525  ffoss  5536  dff2  5706  fmpt  5712  ffnfv  5720  ffvresb  5725  fpr  5744  fprg  5745  idref  5803  dff1o6  5823  fliftf  5846  1stcof  6221  2ndcof  6222  smores  6350  smores2  6352  iordsmo  6355  tfrcllembfn  6415  sbthlemi9  7031  inresflem  7126  frec2uzf1od  10498  frecuzrdgtcl  10504  fclim  11459  ennnfonelemf1  12635  resmhm2b  13121  srgfcl  13529  cnrest2  14472  lmss  14482  psmetxrge0  14568  dvfgg  14924  plyreres  15000  nninfall  15653