Definition df-f 5275

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 5267	. 2 wff F : A --> B
5	3, 1	wfn 5266	. . 3 wff F Fn A
6	3	crn 4676	. . . 4 class ran F
7	6, 2	wss 3166	. . 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  5408  feq2  5409  feq3  5410  nff  5422  sbcfg  5424  ffn  5425  dffn2  5427  frn  5434  dffn3  5436  fss  5437  fco  5441  funssxp  5445  fun  5448  fnfco  5450  fssres  5451  fcoi2  5457  fintm  5461  fin  5462  f0  5466  fconst  5471  f1ssr  5488  fof  5498  dff1o2  5527  fun11iun  5543  ffoss  5554  dff2  5724  fmpt  5730  ffnfv  5738  ffvresb  5743  fpr  5766  fprg  5767  idref  5825  dff1o6  5845  fliftf  5868  1stcof  6249  2ndcof  6250  smores  6378  smores2  6380  iordsmo  6383  tfrcllembfn  6443  sbthlemi9  7067  inresflem  7162  frec2uzf1od  10551  frecuzrdgtcl  10557  fclim  11605  ennnfonelemf1  12789  resmhm2b  13321  srgfcl  13735  cnrest2  14708  lmss  14718  psmetxrge0  14804  dvfgg  15160  plyreres  15236  nninfall  15946