Theorem dmexd 7899

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

Syntax hints:   → wi 4   ∈ wcel 2108  Vcvv 3459  dom cdm 5654

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pr 5402  ax-un 7729

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 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-opab 5182  df-cnv 5662  df-dm 5664  df-rn 5665

This theorem is referenced by:  fndmexd  7900  unxpwdom2  9602  wemapwe  9711  imadomg  10548  fpwwe2lem11  10655  fpwwe2lem12  10656  hashdmpropge2  14501  prdsplusg  17472  prdsmulr  17473  prdsvsca  17474  prdshom  17481  ssclem  17832  subsubc  17866  efgrcl  19696  dprdgrp  19988  dprdf  19989  dprdssv  19999  f1lindf  21782  decpmatval0  22702  pmatcollpw3lem  22721  ordtrest2lem  23141  ordtrest2  23142  mbfmulc2re  25601  mbfneg  25603  dvnf  25881  dvnbss  25882  dchrptlem3  27229  gsummpt2d  33043  gsumfs2d  33049  cycpmco2lem5  33141  cycpmconjslem2  33166  trclubgNEW  43642  omecl  46532  sssmf  46767  mbfresmf  46768  smfpimltxr  46776  smfpimgtxr  46809  smfres  46819  smfco  46831  iinfssc  49024