Definition df-fn 5257

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 5249	. 2 wff A Fn B
4	1	wfun 5248	. . 3 wff Fun A
5	1	cdm 4659	. . . 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  5284  fnsng  5301  fnprg  5309  fntpg  5310  fntp  5311  fncnv  5320  fneq1  5342  fneq2  5343  nffn  5350  fnfun  5351  fndm  5353  fnun  5360  fnco  5362  fnssresb  5366  fnres  5370  fnresi  5371  fn0  5373  fnopabg  5377  sbcfng  5401  fcoi1  5434  f00  5445  f1cnvcnv  5470  fores  5486  dff1o4  5508  foimacnv  5518  fun11iun  5521  funfvdm  5620  respreima  5686  fpr  5740  fnex  5780  fliftf  5842  fnoprabg  6019  tposfn2  6319  tfrlemibfn  6381  tfri1d  6388  tfr1onlembfn  6397  tfri1dALT  6404  tfrcllembfn  6410  sbthlemi9  7024  caseinl  7150  caseinr  7151  ctssdccl  7170  exmidfodomrlemim  7261  axaddf  7928  axmulf  7929  frecuzrdgtcl  10483  frecuzrdgtclt  10492  shftfn  10968  imasaddfnlemg  12897  fntopon  14192