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

Definition df-fn 4848
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 (A Fn B ↔ (Fun A dom A = B))

Detailed syntax breakdown of Definition df-fn
StepHypRef Expression
1 cA . . 3 class A
2 cB . . 3 class B
31, 2wfn 4840 . 2 wff A Fn B
41wfun 4839 . . 3 wff Fun A
51cdm 4288 . . . 4 class dom A
65, 2wceq 1242 . . 3 wff dom A = B
74, 6wa 97 . 2 wff (Fun A dom A = B)
83, 7wb 98 1 wff (A Fn B ↔ (Fun A dom A = B))
Colors of variables: wff set class
This definition is referenced by:  funfn  4874  fnsng  4890  fnprg  4897  fntpg  4898  fntp  4899  fncnv  4908  fneq1  4930  fneq2  4931  nffn  4938  fnfun  4939  fndm  4941  fnun  4948  fnco  4950  fnssresb  4954  fnres  4958  fnresi  4959  fn0  4961  fnopabg  4965  sbcfng  4987  fcoi1  5013  f00  5024  f1cnvcnv  5043  fores  5058  dff1o4  5077  foimacnv  5087  fun11iun  5090  funfvdm  5179  respreima  5238  fpr  5288  fnex  5326  fliftf  5382  fnoprabg  5544  tposfn2  5822  tfrlemibfn  5883  tfri1d  5890  frecuzrdgfn  8839
  Copyright terms: Public domain W3C validator