Definition df-fn 3199

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 3183	. 2 wff A Fn B
4	1	wfun 3182	. . 3 wff Fun A
5	1	cdm 3176	. . . 4 class dom A
6	5, 2	wceq 958	. . 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 3548  fncnv 3567  fneq1 3588  fneq2 3589  hbfn 3590  fnfun 3591  fndm 3593  fnun 3600  fnco 3601  fnssresb 3605  fnresi 3609  fn0 3611  fnopabg 3621  fco 3642  f00 3663  fconst 3664  f1cnv 3672  fores 3687  f1o4 3702  f1ocnv 3707  f1osn 3725  funbrfvb 3761  funfv 3776  fvimacnvALT 3815  dff2 3823  fvi 3848  f1oweALT 3912  tfrlem10 3926  tfr1 3930  frfnom 3957  fnoprabg 4018  curry1 4104  sbthlem9 4461  fodomr 4489  axaddopr 5277  axmulopr 5278  infxpidmlem7 7559  grprn 8053  ringsn 8159  cmpdom 10458  trnij 10608

Copyright terms: Public domain