Definition df-fn 5346

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 5338	. 2 wff A Fn B
4	1	wfun 5337	. . 3 wff Fun A
5	1	cdm 4740	. . . 4 class dom A
6	5, 2	wceq 1398	. . 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  5373  fnsng  5394  fnprg  5402  fntpg  5403  fntp  5404  fncnv  5413  fneq1  5435  fneq2  5436  nffn  5443  fnfun  5444  fndm  5446  fnun  5455  fnco  5457  fnssresb  5461  fnres  5466  fnresi  5467  fn0  5469  fnopabg  5473  sbcfng  5497  fcoi1  5538  f00  5550  f1cnvcnv  5575  fores  5591  dff1o4  5613  foimacnv  5623  fun11iun  5626  funfvdm  5731  respreima  5796  fpr  5857  fnex  5897  fliftf  5963  fnoprabg  6145  tposfn2  6488  tfrlemibfn  6550  tfri1d  6557  tfr1onlembfn  6566  tfri1dALT  6573  tfrcllembfn  6579  sbthlemi9  7226  caseinl  7373  caseinr  7374  ctssdccl  7393  exmidfodomrlemim  7495  axaddf  8171  axmulf  8172  frecuzrdgtcl  10760  frecuzrdgtclt  10769  shftfn  11487  imasaddfnlemg  13501  fntopon  14859