Theorem dmexd 7746

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

Syntax hints:   → wi 4   ∈ wcel 2110  Vcvv 3431  dom cdm 5590

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-ext 2711  ax-sep 5227  ax-nul 5234  ax-pr 5356  ax-un 7582

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1545  df-fal 1555  df-ex 1787  df-sb 2072  df-clab 2718  df-cleq 2732  df-clel 2818  df-rab 3075  df-v 3433  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-nul 4263  df-if 4466  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4846  df-br 5080  df-opab 5142  df-cnv 5598  df-dm 5600  df-rn 5601

This theorem is referenced by:  fndmexd  7747  unxpwdom2  9325  wemapwe  9433  imadomg  10291  fpwwe2lem11  10398  fpwwe2lem12  10399  hashdmpropge2  14195  prdsplusg  17167  prdsmulr  17168  prdsvsca  17169  prdshom  17176  ssclem  17529  subsubc  17566  efgrcl  19319  dprdgrp  19606  dprdf  19607  dprdssv  19617  f1lindf  21027  decpmatval0  21911  pmatcollpw3lem  21930  ordtrest2lem  22352  ordtrest2  22353  mbfmulc2re  24810  mbfneg  24812  dvnf  25089  dvnbss  25090  dchrptlem3  26412  gsummpt2d  31305  cycpmco2lem5  31393  cycpmconjslem2  31418  trclubgNEW  41196  omecl  44012  sssmf  44242  mbfresmf  44243  smfpimltxr  44251  smfpimgtxr  44283  smfres  44292  smfco  44304  isomgreqve  45246