Definition df-fn 5261

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 5253	. 2 wff A Fn B
4	1	wfun 5252	. . 3 wff Fun A
5	1	cdm 4663	. . . 4 class dom A
6	5, 2	wceq 1364	. . 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  5288  fnsng  5305  fnprg  5313  fntpg  5314  fntp  5315  fncnv  5324  fneq1  5346  fneq2  5347  nffn  5354  fnfun  5355  fndm  5357  fnun  5364  fnco  5366  fnssresb  5370  fnres  5374  fnresi  5375  fn0  5377  fnopabg  5381  sbcfng  5405  fcoi1  5438  f00  5449  f1cnvcnv  5474  fores  5490  dff1o4  5512  foimacnv  5522  fun11iun  5525  funfvdm  5624  respreima  5690  fpr  5744  fnex  5784  fliftf  5846  fnoprabg  6023  tposfn2  6324  tfrlemibfn  6386  tfri1d  6393  tfr1onlembfn  6402  tfri1dALT  6409  tfrcllembfn  6415  sbthlemi9  7031  caseinl  7157  caseinr  7158  ctssdccl  7177  exmidfodomrlemim  7268  axaddf  7935  axmulf  7936  frecuzrdgtcl  10504  frecuzrdgtclt  10513  shftfn  10989  imasaddfnlemg  12957  fntopon  14260