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

Definition df-fn 4986
Description: Define a function with domain. Definition 6.15(1) of [TakeutiZaring] p. 27. (Contributed by NM, 1-Aug-1994.)
Assertion
Ref Expression
df-fn (𝐴 Fn 𝐵 ↔ (Fun 𝐴 ∧ dom 𝐴 = 𝐵))

Detailed syntax breakdown of Definition df-fn
StepHypRef Expression
1 cA . . 3 class 𝐴
2 cB . . 3 class 𝐵
31, 2wfn 4978 . 2 wff 𝐴 Fn 𝐵
41wfun 4977 . . 3 wff Fun 𝐴
51cdm 4413 . . . 4 class dom 𝐴
65, 2wceq 1287 . . 3 wff dom 𝐴 = 𝐵
74, 6wa 102 . 2 wff (Fun 𝐴 ∧ dom 𝐴 = 𝐵)
83, 7wb 103 1 wff (𝐴 Fn 𝐵 ↔ (Fun 𝐴 ∧ dom 𝐴 = 𝐵))
Colors of variables: wff set class
This definition is referenced by:  funfn  5012  fnsng  5028  fnprg  5036  fntpg  5037  fntp  5038  fncnv  5047  fneq1  5069  fneq2  5070  nffn  5077  fnfun  5078  fndm  5080  fnun  5087  fnco  5089  fnssresb  5093  fnres  5097  fnresi  5098  fn0  5100  fnopabg  5104  sbcfng  5126  fcoi1  5156  f00  5167  f1cnvcnv  5192  fores  5207  dff1o4  5226  foimacnv  5236  fun11iun  5239  funfvdm  5332  respreima  5392  fpr  5444  fnex  5482  fliftf  5541  fnoprabg  5705  tposfn2  5987  tfrlemibfn  6049  tfri1d  6056  tfr1onlembfn  6065  tfri1dALT  6072  tfrcllembfn  6078  sbthlemi9  6621  exmidfodomrlemim  6774  frecuzrdgtcl  9750  frecuzrdgtclt  9759  shftfn  10158
  Copyright terms: Public domain W3C validator