MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dmexd Structured version   Visualization version   GIF version

Theorem dmexd 7617
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
StepHypRef Expression
1 dmexd.1 . 2 (𝜑𝐴𝑉)
2 dmexg 7615 . 2 (𝐴𝑉 → dom 𝐴 ∈ V)
31, 2syl 17 1 (𝜑 → dom 𝐴 ∈ V)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2114  Vcvv 3496  dom cdm 5557
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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795  ax-sep 5205  ax-nul 5212  ax-pr 5332  ax-un 7463
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-rab 3149  df-v 3498  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-nul 4294  df-if 4470  df-sn 4570  df-pr 4572  df-op 4576  df-uni 4841  df-br 5069  df-opab 5131  df-cnv 5565  df-dm 5567  df-rn 5568
This theorem is referenced by:  unxpwdom2  9054  wemapwe  9162  imadomg  9958  fpwwe2lem12  10065  fpwwe2lem13  10066  hashdmpropge2  13844  prdsplusg  16733  prdsmulr  16734  prdsvsca  16735  prdshom  16742  ssclem  17091  subsubc  17125  efgrcl  18843  dprdgrp  19129  dprdf  19130  dprdssv  19140  f1lindf  20968  decpmatval0  21374  pmatcollpw3lem  21393  ordtrest2lem  21813  ordtrest2  21814  mbfmulc2re  24251  mbfneg  24253  dvnf  24526  dvnbss  24527  dchrptlem3  25844  gsummpt2d  30689  cycpmco2lem5  30774  cycpmconjslem2  30799  trclubgNEW  39985  omecl  42792  sssmf  43022  mbfresmf  43023  smfpimltxr  43031  smfpimgtxr  43063  smfres  43072  smfco  43084  isomgreqve  43997
  Copyright terms: Public domain W3C validator