Theorem dmexd 7911

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

Syntax hints:   → wi 4   ∈ wcel 2098  Vcvv 3461  dom cdm 5678

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696  ax-sep 5300  ax-nul 5307  ax-pr 5429  ax-un 7741

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-rab 3419  df-v 3463  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4323  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4910  df-br 5150  df-opab 5212  df-cnv 5686  df-dm 5688  df-rn 5689

This theorem is referenced by:  fndmexd  7912  unxpwdom2  9613  wemapwe  9722  imadomg  10559  fpwwe2lem11  10666  fpwwe2lem12  10667  hashdmpropge2  14480  prdsplusg  17443  prdsmulr  17444  prdsvsca  17445  prdshom  17452  ssclem  17805  subsubc  17842  efgrcl  19682  dprdgrp  19974  dprdf  19975  dprdssv  19985  f1lindf  21773  decpmatval0  22710  pmatcollpw3lem  22729  ordtrest2lem  23151  ordtrest2  23152  mbfmulc2re  25621  mbfneg  25623  dvnf  25901  dvnbss  25902  dchrptlem3  27244  gsummpt2d  32853  cycpmco2lem5  32943  cycpmconjslem2  32968  trclubgNEW  43190  omecl  46029  sssmf  46264  mbfresmf  46265  smfpimltxr  46273  smfpimgtxr  46306  smfres  46316  smfco  46328