Definition df-fn 6514

Description: Define a function with domain. Definition 6.15(1) of [TakeutiZaring] p. 27. For alternate definitions, see dffn2 6690, dffn3 6700, dffn4 6778, and dffn5 6919. (Contributed by NM, 1-Aug-1994.)

Assertion

Ref	Expression
df-fn	⊢ (𝐴 Fn 𝐵 ↔ (Fun 𝐴 ∧ dom 𝐴 = 𝐵))

Detailed syntax breakdown of Definition df-fn

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2		cB	. . 3 class 𝐵
3	1, 2	wfn 6506	. 2 wff 𝐴 Fn 𝐵
4	1	wfun 6505	. . 3 wff Fun 𝐴
5	1	cdm 5638	. . . 4 class dom 𝐴
6	5, 2	wceq 1540	. . 3 wff dom 𝐴 = 𝐵
7	4, 6	wa 395	. 2 wff (Fun 𝐴 ∧ dom 𝐴 = 𝐵)
8	3, 7	wb 206	1 wff (𝐴 Fn 𝐵 ↔ (Fun 𝐴 ∧ dom 𝐴 = 𝐵))

This definition is referenced by:  funfn  6546  fnsng  6568  fnprg  6575  fntpg  6576  fntp  6577  fncnv  6589  fneq1  6609  fneq2  6610  nffn  6617  fnfun  6618  fndm  6621  fnun  6632  fnssresb  6640  fnres  6645  idfn  6646  fn0  6649  mptfnf  6653  fnopabg  6655  sbcfng  6685  fdmrn  6719  fcoi1  6734  f00  6742  f1cnvcnv  6765  fores  6782  dff1o4  6808  foimacnv  6817  funfv  6948  fvimacnvALT  7029  respreima  7038  dff3  7072  fpr  7126  fnsnbOLD  7140  fnprb  7182  fnex  7191  fliftf  7290  fnoprabg  7512  fiun  7921  f1iun  7922  f1oweALT  7951  curry1  8083  curry2  8086  tposfn2  8227  frrlem11  8275  frrlem12  8276  fpr1  8282  tfrlem10  8355  tfr1  8365  frfnom  8403  undifixp  8907  sbthlem9  9059  fodomr  9092  fodomfir  9279  frr1  9712  rankf  9747  cardf2  9896  axdc3lem2  10404  nqerf  10883  axaddf  11098  axmulf  11099  uzrdgfni  13923  hashkf  14297  shftfn  15039  imasaddfnlem  17491  imasvscafn  17500  fntopon  22811  cnextf  23953  ftc1cn  25950  nofnbday  27564  scutf  27724  onsiso  28169  noseqrdgfn  28200  bdayn0sf1o  28259  grporn  30450  ffsrn  32652  measdivcstALTV  34215  bnj1422  34827  satff  35397  fnsingle  35907  fnimage  35917  imageval  35918  dfrecs2  35938  dfrdg4  35939  bj-isrvec  37282  ftc1cnnc  37686  modelaxreplem1  44968  fnresfnco  47039  funcoressn  47040  afvco2  47174