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

Definition df-fn 4828
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 4820 . 2 wff A Fn B
41wfun 4819 . . 3 wff Fun A
51cdm 4268 . . . 4 class dom A
65, 2wceq 1226 . . 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  4853  fnsng  4869  fnprg  4876  fntpg  4877  fntp  4878  fncnv  4887  fneq1  4909  fneq2  4910  nffn  4917  fnfun  4918  fndm  4920  fnun  4927  fnco  4929  fnssresb  4933  fnres  4937  fnresi  4938  fn0  4940  fnopabg  4944  sbcfng  4966  fcoi1  4991  f00  5002  f1cnvcnv  5021  fores  5036  dff1o4  5055  foimacnv  5065  fun11iun  5068  funfvdm  5157  respreima  5216  fpr  5266  fnex  5304  fliftf  5360  fnoprabg  5521  tposfn2  5799  tfrlemibfn  5859  tfri1d  5867  tfri1  5869
  Copyright terms: Public domain W3C validator