Theorem dmexd 7855

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

Syntax hints:   → wi 4   ∈ wcel 2114  Vcvv 3442  dom cdm 5632

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5243  ax-pr 5379  ax-un 7690

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-cnv 5640  df-dm 5642  df-rn 5643

This theorem is referenced by:  fndmexd  7856  unxpwdom2  9505  wemapwe  9618  imadomg  10456  fpwwe2lem11  10564  fpwwe2lem12  10565  hashdmpropge2  14418  prdsplusg  17390  prdsmulr  17391  prdsvsca  17392  prdshom  17399  ssclem  17755  subsubc  17789  efgrcl  19656  dprdgrp  19948  dprdf  19949  dprdssv  19959  f1lindf  21789  decpmatval0  22720  pmatcollpw3lem  22739  ordtrest2lem  23159  ordtrest2  23160  mbfmulc2re  25617  mbfneg  25619  dvnf  25897  dvnbss  25898  dchrptlem3  27245  gsummpt2d  33143  gsumfs2d  33155  cycpmco2lem5  33224  cycpmconjslem2  33249  trclubgNEW  43974  omecl  46861  sssmf  47096  mbfresmf  47097  smfpimltxr  47105  smfpimgtxr  47138  smfres  47148  smfco  47160  iinfssc  49416