Theorem dmexd 7925

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

Hypothesis

Ref	Expression
dmexd.1	⊢ (𝜑 → 𝐴 ∈ 𝑉)

Assertion

Ref	Expression
dmexd	⊢ (𝜑 → dom 𝐴 ∈ V)

Proof of Theorem dmexd

Step	Hyp	Ref	Expression
1		dmexd.1	. 2 ⊢ (𝜑 → 𝐴 ∈ 𝑉)
2		dmexg 7923	. 2 ⊢ (𝐴 ∈ 𝑉 → dom 𝐴 ∈ V)
3	1, 2	syl 17	1 ⊢ (𝜑 → dom 𝐴 ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2108  Vcvv 3480  dom cdm 5685

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432  ax-un 7755

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-cnv 5693  df-dm 5695  df-rn 5696

This theorem is referenced by:  fndmexd  7926  unxpwdom2  9628  wemapwe  9737  imadomg  10574  fpwwe2lem11  10681  fpwwe2lem12  10682  hashdmpropge2  14522  prdsplusg  17503  prdsmulr  17504  prdsvsca  17505  prdshom  17512  ssclem  17863  subsubc  17898  efgrcl  19733  dprdgrp  20025  dprdf  20026  dprdssv  20036  f1lindf  21842  decpmatval0  22770  pmatcollpw3lem  22789  ordtrest2lem  23211  ordtrest2  23212  mbfmulc2re  25683  mbfneg  25685  dvnf  25963  dvnbss  25964  dchrptlem3  27310  gsummpt2d  33052  gsumfs2d  33058  cycpmco2lem5  33150  cycpmconjslem2  33175  trclubgNEW  43631  omecl  46518  sssmf  46753  mbfresmf  46754  smfpimltxr  46762  smfpimgtxr  46795  smfres  46805  smfco  46817