Theorem dmexd 7828

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

Syntax hints:   → wi 4   ∈ wcel 2111  Vcvv 3436  dom cdm 5611

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-sep 5229  ax-nul 5239  ax-pr 5365  ax-un 7663

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4279  df-if 4471  df-sn 4572  df-pr 4574  df-op 4578  df-uni 4855  df-br 5087  df-opab 5149  df-cnv 5619  df-dm 5621  df-rn 5622

This theorem is referenced by:  fndmexd  7829  unxpwdom2  9469  wemapwe  9582  imadomg  10420  fpwwe2lem11  10527  fpwwe2lem12  10528  hashdmpropge2  14385  prdsplusg  17357  prdsmulr  17358  prdsvsca  17359  prdshom  17366  ssclem  17721  subsubc  17755  efgrcl  19622  dprdgrp  19914  dprdf  19915  dprdssv  19925  f1lindf  21754  decpmatval0  22674  pmatcollpw3lem  22693  ordtrest2lem  23113  ordtrest2  23114  mbfmulc2re  25571  mbfneg  25573  dvnf  25851  dvnbss  25852  dchrptlem3  27199  gsummpt2d  33021  gsumfs2d  33027  cycpmco2lem5  33091  cycpmconjslem2  33116  trclubgNEW  43651  omecl  46541  sssmf  46776  mbfresmf  46777  smfpimltxr  46785  smfpimgtxr  46818  smfres  46828  smfco  46840  iinfssc  49089