Theorem dmexd 7949

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147  Vcvv 3454  dom cdm 5658

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5255  ax-pr 5398  ax-un 7783

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-br 5109  df-opab 5174  df-cnv 5666  df-dm 5668  df-rn 5669

This theorem is used by:  fndmexd  7950  unxpwdom2  9619  wemapwe  9735  imadomg  10652  fpwwe2lem11  10765  fpwwe2lem12  10766  hashdmpropge2  14669  prdsplusg  17679  prdsmulr  17680  prdsvsca  17681  prdshom  17688  ssclem  18044  subsubc  18078  efgrcl  19980  dprdgrp  20272  dprdf  20273  dprdssv  20283  f1lindf  22183  decpmatval0  23137  pmatcollpw3lem  23156  ordtrest2lem  23576  ordtrest2  23577  mbfmulc2re  26024  mbfneg  26026  dvnf  26302  dvnbss  26303  dchrptlem3  27650  gsummpt2d  33709  gsumfs2d  33721  cycpmco2lem5  33790  cycpmconjslem2  33815  trclubgNEW  44879  omecl  47786  sssmf  48021  mbfresmf  48022  smfpimltxr  48030  smfpimgtxr  48063  smfres  48073  smfco  48085  iinfssc  50502