Theorem fndm 3579

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 3188	. 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 954  dom cdm 3165  Fun wfun 3171   Fn wfn 3172

This theorem is referenced by:  funfni 3580  fndmu 3581  fnbr 3582  fneu 3584  fnco 3587  fnresdm 3588  fnresdisj 3589  fnssresb 3591  fnima 3596  fn0 3597  funimadisj 3598  fnex 3599  dmopab2 3611  fdm 3623  f1ocnv 3692  f1o00 3705  fnrnfv 3750  fvelimab 3756  eqfnfv 3788  fsn2 3827  fconst3 3841  fconst4 3842  f1fv 3865  tfrlem8 3909  tfrlem9 3910  tfrlem13 3914  tz7.44-2 3920  tz7.44-3 3921  rdgsucopabn 3938  frfnom 3942  tz7.48-1 3947  tz7.48-2 3948  tz7.48-3 3949  tz7.49 3950  oprssoprval 4025  curry1 4088  curry1val 4090  dmoprab2 4113  om0x 4148  mapsspw 4331  breng 4363  pw2en 4432  phplem4 4497  php3 4501  inf0 4586  noinfep 4620  r1tr 4634  unir1 4647  rankr1 4654  aceq3 4713  zorn2lem2 4769  zorn2lem4 4771  alephon 4845  alephcard 4847  alephnbtwn 4848  alephgeom 4862  cfub 4888  cardcf 4891  cflecard 4892  cfle 4893  dmaddpi 4998  dmmulpi 4999  infxpidmlem4 7506  alephadd 7532  neiss2 7666  ghgrpi 8089

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 3188

Copyright terms: Public domain