Theorem dmexd 7843

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 7841	. 2 ⊢ (𝐴 ∈ 𝑉 → dom 𝐴 ∈ V)
3	1, 2	syl 17	1 ⊢ (𝜑 → dom 𝐴 ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2119  Vcvv 3431  dom cdm 5618

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711  ax-sep 5218  ax-pr 5362  ax-un 7678

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-br 5073  df-opab 5135  df-cnv 5626  df-dm 5628  df-rn 5629

This theorem is referenced by:  fndmexd  7844  unxpwdom2  9493  wemapwe  9609  imadomg  10447  fpwwe2lem11  10555  fpwwe2lem12  10556  hashdmpropge2  14436  prdsplusg  17412  prdsmulr  17413  prdsvsca  17414  prdshom  17421  ssclem  17777  subsubc  17811  efgrcl  19681  dprdgrp  19973  dprdf  19974  dprdssv  19984  f1lindf  21797  decpmatval0  22747  pmatcollpw3lem  22766  ordtrest2lem  23186  ordtrest2  23187  mbfmulc2re  25633  mbfneg  25635  dvnf  25912  dvnbss  25913  dchrptlem3  27247  gsummpt2d  33130  gsumfs2d  33142  cycpmco2lem5  33211  cycpmconjslem2  33236  trclubgNEW  44062  omecl  46946  sssmf  47181  mbfresmf  47182  smfpimltxr  47190  smfpimgtxr  47223  smfres  47233  smfco  47245  iinfssc  49547