Definition df-fn 6035

Description: Define a function with domain. Definition 6.15(1) of [TakeutiZaring] p. 27. For alternate definitions, see dffn2 6188, dffn3 6195, dffn4 6263, and dffn5 6384. (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 6027	. 2 wff 𝐴 Fn 𝐵
4	1	wfun 6026	. . 3 wff Fun 𝐴
5	1	cdm 5250	. . . 4 class dom 𝐴
6	5, 2	wceq 1631	. . 3 wff dom 𝐴 = 𝐵
7	4, 6	wa 382	. 2 wff (Fun 𝐴 ∧ dom 𝐴 = 𝐵)
8	3, 7	wb 196	1 wff (𝐴 Fn 𝐵 ↔ (Fun 𝐴 ∧ dom 𝐴 = 𝐵))

This definition is referenced by:  funfn  6062  fnsng  6082  fnprg  6089  fntpg  6090  fntp  6091  fncnv  6103  fneq1  6120  fneq2  6121  nffn  6128  fnfun  6129  fndm  6131  fnun  6138  fnco  6140  fnssresb  6144  fnres  6148  fnresi  6149  fn0  6152  mptfnf  6156  fnopabg  6158  sbcfng  6183  fdmrn  6205  fcoi1  6219  f00  6228  f1cnvcnv  6251  fores  6266  dff1o4  6287  foimacnv  6296  funfv  6408  fvimacnvALT  6480  respreima  6488  dff3  6516  fpr  6565  fnsnb  6577  fnprb  6617  fnex  6626  fliftf  6709  fnoprabg  6909  fun11iun  7274  f1oweALT  7300  curry1  7421  curry2  7424  tposfn2  7527  wfrlem13  7581  wfr1  7587  tfrlem10  7637  tfr1  7647  frfnom  7684  undifixp  8099  sbthlem9  8235  fodomr  8268  rankf  8822  cardf2  8970  axdc3lem2  9476  nqerf  9955  axaddf  10169  axmulf  10170  uzrdgfni  12966  hashkf  13324  shftfn  14022  imasaddfnlem  16397  imasvscafn  16406  fntopon  20950  cnextf  22091  ftc1cn  24027  grporn  27716  ffsrn  29845  measdivcstOLD  30628  bnj1422  31247  nofnbday  32143  elno2  32145  scutf  32257  fnsingle  32364  fnimage  32374  imageval  32375  dfrecs2  32395  dfrdg4  32396  ftc1cnnc  33817  fnresfnco  41727  funcoressn  41728  afvco2  41777