Theorem dmexd 7896

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

Syntax hints:   → wi 4   ∈ wcel 2143  Vcvv 3455  dom cdm 5661

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5257  ax-pr 5404  ax-un 7732

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-br 5110  df-opab 5174  df-cnv 5669  df-dm 5671  df-rn 5672

This theorem is referenced by:  fndmexd  7897  unxpwdom2  9546  wemapwe  9662  imadomg  10513  fpwwe2lem11  10621  fpwwe2lem12  10622  hashdmpropge2  14516  prdsplusg  17506  prdsmulr  17507  prdsvsca  17508  prdshom  17515  ssclem  17871  subsubc  17905  efgrcl  19780  dprdgrp  20072  dprdf  20073  dprdssv  20083  f1lindf  21972  decpmatval0  22921  pmatcollpw3lem  22940  ordtrest2lem  23360  ordtrest2  23361  mbfmulc2re  25807  mbfneg  25809  dvnf  26086  dvnbss  26087  dchrptlem3  27430  gsummpt2d  33369  gsumfs2d  33381  cycpmco2lem5  33450  cycpmconjslem2  33475  trclubgNEW  44344  omecl  47217  sssmf  47452  mbfresmf  47453  smfpimltxr  47461  smfpimgtxr  47494  smfres  47504  smfco  47516  iinfssc  49835