Definition df-fn 5380

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	|- ( A Fn B <-> ( Fun A /\ dom A = B ) )

Detailed syntax breakdown of Definition df-fn

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2		cB	. . 3 class B
3	1, 2	wfn 5372	. 2 wff A Fn B
4	1	wfun 5371	. . 3 wff Fun A
5	1	cdm 4774	. . . 4 class dom A
6	5, 2	wceq 1402	. . 3 wff dom A = B
7	4, 6	wa 104	. 2 wff ( Fun A /\ dom A = B )
8	3, 7	wb 105	1 wff ( A Fn B <-> ( Fun A /\ dom A = B ) )

This definition is used by:  funfn  5407  fnsng  5428  fnprg  5436  fntpg  5437  fntp  5438  fncnv  5447  fneq1  5469  fneq2  5470  nffn  5477  fnfun  5478  fndm  5480  fnun  5489  fnco  5491  fnssresb  5495  fnres  5500  fnresi  5501  fn0  5503  fnopabg  5507  sbcfng  5531  fcoi1  5572  f00  5584  f1cnvcnv  5609  fores  5625  dff1o4  5647  foimacnv  5657  fun11iun  5660  funfvdm  5766  respreima  5836  fpr  5897  fnex  5937  fliftf  6005  fdmrn  6034  fnoprabg  6189  tposfn2  6537  tfrlemibfn  6599  tfri1d  6606  tfr1onlembfn  6615  tfri1dALT  6622  tfrcllembfn  6628  sbthlemi9  7282  caseinl  7431  caseinr  7432  ctssdccl  7451  exmidfodomrlemim  7553  axaddf  8235  axmulf  8236  frecuzrdgtcl  10849  frecuzrdgtclt  10858  shftfn  11589  imasaddfnlemg  13635  fntopon  15125