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

Definition df-f 5127
 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 5119 . 2 wff 𝐹:𝐴𝐵
53, 1wfn 5118 . . 3 wff 𝐹 Fn 𝐴
63crn 4540 . . . 4 class ran 𝐹
76, 2wss 3071 . . 3 wff ran 𝐹𝐵
85, 7wa 103 . 2 wff (𝐹 Fn 𝐴 ∧ ran 𝐹𝐵)
94, 8wb 104 1 wff (𝐹:𝐴𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹𝐵))
 Colors of variables: wff set class This definition is referenced by:  feq1  5255  feq2  5256  feq3  5257  nff  5269  sbcfg  5271  ffn  5272  dffn2  5274  frn  5281  dffn3  5283  fss  5284  fco  5288  funssxp  5292  fun  5295  fnfco  5297  fssres  5298  fcoi2  5304  fintm  5308  fin  5309  f0  5313  fconst  5318  f1ssr  5335  fof  5345  dff1o2  5372  fun11iun  5388  ffoss  5399  dff2  5564  fmpt  5570  ffnfv  5578  ffvresb  5583  fpr  5602  fprg  5603  idref  5658  dff1o6  5677  fliftf  5700  1stcof  6061  2ndcof  6062  smores  6189  smores2  6191  iordsmo  6194  tfrcllembfn  6254  sbthlemi9  6853  inresflem  6945  frec2uzf1od  10191  frecuzrdgtcl  10197  fclim  11075  ennnfonelemf1  11942  cnrest2  12419  lmss  12429  psmetxrge0  12515  dvfgg  12840  nninfall  13265
 Copyright terms: Public domain W3C validator