New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  df-fn GIF version

Definition df-fn 4790
 Description: Define a function with domain. Definition 6.15(1) of [TakeutiZaring] p. 27. For alternate definitions, see dffn2 5224, dffn3 5229, dffn4 5275, and dffn5 5363. (Contributed by SF, 5-Jan-2015.)
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 4776 . 2 wff A Fn B
41wfun 4775 . . 3 wff Fun A
51cdm 4772 . . . 4 class dom A
65, 2wceq 1642 . . 3 wff dom A = B
74, 6wa 358 . 2 wff (Fun A dom A = B)
83, 7wb 176 1 wff (A Fn B ↔ (Fun A dom A = B))
 Colors of variables: wff setvar class This definition is referenced by:  funfn  5136  fnsn  5152  fnprg  5153  fncnv  5158  fneq1  5173  fneq2  5174  nffn  5180  fnfun  5181  fndm  5182  fnun  5189  fnco  5191  fnssresb  5195  fnres  5199  fnresi  5200  fn0  5202  fnopabg  5205  f0  5248  f00  5249  fores  5278  dff1o4  5294  foimacnv  5303  fun11iun  5305  f1o0  5319  f1ovi  5321  funfv  5375  respreima  5410  dff3  5420  fpr  5437  fvi  5442  1stfo  5505  2ndfo  5506  swapf1o  5511  fnoprabg  5585  fntxp  5804  fnsex  5832  fnpprod  5843  mapexi  6003  fndmeng  6046  enpw1  6062  enmap2  6068  fnfrec  6320
 Copyright terms: Public domain W3C validator