Definition df-fn 3274

Description: Define a function with domain. Definition 6.15(1) of [TakeutiZaring] p. 27. For alternate definitions, see dffn2 3735, dffn3 3741, dffn4 3785, and dffn5 3869.

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 3258	. 2 wff A Fn B
4	1	wfun 3257	. . 3 wff Fun A
5	1	cdm 3251	. . . 4 class dom A
6	5, 2	wceq 992	. . 3 wff dom A = B
7	4, 6	wa 221	. 2 wff (Fun A /\ dom A = B)
8	3, 7	wb 144	1 wff (A Fn B <-> (Fun A /\ dom A = B))

This definition is referenced by:  funfn 3647  fncnv 3666  fneq1 3688  fneq2 3689  hbfn 3690  fnfun 3691  fndm 3693  fnun 3700  fnco 3701  fnssresb 3705  fnresi 3709  fn0 3711  fnopabg 3722  fco 3743  f00 3764  fconst 3765  f1cnv 3773  fores 3789  dff1o4 3804  f1ocnv 3809  foimacnv 3814  f1osn 3830  funbrfvb 3866  funfv 3881  fvimacnvALT 3923  dff3 3931  fvi 3956  f1oweALT 4020  fnoprabg 4072  curry1 4193  curry2 4196  tfrlem10 4221  tfr1 4225  frfnom 4252  sbthlem9 4600  fodomr 4628  axaddopr 5419  axmulopr 5420  infxpidmlem7 7770  grprn 8269  ringsn 8405  cmpdom 10752  zrdivrng 10969  trnij 11160  opncldf1 11454  cnsubsp 11483  subtopmetlem 11505  neibastop2lem3 11582  ssga 11777  gapm 11784  respreima 11795

Copyright terms: Public domain