Theorem fndm 2723

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 2433	. 2 ⊢ (F Fn A ↔ (Fun F ∧ dom F = A))
2	1	pm3.27bd 263	1 ⊢ (F Fn A → dom F = A)

Syntax hints:   → wi 2   = wceq 1091  dom cdm 2410  Fun wfun 2416   Fn wfn 2417

This theorem is referenced by:  funfni 2724  fndmu 2725  fnbr 2726  fneu 2728  fnresdm 2731  fnresdisj 2732  fnssres 2734  fnima 2738  fn0 2739  fnex 2740  fdm 2756  f1ocnv 2811  f1o00 2823  fniunfv 2860  cleqfv 2880  fsn2 2896  f1fv 2916  tfrlem8 2956  tfrlem9 2957  tfrlem13 2961  tz7.44-2 2967  tz7.44-3 2968  rdgsucopabn 2985  frfnom 2989  tz7.48-1 2994  tz7.48-2 2995  tz7.48-3 2996  tz7.49 2997  dmoprab2 3040  om0x 3126  breng 3280  pw2en 3348  phplem5 3407  php3 3411  inf0 3457  r1tr 3498  unir1 3511  rankr1 3518  aceq3 3556  ac6lem 3575  zornlem2 3604  zornlem4 3606  alephon 3671  alephcard 3673  alephnbtwn 3674  alephgeom 3687  cfub 3703  cardcf 3706  cflecard 3707  cfle 3708  dmaddpi 3812  dmmulpi 3813  infxpidmlem4 4936

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

This theorem depends on definitions:  df-bi 128  df-an 198  df-fn 2433

metamath.org