Definition df-fn 3183

Description: Define a function with domain. Definition 6.15(1) of [TakeutiZaring] p. 27.

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 3167	. 2 wff A Fn B
4	1	wfun 3166	. . 3 wff Fun A
5	1	cdm 3160	. . . 4 class dom A
6	5, 2	wceq 953	. . 3 wff dom A = B
7	4, 6	wa 223	. 2 wff (Fun A /\ dom A = B)
8	3, 7	wb 146	1 wff (A Fn B <-> (Fun A /\ dom A = B))

This definition is referenced by:  funfn 3528  fncnv 3547  fneq1 3568  fneq2 3569  hbfn 3570  fnfun 3571  fndm 3573  fnun 3580  fnco 3581  fnssresb 3585  fnresi 3589  fn0 3591  fnopabg 3601  fco 3621  f00 3642  fconst 3643  f1cnv 3651  fores 3666  f1o4 3681  f1ocnv 3686  f1osn 3704  funbrfvb 3740  funfv 3755  fvimacnvALT 3794  dff2 3802  fvi 3827  f1oweALT 3891  tfrlem10 3905  tfr1 3909  frfnom 3936  fnoprabg 3997  curry1 4082  sbthlem9 4435  fodomr 4463  axaddopr 5237  axmulopr 5238  infxpidmlem7 7501  grprn 7990  ringsn 8100  cmpdom 10364  trnij 10481

Copyright terms: Public domain