Definition df-f 3184

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 3168	. 2 wff F:A-->B
5	3, 1	wfn 3167	. . 3 wff F Fn A
6	3	crn 3161	. . . 4 class ran F
7	6, 2	wss 2037	. . 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 3606  feq2 3607  feq3 3608  feq23 3609  hbf 3611  ffn 3613  fnf 3614  frn 3618  fnfrn 3619  fss 3620  fco 3621  funssxp 3623  fun 3626  fnfco 3627  fssres 3628  fint 3635  fin 3636  f0 3641  fconst 3643  fof 3657  f1o2 3678  f1o3 3679  ffoss 3696  dff4 3801  dff2 3802  fopab2 3808  ffnfv 3813  fopabco 3817  f1ofv 3862  1stcof 4085  mapval2 4319  map0e 4326  sbthlem9 4435  inf3lem6 4590  ac5b 4725  om2uzf1o 6238  seq1f 6260  seq1f2 6261  ser1ft 6265  reeff1o 7368  ruclem13 7465  infmap2lem2 7522  idcn 7705  lmsslem 7887  hhssnv 9054  pjf 9566  homcard 10426  trnij 10481

Copyright terms: Public domain