Definition df-fn 4984

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 4976	. 2 wff A Fn B
4	1	wfun 4975	. . 3 wff Fun A
5	1	cdm 4411	. . . 4 class dom A
6	5, 2	wceq 1287	. . 3 wff dom A = B
7	4, 6	wa 102	. 2 wff ( Fun A /\ dom A = B )
8	3, 7	wb 103	1 wff ( A Fn B <-> ( Fun A /\ dom A = B ) )

This definition is referenced by:  funfn  5010  fnsng  5026  fnprg  5034  fntpg  5035  fntp  5036  fncnv  5045  fneq1  5067  fneq2  5068  nffn  5075  fnfun  5076  fndm  5078  fnun  5085  fnco  5087  fnssresb  5091  fnres  5095  fnresi  5096  fn0  5098  fnopabg  5102  sbcfng  5124  fcoi1  5154  f00  5165  f1cnvcnv  5190  fores  5205  dff1o4  5224  foimacnv  5234  fun11iun  5237  funfvdm  5330  respreima  5390  fpr  5442  fnex  5480  fliftf  5539  fnoprabg  5703  tposfn2  5985  tfrlemibfn  6047  tfri1d  6054  tfr1onlembfn  6063  tfri1dALT  6070  tfrcllembfn  6076  sbthlemi9  6618  exmidfodomrlemim  6771  frecuzrdgtcl  9747  frecuzrdgtclt  9756  shftfn  10155