Definition df-fn 5329

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 5321	. 2 wff A Fn B
4	1	wfun 5320	. . 3 wff Fun A
5	1	cdm 4725	. . . 4 class dom A
6	5, 2	wceq 1397	. . 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 referenced by:  funfn  5356  fnsng  5377  fnprg  5385  fntpg  5386  fntp  5387  fncnv  5396  fneq1  5418  fneq2  5419  nffn  5426  fnfun  5427  fndm  5429  fnun  5438  fnco  5440  fnssresb  5444  fnres  5449  fnresi  5450  fn0  5452  fnopabg  5456  sbcfng  5480  fcoi1  5517  f00  5528  f1cnvcnv  5553  fores  5569  dff1o4  5591  foimacnv  5601  fun11iun  5604  funfvdm  5709  respreima  5775  fpr  5836  fnex  5876  fliftf  5940  fnoprabg  6122  tposfn2  6432  tfrlemibfn  6494  tfri1d  6501  tfr1onlembfn  6510  tfri1dALT  6517  tfrcllembfn  6523  sbthlemi9  7164  caseinl  7290  caseinr  7291  ctssdccl  7310  exmidfodomrlemim  7412  axaddf  8088  axmulf  8089  frecuzrdgtcl  10674  frecuzrdgtclt  10683  shftfn  11385  imasaddfnlemg  13398  fntopon  14750