Definition df-fn 5321

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 5313	. 2 wff A Fn B
4	1	wfun 5312	. . 3 wff Fun A
5	1	cdm 4719	. . . 4 class dom A
6	5, 2	wceq 1395	. . 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  5348  fnsng  5368  fnprg  5376  fntpg  5377  fntp  5378  fncnv  5387  fneq1  5409  fneq2  5410  nffn  5417  fnfun  5418  fndm  5420  fnun  5429  fnco  5431  fnssresb  5435  fnres  5440  fnresi  5441  fn0  5443  fnopabg  5447  sbcfng  5471  fcoi1  5506  f00  5517  f1cnvcnv  5542  fores  5558  dff1o4  5580  foimacnv  5590  fun11iun  5593  funfvdm  5697  respreima  5763  fpr  5821  fnex  5861  fliftf  5923  fnoprabg  6105  tposfn2  6412  tfrlemibfn  6474  tfri1d  6481  tfr1onlembfn  6490  tfri1dALT  6497  tfrcllembfn  6503  sbthlemi9  7132  caseinl  7258  caseinr  7259  ctssdccl  7278  exmidfodomrlemim  7379  axaddf  8055  axmulf  8056  frecuzrdgtcl  10634  frecuzrdgtclt  10643  shftfn  11335  imasaddfnlemg  13347  fntopon  14698