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

Definition df-f 4906
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 (𝐹:𝐴𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹𝐵))

Detailed syntax breakdown of Definition df-f
StepHypRef Expression
1 cA . . 3 class 𝐴
2 cB . . 3 class 𝐵
3 cF . . 3 class 𝐹
41, 2, 3wf 4898 . 2 wff 𝐹:𝐴𝐵
53, 1wfn 4897 . . 3 wff 𝐹 Fn 𝐴
63crn 4346 . . . 4 class ran 𝐹
76, 2wss 2917 . . 3 wff ran 𝐹𝐵
85, 7wa 97 . 2 wff (𝐹 Fn 𝐴 ∧ ran 𝐹𝐵)
94, 8wb 98 1 wff (𝐹:𝐴𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹𝐵))
Colors of variables: wff set class
This definition is referenced by:  feq1  5030  feq2  5031  feq3  5032  nff  5043  sbcfg  5045  ffn  5046  dffn2  5047  frn  5052  dffn3  5053  fss  5054  fco  5056  funssxp  5060  fun  5063  fnfco  5065  fssres  5066  fcoi2  5071  fintm  5075  fin  5076  f0  5080  fconst  5082  f1ssr  5098  fof  5106  dff1o2  5131  fun11iun  5147  ffoss  5158  dff2  5311  fmpt  5319  ffnfv  5323  ffvresb  5328  fpr  5345  fprg  5346  idref  5396  dff1o6  5416  fliftf  5439  1stcof  5790  2ndcof  5791  smores  5907  smores2  5909  iordsmo  5912  frec2uzf1od  9192  fclim  9815
  Copyright terms: Public domain W3C validator