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

Definition df-fn 4929
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 4921 . 2 wff 𝐴 Fn 𝐵
41wfun 4920 . . 3 wff Fun 𝐴
51cdm 4365 . . . 4 class dom 𝐴
65, 2wceq 1285 . . 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  4955  fnsng  4971  fnprg  4979  fntpg  4980  fntp  4981  fncnv  4990  fneq1  5012  fneq2  5013  nffn  5020  fnfun  5021  fndm  5023  fnun  5030  fnco  5032  fnssresb  5036  fnres  5040  fnresi  5041  fn0  5043  fnopabg  5047  sbcfng  5069  fcoi1  5095  f00  5106  f1cnvcnv  5125  fores  5140  dff1o4  5159  foimacnv  5169  fun11iun  5172  funfvdm  5262  respreima  5321  fpr  5371  fnex  5409  fliftf  5464  fnoprabg  5627  tposfn2  5909  tfrlemibfn  5971  tfri1d  5978  tfr1onlembfn  5987  tfri1dALT  5994  tfrcllembfn  6000  frecuzrdgtcl  9483  frecuzrdgtclt  9492  shftfn  9839
  Copyright terms: Public domain W3C validator