Definition df-f 4010

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

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 3994	. 2 wff F:A-->B
5	3, 1	wfn 3993	. . 3 wff F Fn A
6	3	crn 3987	. . . 4 class ran F
7	6, 2	wss 2593	. . 3 wff ran F C_ B
8	5, 7	wa 240	. 2 wff (F Fn A /\ ran F C_ B)
9	4, 8	wb 163	1 wff (F:A-->B <-> (F Fn A /\ ran F C_ B))

This definition is referenced by:  feq1 4551  feq2 4552  feq3 4553  feq23OLD 4555  hbf 4560  ffn 4562  dffn2 4563  dffn2OLD 4564  frn 4569  dffn3 4570  fss 4571  fssOLD 4572  fco 4573  fcoOLD 4574  funssxp 4577  fun 4580  fnfco 4581  fssres 4582  fcoi2 4586  fint 4591  fintOLD 4592  fin 4593  finOLD 4594  f0 4600  fconst 4602  fconstOLD 4603  fof 4617  dff1o2 4639  dff1o2OLD 4640  dff1o3OLD 4642  ffoss 4665  dff2 4789  dff3 4790  fopab2 4796  ffnfv 4801  fopabco 4805  fpr 4810  fprOLD 4811  dff1o6 4853  1stcof 5040  mapval2 5394  map0e 5401  sbthlem9 5518  inf3lem6 5724  ac5b 5915  om2uzf1oi 7712  seq1f 7736  seq1f2 7737  ser1f 7741  reeff1o 8691  ruclem13 8791  infmap2lem2 8849  idcn 9042  lmsslem 9230  ssga 9455  hhssnv 10767  pjfi 11284  fresin 13840  elno2 14005  axdenselem6 14024  dff1o6f 14416  fopab2g 14485  domrancur1b 14548  isppm 14715  homcard 14893  trnij 15015  cnsubsp 15426  cnsubsp2 15427  tailmap 15636  filnet 15645  cnimass 15888  heiborlem29 15983  heiborlem33 15987  pcocn 16076  smores 16446  iordsmo 16448

Copyright terms: Public domain