Definition df-fn 5258

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 5250	. 2 wff A Fn B
4	1	wfun 5249	. . 3 wff Fun A
5	1	cdm 4660	. . . 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  5285  fnsng  5302  fnprg  5310  fntpg  5311  fntp  5312  fncnv  5321  fneq1  5343  fneq2  5344  nffn  5351  fnfun  5352  fndm  5354  fnun  5361  fnco  5363  fnssresb  5367  fnres  5371  fnresi  5372  fn0  5374  fnopabg  5378  sbcfng  5402  fcoi1  5435  f00  5446  f1cnvcnv  5471  fores  5487  dff1o4  5509  foimacnv  5519  fun11iun  5522  funfvdm  5621  respreima  5687  fpr  5741  fnex  5781  fliftf  5843  fnoprabg  6020  tposfn2  6321  tfrlemibfn  6383  tfri1d  6390  tfr1onlembfn  6399  tfri1dALT  6406  tfrcllembfn  6412  sbthlemi9  7026  caseinl  7152  caseinr  7153  ctssdccl  7172  exmidfodomrlemim  7263  axaddf  7930  axmulf  7931  frecuzrdgtcl  10486  frecuzrdgtclt  10495  shftfn  10971  imasaddfnlemg  12900  fntopon  14203