Definition df-fn 5378

Description: Define a function with domain. Definition 6.15(1) of [TakeutiZaring] p. 27. (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 5370	. 2 wff 𝐴 Fn 𝐵
4	1	wfun 5369	. . 3 wff Fun 𝐴
5	1	cdm 4772	. . . 4 class dom 𝐴
6	5, 2	wceq 1402	. . 3 wff dom 𝐴 = 𝐵
7	4, 6	wa 104	. 2 wff (Fun 𝐴 ∧ dom 𝐴 = 𝐵)
8	3, 7	wb 105	1 wff (𝐴 Fn 𝐵 ↔ (Fun 𝐴 ∧ dom 𝐴 = 𝐵))

This definition is used by:  funfn  5405  fnsng  5426  fnprg  5434  fntpg  5435  fntp  5436  fncnv  5445  fneq1  5467  fneq2  5468  nffn  5475  fnfun  5476  fndm  5478  fnun  5487  fnco  5489  fnssresb  5493  fnres  5498  fnresi  5499  fn0  5501  fnopabg  5505  sbcfng  5529  fcoi1  5570  f00  5582  f1cnvcnv  5607  fores  5623  dff1o4  5645  foimacnv  5655  fun11iun  5658  funfvdm  5763  respreima  5830  fpr  5891  fnex  5931  fliftf  5999  fdmrn  6028  fnoprabg  6183  tposfn2  6531  tfrlemibfn  6593  tfri1d  6600  tfr1onlembfn  6609  tfri1dALT  6616  tfrcllembfn  6622  sbthlemi9  7276  caseinl  7425  caseinr  7426  ctssdccl  7445  exmidfodomrlemim  7547  axaddf  8229  axmulf  8230  frecuzrdgtcl  10832  frecuzrdgtclt  10841  shftfn  11572  imasaddfnlemg  13618  fntopon  15108