Definition df-fn 5274

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 5266	. 2 wff A Fn B
4	1	wfun 5265	. . 3 wff Fun A
5	1	cdm 4675	. . . 4 class dom A
6	5, 2	wceq 1373	. . 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  5301  fnsng  5321  fnprg  5329  fntpg  5330  fntp  5331  fncnv  5340  fneq1  5362  fneq2  5363  nffn  5370  fnfun  5371  fndm  5373  fnun  5382  fnco  5384  fnssresb  5388  fnres  5392  fnresi  5393  fn0  5395  fnopabg  5399  sbcfng  5423  fcoi1  5456  f00  5467  f1cnvcnv  5492  fores  5508  dff1o4  5530  foimacnv  5540  fun11iun  5543  funfvdm  5642  respreima  5708  fpr  5766  fnex  5806  fliftf  5868  fnoprabg  6046  tposfn2  6352  tfrlemibfn  6414  tfri1d  6421  tfr1onlembfn  6430  tfri1dALT  6437  tfrcllembfn  6443  sbthlemi9  7067  caseinl  7193  caseinr  7194  ctssdccl  7213  exmidfodomrlemim  7309  axaddf  7981  axmulf  7982  frecuzrdgtcl  10557  frecuzrdgtclt  10566  shftfn  11135  imasaddfnlemg  13146  fntopon  14496