Definition df-fn 4972

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 4964	. 2 wff A Fn B
4	1	wfun 4963	. . 3 wff Fun A
5	1	cdm 4401	. . . 4 class dom A
6	5, 2	wceq 1285	. . 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  4998  fnsng  5014  fnprg  5022  fntpg  5023  fntp  5024  fncnv  5033  fneq1  5055  fneq2  5056  nffn  5063  fnfun  5064  fndm  5066  fnun  5073  fnco  5075  fnssresb  5079  fnres  5083  fnresi  5084  fn0  5086  fnopabg  5090  sbcfng  5112  fcoi1  5139  f00  5150  f1cnvcnv  5175  fores  5190  dff1o4  5209  foimacnv  5219  fun11iun  5222  funfvdm  5312  respreima  5372  fpr  5421  fnex  5459  fliftf  5518  fnoprabg  5681  tposfn2  5963  tfrlemibfn  6025  tfri1d  6032  tfr1onlembfn  6041  tfri1dALT  6048  tfrcllembfn  6054  exmidfodomrlemim  6730  frecuzrdgtcl  9708  frecuzrdgtclt  9717  shftfn  10086