Definition df-f 4175

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

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 4159	. 2 wff F:A-->B
5	3, 1	wfn 4158	. . 3 wff F Fn A
6	3	crn 4152	. . . 4 class ran F
7	6, 2	wss 2859	. . 3 wff ran F C_ B
8	5, 7	wa 433	. 2 wff (F Fn A /\ ran F C_ B)
9	4, 8	wb 231	1 wff (F:A-->B <-> (F Fn A /\ ran F C_ B))

This definition is referenced by:  feq1 4685  feq2 4686  feq3 4687  hbf 4696  ffn 4698  dffn2 4699  frn 4704  dffn3 4705  fss 4706  fco 4707  funssxp 4709  fun 4712  fnfco 4713  fssres 4714  fcoi2 4717  fint 4721  fin 4722  f0 4727  fconst 4729  fof 4744  dff1o2 4766  ffoss 4790  dff2 4918  dff3 4919  fopab2 4927  ffnfv 4932  fopabco 4936  fpr 4943  dff1o6 4987  fmpt2d 5157  1stcof 5186  smores 5303  smores2 5305  iordsmo 5308  mapval2 5598  map0e 5605  sbthlem9 5727  sucdom2 5854  inf3lem6 6000  alephsmo 6291  alephsing 6358  axdc3lem2 6377  ac5b 6394  om2uzf1oi 8197  seq1f 8225  seq1f2 8226  ser1f 8232  reeff1o 9207  ruclem13 9321  infmap2lem2 9379  idcn 10058  lmsslem 10246  ssga 10476  hhssnv 11759  pjfi 12274  nqerf 14533  fresin 14717  elno2 14907  elno3 14908  axdenselem6 14940  dff1o6f 15389  2ndcof 15463  fopab2g 15480  domrancur1b 15548  isppm 15711  homcard 15911  cmptdst 15978  trnij 16068  cnsubsp 16511  cnsubsp2 16512  tailmap 16721  filnet 16730  cnimass 16973  heiborlem29 17068  heiborlem33 17072  pcocn 17161  smoresOLD 17529  iordsmoOLD 17531

Copyright terms: Public domain