Theorem dmexd 7847

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

Syntax hints:   → wi 4   ∈ wcel 2121  Vcvv 3433  dom cdm 5621

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713  ax-sep 5221  ax-pr 5365  ax-un 7682

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-3an 1095  df-tru 1551  df-fal 1561  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-rab 3394  df-v 3435  df-dif 3888  df-un 3890  df-in 3892  df-ss 3902  df-nul 4265  df-if 4458  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4842  df-br 5076  df-opab 5138  df-cnv 5629  df-dm 5631  df-rn 5632

This theorem is referenced by:  fndmexd  7848  unxpwdom2  9497  wemapwe  9613  imadomg  10451  fpwwe2lem11  10559  fpwwe2lem12  10560  hashdmpropge2  14440  prdsplusg  17416  prdsmulr  17417  prdsvsca  17418  prdshom  17425  ssclem  17781  subsubc  17815  efgrcl  19685  dprdgrp  19977  dprdf  19978  dprdssv  19988  f1lindf  21801  decpmatval0  22751  pmatcollpw3lem  22770  ordtrest2lem  23190  ordtrest2  23191  mbfmulc2re  25637  mbfneg  25639  dvnf  25916  dvnbss  25917  dchrptlem3  27251  gsummpt2d  33134  gsumfs2d  33146  cycpmco2lem5  33215  cycpmconjslem2  33240  trclubgNEW  44077  omecl  46960  sssmf  47195  mbfresmf  47196  smfpimltxr  47204  smfpimgtxr  47237  smfres  47247  smfco  47259  iinfssc  49561