Definition df-fn 5238

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 5230	. 2 wff A Fn B
4	1	wfun 5229	. . 3 wff Fun A
5	1	cdm 4644	. . . 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  5265  fnsng  5282  fnprg  5290  fntpg  5291  fntp  5292  fncnv  5301  fneq1  5323  fneq2  5324  nffn  5331  fnfun  5332  fndm  5334  fnun  5341  fnco  5343  fnssresb  5347  fnres  5351  fnresi  5352  fn0  5354  fnopabg  5358  sbcfng  5382  fcoi1  5415  f00  5426  f1cnvcnv  5451  fores  5466  dff1o4  5488  foimacnv  5498  fun11iun  5501  funfvdm  5600  respreima  5665  fpr  5719  fnex  5759  fliftf  5821  fnoprabg  5998  tposfn2  6292  tfrlemibfn  6354  tfri1d  6361  tfr1onlembfn  6370  tfri1dALT  6377  tfrcllembfn  6383  sbthlemi9  6995  caseinl  7121  caseinr  7122  ctssdccl  7141  exmidfodomrlemim  7231  axaddf  7898  axmulf  7899  frecuzrdgtcl  10445  frecuzrdgtclt  10454  shftfn  10868  imasaddfnlemg  12794  fntopon  14001