Theorem dmexd 7845

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

Syntax hints:   → wi 4   ∈ wcel 2113  Vcvv 3440  dom cdm 5624

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 2115  ax-9 2123  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377  ax-un 7680

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 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-opab 5161  df-cnv 5632  df-dm 5634  df-rn 5635

This theorem is referenced by:  fndmexd  7846  unxpwdom2  9493  wemapwe  9606  imadomg  10444  fpwwe2lem11  10552  fpwwe2lem12  10553  hashdmpropge2  14406  prdsplusg  17378  prdsmulr  17379  prdsvsca  17380  prdshom  17387  ssclem  17743  subsubc  17777  efgrcl  19644  dprdgrp  19936  dprdf  19937  dprdssv  19947  f1lindf  21777  decpmatval0  22708  pmatcollpw3lem  22727  ordtrest2lem  23147  ordtrest2  23148  mbfmulc2re  25605  mbfneg  25607  dvnf  25885  dvnbss  25886  dchrptlem3  27233  gsummpt2d  33132  gsumfs2d  33144  cycpmco2lem5  33212  cycpmconjslem2  33237  trclubgNEW  43859  omecl  46747  sssmf  46982  mbfresmf  46983  smfpimltxr  46991  smfpimgtxr  47024  smfres  47034  smfco  47046  iinfssc  49302