Theorem dmexd 7879

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

Syntax hints:   → wi 4   ∈ wcel 2109  Vcvv 3447  dom cdm 5638

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387  ax-un 7711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-cnv 5646  df-dm 5648  df-rn 5649

This theorem is referenced by:  fndmexd  7880  unxpwdom2  9541  wemapwe  9650  imadomg  10487  fpwwe2lem11  10594  fpwwe2lem12  10595  hashdmpropge2  14448  prdsplusg  17421  prdsmulr  17422  prdsvsca  17423  prdshom  17430  ssclem  17781  subsubc  17815  efgrcl  19645  dprdgrp  19937  dprdf  19938  dprdssv  19948  f1lindf  21731  decpmatval0  22651  pmatcollpw3lem  22670  ordtrest2lem  23090  ordtrest2  23091  mbfmulc2re  25549  mbfneg  25551  dvnf  25829  dvnbss  25830  dchrptlem3  27177  gsummpt2d  32989  gsumfs2d  32995  cycpmco2lem5  33087  cycpmconjslem2  33112  trclubgNEW  43607  omecl  46501  sssmf  46736  mbfresmf  46737  smfpimltxr  46745  smfpimgtxr  46778  smfres  46788  smfco  46800  iinfssc  49046