Definition df-fn 5293

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 5285	. 2 wff A Fn B
4	1	wfun 5284	. . 3 wff Fun A
5	1	cdm 4693	. . . 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  5320  fnsng  5340  fnprg  5348  fntpg  5349  fntp  5350  fncnv  5359  fneq1  5381  fneq2  5382  nffn  5389  fnfun  5390  fndm  5392  fnun  5401  fnco  5403  fnssresb  5407  fnres  5412  fnresi  5413  fn0  5415  fnopabg  5419  sbcfng  5443  fcoi1  5478  f00  5489  f1cnvcnv  5514  fores  5530  dff1o4  5552  foimacnv  5562  fun11iun  5565  funfvdm  5665  respreima  5731  fpr  5789  fnex  5829  fliftf  5891  fnoprabg  6069  tposfn2  6375  tfrlemibfn  6437  tfri1d  6444  tfr1onlembfn  6453  tfri1dALT  6460  tfrcllembfn  6466  sbthlemi9  7093  caseinl  7219  caseinr  7220  ctssdccl  7239  exmidfodomrlemim  7340  axaddf  8016  axmulf  8017  frecuzrdgtcl  10594  frecuzrdgtclt  10603  shftfn  11250  imasaddfnlemg  13261  fntopon  14611