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

Theorem dmexd 7604
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 7602 . 2 (𝐴𝑉 → dom 𝐴 ∈ V)
31, 2syl 17 1 (𝜑 → dom 𝐴 ∈ V)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2105  Vcvv 3492  dom cdm 5548
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-sep 5194  ax-nul 5201  ax-pr 5320  ax-un 7450
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-rex 3141  df-rab 3144  df-v 3494  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-nul 4289  df-if 4464  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4831  df-br 5058  df-opab 5120  df-cnv 5556  df-dm 5558  df-rn 5559
This theorem is referenced by:  unxpwdom2  9040  wemapwe  9148  imadomg  9944  fpwwe2lem12  10051  fpwwe2lem13  10052  hashdmpropge2  13829  prdsplusg  16719  prdsmulr  16720  prdsvsca  16721  prdshom  16728  ssclem  17077  subsubc  17111  efgrcl  18770  dprdgrp  19056  dprdf  19057  dprdssv  19067  f1lindf  20894  decpmatval0  21300  pmatcollpw3lem  21319  ordtrest2lem  21739  ordtrest2  21740  mbfmulc2re  24176  mbfneg  24178  dvnf  24451  dvnbss  24452  dchrptlem3  25769  gsummpt2d  30614  cycpmco2lem5  30699  cycpmconjslem2  30724  trclubgNEW  39856  omecl  42662  sssmf  42892  mbfresmf  42893  smfpimltxr  42901  smfpimgtxr  42933  smfres  42942  smfco  42954  isomgreqve  43867
  Copyright terms: Public domain W3C validator