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

Definition df-fn 4820
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 4812 . 2 wff A Fn B
41wfun 4811 . . 3 wff Fun A
51cdm 4260 . . . 4 class dom A
65, 2wceq 1223 . . 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  4845  fnsng  4861  fnprg  4868  fntpg  4869  fntp  4870  fncnv  4879  fneq1  4901  fneq2  4902  nffn  4909  fnfun  4910  fndm  4912  fnun  4919  fnco  4921  fnssresb  4925  fnres  4929  fnresi  4930  fn0  4932  fnopabg  4936  sbcfng  4958  fcoi1  4983  f00  4994  f1cnvcnv  5013  fores  5028  dff1o4  5047  foimacnv  5057  fun11iun  5060  funfvdm  5149  respreima  5208  fpr  5258  fnex  5296  fliftf  5352  fnoprabg  5513  tposfn2  5791  tfrlemibfn  5851  tfri1d  5859  tfri1  5861
  Copyright terms: Public domain W3C validator