Definition df-f 5337

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 5329	. 2 wff F : A --> B
5	3, 1	wfn 5328	. . 3 wff F Fn A
6	3	crn 4732	. . . 4 class ran F
7	6, 2	wss 3201	. . 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  5472  feq2  5473  feq3  5474  nff  5486  sbcfg  5488  ffn  5489  dffn2  5491  frn  5498  dffn3  5500  fss  5501  fco  5507  funssxp  5512  fun  5516  fnfco  5519  fssres  5520  fcoi2  5526  fintm  5530  fin  5531  f0  5536  fconst  5541  f1ssr  5558  fof  5568  dff1o2  5597  fun11iun  5613  ffoss  5625  dff2  5799  fmpt  5805  ffnfv  5813  ffvresb  5818  fcof  5841  fpr  5844  fprg  5845  idref  5907  dff1o6  5927  fliftf  5950  1stcof  6335  2ndcof  6336  smores  6501  smores2  6503  iordsmo  6506  tfrcllembfn  6566  sbthlemi9  7207  inresflem  7302  frec2uzf1od  10712  frecuzrdgtcl  10718  fclim  11915  ennnfonelemf1  13100  resmhm2b  13633  srgfcl  14048  cnrest2  15027  lmss  15037  psmetxrge0  15123  dvfgg  15479  plyreres  15555  ausgrusgrben  16086  ausgrumgrien  16088  subuhgr  16190  subupgr  16191  subumgr  16192  subusgr  16193  nninfall  16712