Theorem dmexd 7854

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

Syntax hints:   → wi 4   ∈ wcel 2114  Vcvv 3429  dom cdm 5631

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708  ax-sep 5231  ax-pr 5375  ax-un 7689

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-opab 5148  df-cnv 5639  df-dm 5641  df-rn 5642

This theorem is referenced by:  fndmexd  7855  unxpwdom2  9503  wemapwe  9618  imadomg  10456  fpwwe2lem11  10564  fpwwe2lem12  10565  hashdmpropge2  14445  prdsplusg  17421  prdsmulr  17422  prdsvsca  17423  prdshom  17430  ssclem  17786  subsubc  17820  efgrcl  19690  dprdgrp  19982  dprdf  19983  dprdssv  19993  f1lindf  21802  decpmatval0  22729  pmatcollpw3lem  22748  ordtrest2lem  23168  ordtrest2  23169  mbfmulc2re  25615  mbfneg  25617  dvnf  25894  dvnbss  25895  dchrptlem3  27229  gsummpt2d  33110  gsumfs2d  33122  cycpmco2lem5  33191  cycpmconjslem2  33216  trclubgNEW  44045  omecl  46931  sssmf  47166  mbfresmf  47167  smfpimltxr  47175  smfpimgtxr  47208  smfres  47218  smfco  47230  iinfssc  49532