Theorem fndm 3593

Description: The domain of a function.

Assertion

Ref	Expression
fndm	|- (F Fn A -> dom F = A)

Proof of Theorem fndm

Step	Hyp	Ref	Expression
1		df-fn 3199	. 2 |- (F Fn A <-> (Fun F /\ dom F = A))
2	1	pm3.27bi 326	1 |- (F Fn A -> dom F = A)

Syntax hints:   -> wi 3   = wceq 958  dom cdm 3176  Fun wfun 3182   Fn wfn 3183

This theorem is referenced by:  funfni 3594  fndmu 3595  fnbr 3596  fneu 3598  fnco 3601  fnresdm 3602  fnresdisj 3603  fnssresb 3605  fnima 3610  fn0 3611  funimadisj 3612  fnex 3613  dmopab2 3625  fdm 3637  f1ocnv 3707  f1o00 3720  fnrnfv 3765  fvelimab 3771  eqfnfv 3803  fsn2 3842  fconst3 3856  fconst4 3857  f1fv 3880  tfrlem8 3924  tfrlem9 3925  tfrlem13 3929  tz7.44-2 3935  tz7.44-3 3936  rdgsucopabn 3953  frfnom 3957  tz7.48-1 3962  tz7.48-2 3963  tz7.48-3 3964  tz7.49 3965  oprssoprval 4040  curry1 4104  curry1val 4106  dmoprab2 4129  om0x 4164  mapsspw 4347  breng 4381  pw2en 4452  phplem4 4517  php3 4521  php3OLD 4522  inf0 4615  noinfep 4650  r1tr 4664  unir1 4677  rankr1 4684  aceq3 4743  zorn2lem2 4799  zorn2lem4 4801  alephon 4876  alephcard 4878  alephnbtwn 4879  alephgeom 4893  cfub 4920  cardcf 4923  cflecard 4924  cfle 4925  dmaddpi 5030  dmmulpi 5031  infxpidmlem4 7556  alephadd 7584  neiss2 7713  ghgrpi 8133

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 147  df-an 225  df-fn 3199

Copyright terms: Public domain