MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-fn Structured version   Visualization version   GIF version

Definition df-fn 5793
Description: Define a function with domain. Definition 6.15(1) of [TakeutiZaring] p. 27. For alternate definitions, see dffn2 5946, dffn3 5953, dffn4 6019, and dffn5 6136. (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 5785 . 2 wff 𝐴 Fn 𝐵
41wfun 5784 . . 3 wff Fun 𝐴
51cdm 5028 . . . 4 class dom 𝐴
65, 2wceq 1474 . . 3 wff dom 𝐴 = 𝐵
74, 6wa 382 . 2 wff (Fun 𝐴 ∧ dom 𝐴 = 𝐵)
83, 7wb 194 1 wff (𝐴 Fn 𝐵 ↔ (Fun 𝐴 ∧ dom 𝐴 = 𝐵))
Colors of variables: wff setvar class
This definition is referenced by:  funfn  5819  fnsng  5838  fnprg  5847  fntpg  5848  fntp  5849  fncnv  5862  fneq1  5879  fneq2  5880  nffn  5887  fnfun  5888  fndm  5890  fnun  5897  fnco  5899  fnssresb  5903  fnres  5907  fnresi  5908  fn0  5910  mptfnf  5914  fnopabg  5916  sbcfng  5941  fdmrn  5963  fcoi1  5976  f00  5985  f1cnvcnv  6007  fores  6022  dff1o4  6043  foimacnv  6052  funfv  6160  fvimacnvALT  6229  respreima  6237  dff3  6265  fpr  6304  fnsnb  6315  fnprb  6355  fnex  6364  fliftf  6443  fnoprabg  6637  fun11iun  6996  f1oweALT  7020  curry1  7133  curry2  7136  tposfn2  7238  wfrlem13  7291  wfr1  7297  tfrlem10  7347  tfr1  7357  frfnom  7394  undifixp  7807  sbthlem9  7940  fodomr  7973  rankf  8517  cardf2  8629  axdc3lem2  9133  nqerf  9608  axaddf  9822  axmulf  9823  uzrdgfni  12574  hashkf  12936  shftfn  13607  imasaddfnlem  15957  imasvscafn  15966  cnextf  21622  ftc1cn  23527  grporn  26525  ffsrn  28698  measdivcstOLD  29420  bnj145OLD  29855  bnj1422  29968  nofnbday  30855  elno2  30857  bdayfn  30884  fnsingle  31002  fnimage  31012  imageval  31013  dfrecs2  31033  dfrdg4  31034  bj-fntopon  32039  ftc1cnnc  32450  fnresfnco  39652  funcoressn  39653  afvco2  39703
  Copyright terms: Public domain W3C validator