Theorem ffdmd 6735

Description: The domain of a function. (Contributed by Glauco Siliprandi, 26-Jun-2021.)

Hypothesis

Ref	Expression
ffdmd.1	⊢ (𝜑 → 𝐹:𝐴⟶𝐵)

Assertion

Ref	Expression
ffdmd	⊢ (𝜑 → 𝐹:dom 𝐹⟶𝐵)

Proof of Theorem ffdmd

Step	Hyp	Ref	Expression
1		ffdmd.1	. . 3 ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)
2		ffdm 6734	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → (𝐹:dom 𝐹⟶𝐵 ∧ dom 𝐹 ⊆ 𝐴))
3	1, 2	syl 17	. 2 ⊢ (𝜑 → (𝐹:dom 𝐹⟶𝐵 ∧ dom 𝐹 ⊆ 𝐴))
4	3	simpld 495	1 ⊢ (𝜑 → 𝐹:dom 𝐹⟶𝐵)

Syntax hints:   → wi 4   ∧ wa 396   ⊆ wss 3944  dom cdm 5669  ⟶wf 6528

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3475  df-in 3951  df-ss 3961  df-fn 6535  df-f 6536

This theorem is referenced by:  ordtypelem5  9499  ablfaclem2  19915  ablfac2  19918  f1lindf  21310  lmcnp  22737  upgr1e  28238  upgrres1  28435  umgrres1  28436  umgr2v2e  28647  pliguhgr  29602  s3f1  31984  ccatf1  31986  swrdf1  31991  tocyccntz  32174  dfac21  41579  xlimmnfvlem1  44321  xlimpnfvlem1  44325  itgperiod  44470  issmfd  45224  issmfdf  45226  cnfsmf  45229  issmfled  45246  issmfgtd  45250  smfsuplem1  45300