Definition df-f 3191

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 3175	. 2 wff F:A-->B
5	3, 1	wfn 3174	. . 3 wff F Fn A
6	3	crn 3168	. . . 4 class ran F
7	6, 2	wss 2045	. . 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 3617  feq2 3618  feq3 3619  feq23 3620  hbf 3622  ffn 3624  fnf 3625  frn 3630  fnfrn 3631  fss 3632  fco 3633  funssxp 3635  fun 3638  fnfco 3639  fssres 3640  fint 3647  fin 3648  f0 3653  fconst 3655  fof 3669  f1o2 3690  f1o3 3691  ffoss 3708  dff4 3813  dff2 3814  fopab2 3820  ffnfv 3825  fopabco 3829  f1ofv 3874  1stcof 4098  mapval2 4332  map0e 4339  sbthlem9 4448  inf3lem6 4605  ac5b 4740  om2uzf1o 6256  seq1f 6278  seq1f2 6279  ser1ft 6283  reeff1o 7404  ruclem13 7501  infmap2lem2 7559  idcn 7745  lmsslem 7935  hhssnv 9122  pjf 9640  homcard 10520  trnij 10588

Copyright terms: Public domain