Definition df-fn 5126

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 5118	. 2 wff A Fn B
4	1	wfun 5117	. . 3 wff Fun A
5	1	cdm 4539	. . . 4 class dom A
6	5, 2	wceq 1331	. . 3 wff dom A = B
7	4, 6	wa 103	. 2 wff ( Fun A /\ dom A = B )
8	3, 7	wb 104	1 wff ( A Fn B <-> ( Fun A /\ dom A = B ) )

This definition is referenced by:  funfn  5153  fnsng  5170  fnprg  5178  fntpg  5179  fntp  5180  fncnv  5189  fneq1  5211  fneq2  5212  nffn  5219  fnfun  5220  fndm  5222  fnun  5229  fnco  5231  fnssresb  5235  fnres  5239  fnresi  5240  fn0  5242  fnopabg  5246  sbcfng  5270  fcoi1  5303  f00  5314  f1cnvcnv  5339  fores  5354  dff1o4  5375  foimacnv  5385  fun11iun  5388  funfvdm  5484  respreima  5548  fpr  5602  fnex  5642  fliftf  5700  fnoprabg  5872  tposfn2  6163  tfrlemibfn  6225  tfri1d  6232  tfr1onlembfn  6241  tfri1dALT  6248  tfrcllembfn  6254  sbthlemi9  6853  caseinl  6976  caseinr  6977  ctssdccl  6996  exmidfodomrlemim  7057  axaddf  7676  axmulf  7677  frecuzrdgtcl  10185  frecuzrdgtclt  10194  shftfn  10596  fntopon  12191