ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-f Structured version   GIF version

Definition df-f 4821
Description: Define a function (mapping) with domain and codomain. Definition 6.15(3) of [TakeutiZaring] p. 27. (Contributed by NM, 1-Aug-1994.)
Assertion
Ref Expression
df-f (𝐹:AB ↔ (𝐹 Fn A ran 𝐹B))

Detailed syntax breakdown of Definition df-f
StepHypRef Expression
1 cA . . 3 class A
2 cB . . 3 class B
3 cF . . 3 class 𝐹
41, 2, 3wf 4813 . 2 wff 𝐹:AB
53, 1wfn 4812 . . 3 wff 𝐹 Fn A
63crn 4261 . . . 4 class ran 𝐹
76, 2wss 2885 . . 3 wff ran 𝐹B
85, 7wa 97 . 2 wff (𝐹 Fn A ran 𝐹B)
94, 8wb 98 1 wff (𝐹:AB ↔ (𝐹 Fn A ran 𝐹B))
Colors of variables: wff set class
This definition is referenced by:  feq1  4944  feq2  4945  feq3  4946  nff  4957  sbcfg  4959  ffn  4960  dffn2  4961  frn  4966  dffn3  4967  fss  4968  fco  4969  funssxp  4973  fun  4976  fnfco  4978  fssres  4979  fcoi2  4984  fintm  4988  fin  4989  f0  4993  fconst  4995  f1ssr  5011  fof  5019  dff1o2  5044  fun11iun  5060  ffoss  5071  dff2  5224  fmpt  5232  ffnfv  5236  ffvresb  5241  fpr  5258  fprg  5259  idref  5309  dff1o6  5329  fliftf  5352  1stcof  5701  2ndcof  5702  smores  5817  smores2  5819  iordsmo  5822
  Copyright terms: Public domain W3C validator