Theorem fndm 3587

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 3193	. 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 956  dom cdm 3170  Fun wfun 3176   Fn wfn 3177

This theorem is referenced by:  funfni 3588  fndmu 3589  fnbr 3590  fneu 3592  fnco 3595  fnresdm 3596  fnresdisj 3597  fnssresb 3599  fnima 3604  fn0 3605  funimadisj 3606  fnex 3607  dmopab2 3619  fdm 3631  f1ocnv 3701  f1o00 3714  fnrnfv 3759  fvelimab 3765  eqfnfv 3797  fsn2 3836  fconst3 3850  fconst4 3851  f1fv 3874  tfrlem8 3918  tfrlem9 3919  tfrlem13 3923  tz7.44-2 3929  tz7.44-3 3930  rdgsucopabn 3947  frfnom 3951  tz7.48-1 3956  tz7.48-2 3957  tz7.48-3 3958  tz7.49 3959  oprssoprval 4034  curry1 4098  curry1val 4100  dmoprab2 4123  om0x 4158  mapsspw 4341  breng 4375  pw2en 4446  phplem4 4511  php3 4515  php3OLD 4516  inf0 4606  noinfep 4640  r1tr 4654  unir1 4667  rankr1 4674  aceq3 4733  zorn2lem2 4789  zorn2lem4 4791  alephon 4865  alephcard 4867  alephnbtwn 4868  alephgeom 4882  cfub 4908  cardcf 4911  cflecard 4912  cfle 4913  dmaddpi 5018  dmmulpi 5019  infxpidmlem4 7555  alephadd 7582  neiss2 7716  ghgrpi 8137

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 3193

Copyright terms: Public domain