Theorem dmexd 7900

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

Syntax hints:   → wi 4   ∈ wcel 2104  Vcvv 3472  dom cdm 5677

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701  ax-sep 5300  ax-nul 5307  ax-pr 5428  ax-un 7729

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-rab 3431  df-v 3474  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-opab 5212  df-cnv 5685  df-dm 5687  df-rn 5688

This theorem is referenced by:  fndmexd  7901  unxpwdom2  9587  wemapwe  9696  imadomg  10533  fpwwe2lem11  10640  fpwwe2lem12  10641  hashdmpropge2  14450  prdsplusg  17410  prdsmulr  17411  prdsvsca  17412  prdshom  17419  ssclem  17772  subsubc  17809  efgrcl  19626  dprdgrp  19918  dprdf  19919  dprdssv  19929  f1lindf  21598  decpmatval0  22488  pmatcollpw3lem  22507  ordtrest2lem  22929  ordtrest2  22930  mbfmulc2re  25399  mbfneg  25401  dvnf  25678  dvnbss  25679  dchrptlem3  27003  gsummpt2d  32469  cycpmco2lem5  32557  cycpmconjslem2  32582  trclubgNEW  42673  omecl  45519  sssmf  45754  mbfresmf  45755  smfpimltxr  45763  smfpimgtxr  45796  smfres  45806  smfco  45818  isomgreqve  46793