Definition df-f 3275

Description: Define a function (mapping) with domain and codomain. Definition 6.15(3) of [TakeutiZaring] p. 27. For alternate definitions, see dff2 3930, dff3 3931, and dff4 3932.

Assertion

Ref	Expression
df-f	|- (F:A-->B <-> (F Fn A /\ ran F (_ 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 3259	. 2 wff F:A-->B
5	3, 1	wfn 3258	. . 3 wff F Fn A
6	3	crn 3252	. . . 4 class ran F
7	6, 2	wss 2099	. . 3 wff ran F (_ B
8	5, 7	wa 221	. 2 wff (F Fn A /\ ran F (_ B)
9	4, 8	wb 144	1 wff (F:A-->B <-> (F Fn A /\ ran F (_ B))

This definition is referenced by:  feq1 3727  feq2 3728  feq3 3729  feq23 3730  hbf 3732  ffn 3734  dffn2 3735  frn 3740  dffn3 3741  fss 3742  fco 3743  funssxp 3745  fun 3748  fnfco 3749  fssres 3750  fint 3757  fin 3758  f0 3763  fconst 3765  fof 3779  dff1o2 3801  dff1o3 3802  ffoss 3822  dff2 3930  dff3 3931  fopab2 3937  ffnfv 3942  fopabco 3946  dff1o6 3991  1stcof 4160  mapval2 4476  map0e 4483  sbthlem9 4600  inf3lem6 4763  ac5b 4899  om2uzf1oi 6664  seq1f 6688  seq1f2 6689  ser1f 6693  reeff1o 7634  ruclem13 7734  infmap2lem2 7792  idcn 7976  lmsslem 8163  hhssnv 9410  pjfi 9927  isppm 10917  homcard 11045  trnij 11160  cnsubsp 11483  cnsubsp2 11484  tailmap 11759  filnet 11768  ssga 11777  cnimass 11949  heiborlem29 12039  heiborlem33 12043

Copyright terms: Public domain