Definition df-fn 5275

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 5267	. 2 wff A Fn B
4	1	wfun 5266	. . 3 wff Fun A
5	1	cdm 4676	. . . 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  5302  fnsng  5322  fnprg  5330  fntpg  5331  fntp  5332  fncnv  5341  fneq1  5363  fneq2  5364  nffn  5371  fnfun  5372  fndm  5374  fnun  5383  fnco  5385  fnssresb  5389  fnres  5394  fnresi  5395  fn0  5397  fnopabg  5401  sbcfng  5425  fcoi1  5458  f00  5469  f1cnvcnv  5494  fores  5510  dff1o4  5532  foimacnv  5542  fun11iun  5545  funfvdm  5644  respreima  5710  fpr  5768  fnex  5808  fliftf  5870  fnoprabg  6048  tposfn2  6354  tfrlemibfn  6416  tfri1d  6423  tfr1onlembfn  6432  tfri1dALT  6439  tfrcllembfn  6445  sbthlemi9  7069  caseinl  7195  caseinr  7196  ctssdccl  7215  exmidfodomrlemim  7311  axaddf  7983  axmulf  7984  frecuzrdgtcl  10559  frecuzrdgtclt  10568  shftfn  11168  imasaddfnlemg  13179  fntopon  14529