Definition df-fn 4790

Description: Define a function with domain. Definition 6.15(1) of [TakeutiZaring] p. 27. For alternate definitions, see dffn2 5224, dffn3 5229, dffn4 5275, and dffn5 5363. (Contributed by SF, 5-Jan-2015.)

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 4776	. 2 wff A Fn B
4	1	wfun 4775	. . 3 wff Fun A
5	1	cdm 4772	. . . 4 class dom A
6	5, 2	wceq 1642	. . 3 wff dom A = B
7	4, 6	wa 358	. 2 wff (Fun A /\ dom A = B)
8	3, 7	wb 176	1 wff (A Fn B <-> (Fun A /\ dom A = B))

This definition is referenced by:  funfn  5136  fnsn  5152  fnprg  5153  fncnv  5158  fneq1  5173  fneq2  5174  nffn  5180  fnfun  5181  fndm  5182  fnun  5189  fnco  5191  fnssresb  5195  fnres  5199  fnresi  5200  fn0  5202  fnopabg  5205  f0  5248  f00  5249  fores  5278  dff1o4  5294  foimacnv  5303  fun11iun  5305  f1o0  5319  f1ovi  5321  funfv  5375  respreima  5410  dff3  5420  fpr  5437  fvi  5442  1stfo  5505  2ndfo  5506  swapf1o  5511  fnoprabg  5585  fntxp  5804  fnsex  5832  fnpprod  5843  mapexi  6003  fndmeng  6046  enpw1  6062  enmap2  6068  fnfrec  6320