Definition df-fn 6496

Description: Define a function with domain. Definition 6.15(1) of [TakeutiZaring] p. 27. For alternate definitions, see dffn2 6665, dffn3 6675, dffn4 6753, and dffn5 6893. (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 6488	. 2 wff 𝐴 Fn 𝐵
4	1	wfun 6487	. . 3 wff Fun 𝐴
5	1	cdm 5625	. . . 4 class dom 𝐴
6	5, 2	wceq 1542	. . 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  6523  fnsng  6545  fnprg  6552  fntpg  6553  fntp  6554  fncnv  6566  fneq1  6584  fneq2  6585  nffn  6592  fnfun  6593  fndm  6596  fnun  6607  fnssresb  6615  fnres  6620  idfn  6621  fn0  6624  mptfnf  6628  fnopabg  6630  sbcfng  6660  fdmrn  6694  fcoi1  6709  f00  6717  f1cnvcnv  6740  fores  6757  dff1o4  6783  foimacnv  6792  funfv  6922  fvimacnvALT  7004  respreima  7013  dff3  7047  fpr  7101  fnsnbOLD  7114  fnprb  7156  fnex  7165  fliftf  7263  fnoprabg  7483  fiun  7889  f1iun  7890  f1oweALT  7918  curry1  8048  curry2  8051  tposfn2  8192  frrlem11  8240  frrlem12  8241  fpr1  8247  tfrlem10  8320  tfr1  8330  frfnom  8368  undifixp  8876  sbthlem9  9027  fodomr  9060  fodomfir  9232  frr1  9675  rankf  9710  cardf2  9859  axdc3lem2  10365  nqerf  10845  axaddf  11060  axmulf  11061  uzrdgfni  13885  hashkf  14259  shftfn  15000  imasaddfnlem  17453  imasvscafn  17462  nfchnd  18538  fntopon  22872  cnextf  24014  ftc1cn  26010  nofnbday  27624  cutsf  27792  oniso  28271  noseqrdgfn  28306  bdayn0sf1o  28370  grporn  30600  ffsrn  32809  measdivcstALTV  34384  bnj1422  34995  satff  35606  fnsingle  36113  fnimage  36123  imageval  36124  dfrecs2  36146  dfrdg4  36147  bj-isrvec  37501  ftc1cnnc  37895  modelaxreplem1  45286  fnresfnco  47354  funcoressn  47355  afvco2  47489