Theorem dmexd 7842

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

Syntax hints:   → wi 4   ∈ wcel 2113  Vcvv 3437  dom cdm 5621

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705  ax-sep 5238  ax-nul 5248  ax-pr 5374  ax-un 7677

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4283  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4861  df-br 5096  df-opab 5158  df-cnv 5629  df-dm 5631  df-rn 5632

This theorem is referenced by:  fndmexd  7843  unxpwdom2  9485  wemapwe  9598  imadomg  10436  fpwwe2lem11  10543  fpwwe2lem12  10544  hashdmpropge2  14397  prdsplusg  17369  prdsmulr  17370  prdsvsca  17371  prdshom  17378  ssclem  17734  subsubc  17768  efgrcl  19635  dprdgrp  19927  dprdf  19928  dprdssv  19938  f1lindf  21768  decpmatval0  22699  pmatcollpw3lem  22718  ordtrest2lem  23138  ordtrest2  23139  mbfmulc2re  25596  mbfneg  25598  dvnf  25876  dvnbss  25877  dchrptlem3  27224  gsummpt2d  33060  gsumfs2d  33072  cycpmco2lem5  33140  cycpmconjslem2  33165  trclubgNEW  43775  omecl  46663  sssmf  46898  mbfresmf  46899  smfpimltxr  46907  smfpimgtxr  46940  smfres  46950  smfco  46962  iinfssc  49218