Theorem dmexd 7596

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

Syntax hints:   → wi 4   ∈ wcel 2111  Vcvv 3441  dom cdm 5519

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-nul 5174  ax-pr 5295  ax-un 7441

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-rab 3115  df-v 3443  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-if 4426  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-br 5031  df-opab 5093  df-cnv 5527  df-dm 5529  df-rn 5530

This theorem is referenced by:  fndmexd  7597  unxpwdom2  9036  wemapwe  9144  imadomg  9945  fpwwe2lem12  10052  fpwwe2lem13  10053  hashdmpropge2  13837  prdsplusg  16723  prdsmulr  16724  prdsvsca  16725  prdshom  16732  ssclem  17081  subsubc  17115  efgrcl  18833  dprdgrp  19120  dprdf  19121  dprdssv  19131  f1lindf  20511  decpmatval0  21369  pmatcollpw3lem  21388  ordtrest2lem  21808  ordtrest2  21809  mbfmulc2re  24252  mbfneg  24254  dvnf  24530  dvnbss  24531  dchrptlem3  25850  gsummpt2d  30734  cycpmco2lem5  30822  cycpmconjslem2  30847  trclubgNEW  40318  omecl  43142  sssmf  43372  mbfresmf  43373  smfpimltxr  43381  smfpimgtxr  43413  smfres  43422  smfco  43434  isomgreqve  44343