Definition df-f 5212

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 5204	. 2 wff F : A --> B
5	3, 1	wfn 5203	. . 3 wff F Fn A
6	3	crn 4621	. . . 4 class ran F
7	6, 2	wss 3127	. . 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  5340  feq2  5341  feq3  5342  nff  5354  sbcfg  5356  ffn  5357  dffn2  5359  frn  5366  dffn3  5368  fss  5369  fco  5373  funssxp  5377  fun  5380  fnfco  5382  fssres  5383  fcoi2  5389  fintm  5393  fin  5394  f0  5398  fconst  5403  f1ssr  5420  fof  5430  dff1o2  5458  fun11iun  5474  ffoss  5485  dff2  5652  fmpt  5658  ffnfv  5666  ffvresb  5671  fpr  5690  fprg  5691  idref  5748  dff1o6  5767  fliftf  5790  1stcof  6154  2ndcof  6155  smores  6283  smores2  6285  iordsmo  6288  tfrcllembfn  6348  sbthlemi9  6954  inresflem  7049  frec2uzf1od  10376  frecuzrdgtcl  10382  fclim  11270  ennnfonelemf1  12386  srgfcl  12962  cnrest2  13316  lmss  13326  psmetxrge0  13412  dvfgg  13737  nninfall  14328