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

Definition df-fn 4905
 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 4897 . 2 wff 𝐴 Fn 𝐵
41wfun 4896 . . 3 wff Fun 𝐴
51cdm 4345 . . . 4 class dom 𝐴
65, 2wceq 1243 . . 3 wff dom 𝐴 = 𝐵
74, 6wa 97 . 2 wff (Fun 𝐴 ∧ dom 𝐴 = 𝐵)
83, 7wb 98 1 wff (𝐴 Fn 𝐵 ↔ (Fun 𝐴 ∧ dom 𝐴 = 𝐵))
 Colors of variables: wff set class This definition is referenced by:  funfn  4931  fnsng  4947  fnprg  4954  fntpg  4955  fntp  4956  fncnv  4965  fneq1  4987  fneq2  4988  nffn  4995  fnfun  4996  fndm  4998  fnun  5005  fnco  5007  fnssresb  5011  fnres  5015  fnresi  5016  fn0  5018  fnopabg  5022  sbcfng  5044  fcoi1  5070  f00  5081  f1cnvcnv  5100  fores  5115  dff1o4  5134  foimacnv  5144  fun11iun  5147  funfvdm  5236  respreima  5295  fpr  5345  fnex  5383  fliftf  5439  fnoprabg  5602  tposfn2  5881  tfrlemibfn  5942  tfri1d  5949  frecuzrdgfn  9198  shftfn  9425
 Copyright terms: Public domain W3C validator