Definition df-fn 4791

Description: Define a function with domain. Definition 6.15(1) of [TakeutiZaring] p. 27. For alternate definitions, see dffn2 5225, dffn3 5230, dffn4 5276, and dffn5 5364. (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 4777	. 2 wff A Fn B
4	1	wfun 4776	. . 3 wff Fun A
5	1	cdm 4773	. . . 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  5137  fnsn  5153  fnprg  5154  fncnv  5159  fneq1  5174  fneq2  5175  nffn  5181  fnfun  5182  fndm  5183  fnun  5190  fnco  5192  fnssresb  5196  fnres  5200  fnresi  5201  fn0  5203  fnopabg  5206  f0  5249  f00  5250  fores  5279  dff1o4  5295  foimacnv  5304  fun11iun  5306  f1o0  5320  f1ovi  5322  funfv  5376  respreima  5411  dff3  5421  fpr  5438  fvi  5443  1stfo  5506  2ndfo  5507  swapf1o  5512  fnoprabg  5586  fntxp  5805  fnsex  5833  fnpprod  5844  mapexi  6004  fndmeng  6047  enpw1  6063  enmap2  6069  fnfrec  6321