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 2105  Vcvv 3477  dom cdm 5688

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437  ax-un 7753

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-opab 5210  df-cnv 5696  df-dm 5698  df-rn 5699

This theorem is referenced by:  fndmexd  7926  unxpwdom2  9625  wemapwe  9734  imadomg  10571  fpwwe2lem11  10678  fpwwe2lem12  10679  hashdmpropge2  14518  prdsplusg  17504  prdsmulr  17505  prdsvsca  17506  prdshom  17513  ssclem  17866  subsubc  17903  efgrcl  19747  dprdgrp  20039  dprdf  20040  dprdssv  20050  f1lindf  21859  decpmatval0  22785  pmatcollpw3lem  22804  ordtrest2lem  23226  ordtrest2  23227  mbfmulc2re  25696  mbfneg  25698  dvnf  25977  dvnbss  25978  dchrptlem3  27324  gsummpt2d  33034  gsumfs2d  33040  cycpmco2lem5  33132  cycpmconjslem2  33157  trclubgNEW  43607  omecl  46458  sssmf  46693  mbfresmf  46694  smfpimltxr  46702  smfpimgtxr  46735  smfres  46745  smfco  46757