Definition df-fn 4174

Description: Define a function with domain. Definition 6.15(1) of [TakeutiZaring] p. 27. For alternate definitions, see dffn2 4699, dffn3 4705, dffn4 4750, and dffn5 4842.

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 4158	. 2 wff A Fn B
4	1	wfun 4157	. . 3 wff Fun A
5	1	cdm 4151	. . . 4 class dom A
6	5, 2	wceq 1615	. . 3 wff dom A = B
7	4, 6	wa 433	. 2 wff (Fun A /\ dom A = B)
8	3, 7	wb 231	1 wff (A Fn B <-> (Fun A /\ dom A = B))

This definition is referenced by:  funfn 4591  fnsn 4608  fnprg 4609  fntp 4610  fncnv 4618  fneq1 4640  fneq2 4641  hbfn 4647  fnfun 4648  fndm 4650  fnun 4657  fnco 4658  fnssresb 4662  fnresi 4666  fn0 4668  fnex 4670  fnopabg 4680  fcoi1 4716  f00 4728  f1cnvcnv 4738  fores 4754  dff1o4 4769  foimacnv 4779  funbrfvb 4839  funfv 4855  fvimacnvALT 4907  respreima 4911  dff3 4919  fpr 4943  fvi 4949  f1oweALT 5019  fnoprabg 5073  fnmpt 5154  curry1 5238  curry2 5241  tfrlem10 5332  tfr1 5336  frfnom 5363  sbthlem9 5727  fodomr 5759  axdc3lem2 6377  axaddopr 6860  axmulopr 6861  infxpidmlem7OLD 9357  grprn 10357  ssga 10476  gapm 10483  ringsn 10511  subtopmetlem 11251  zrdivrng 11414  bnj143 13413  bnj1422 14047  bnj103 14152  bnj522 14190  bnj535 14194  nqerf 14533  fresin 14717  wfrlem13 14869  wfr1 14873  elno2 14907  bdayfn 14932  axdenselem1 14935  cmpdom 15476  repfuntw 15502  unprj 15511  domrancur1b 15548  domrancur1c 15550  curgrpact 15731  trnij 16068  opncldf1 16487  cnsubsp 16511  neibastop2lem3 16606  prfOLD 16765  respreimaOLD 16769

Copyright terms: Public domain