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  5529  f1cnvcnv  5554  fores  5570  dff1o4  5592  foimacnv  5602  fun11iun  5605  funfvdm  5710  respreima  5776  fpr  5837  fnex  5877  fliftf  5943  fnoprabg  6125  tposfn2  6435  tfrlemibfn  6497  tfri1d  6504  tfr1onlembfn  6513  tfri1dALT  6520  tfrcllembfn  6526  sbthlemi9  7167  caseinl  7293  caseinr  7294  ctssdccl  7313  exmidfodomrlemim  7415  axaddf  8091  axmulf  8092  frecuzrdgtcl  10678  frecuzrdgtclt  10687  shftfn  11405  imasaddfnlemg  13418  fntopon  14775