Definition df-fn 5220

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 5212	. 2 wff A Fn B
4	1	wfun 5211	. . 3 wff Fun A
5	1	cdm 4627	. . . 4 class dom A
6	5, 2	wceq 1353	. . 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  5247  fnsng  5264  fnprg  5272  fntpg  5273  fntp  5274  fncnv  5283  fneq1  5305  fneq2  5306  nffn  5313  fnfun  5314  fndm  5316  fnun  5323  fnco  5325  fnssresb  5329  fnres  5333  fnresi  5334  fn0  5336  fnopabg  5340  sbcfng  5364  fcoi1  5397  f00  5408  f1cnvcnv  5433  fores  5448  dff1o4  5470  foimacnv  5480  fun11iun  5483  funfvdm  5580  respreima  5645  fpr  5699  fnex  5739  fliftf  5800  fnoprabg  5976  tposfn2  6267  tfrlemibfn  6329  tfri1d  6336  tfr1onlembfn  6345  tfri1dALT  6352  tfrcllembfn  6358  sbthlemi9  6964  caseinl  7090  caseinr  7091  ctssdccl  7110  exmidfodomrlemim  7200  axaddf  7867  axmulf  7868  frecuzrdgtcl  10412  frecuzrdgtclt  10421  shftfn  10833  imasaddfnlemg  12735  fntopon  13527