Definition df-f 3194

Description: Define a function (mapping) with domain and codomain. Definition 6.15(3) of [TakeutiZaring] p. 27.

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 3178	. 2 wff F:A-->B
5	3, 1	wfn 3177	. . 3 wff F Fn A
6	3	crn 3171	. . . 4 class ran F
7	6, 2	wss 2047	. . 3 wff ran F (_ B
8	5, 7	wa 223	. 2 wff (F Fn A /\ ran F (_ B)
9	4, 8	wb 146	1 wff (F:A-->B <-> (F Fn A /\ ran F (_ B))

This definition is referenced by:  feq1 3620  feq2 3621  feq3 3622  feq23 3623  hbf 3625  ffn 3627  fnf 3628  frn 3633  fnfrn 3634  fss 3635  fco 3636  funssxp 3638  fun 3641  fnfco 3642  fssres 3643  fint 3650  fin 3651  f0 3656  fconst 3658  fof 3672  f1o2 3693  f1o3 3694  ffoss 3711  dff4 3816  dff2 3817  fopab2 3823  ffnfv 3828  fopabco 3832  f1ofv 3877  1stcof 4101  mapval2 4335  map0e 4342  sbthlem9 4455  inf3lem6 4618  ac5b 4753  om2uzf1o 6301  seq1f 6323  seq1f2 6324  ser1ft 6328  reeff1o 7426  ruclem13 7522  infmap2lem2 7580  idcn 7766  lmsslem 7952  hhssnv 9134  pjf 9649  homcard 10539  trnij 10637

Copyright terms: Public domain