Description: The domain of a function. (Contributed by Glauco Siliprandi, 23Oct2021)
Ref  Expression  

Hypothesis  fndmd.1   ( ph > F Fn A ) 

Assertion  fndmd   ( ph > dom F = A ) 
Step  Hyp  Ref  Expression 

1  fndmd.1   ( ph > F Fn A ) 

2  fndm   ( F Fn A > dom F = A ) 

3  1 2  syl   ( ph > dom F = A ) 