![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > dmexd | Structured version Visualization version GIF version |
Description: The domain of a set is a set. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
Ref | Expression |
---|---|
dmexd.1 | ⊢ (𝜑 → 𝐴 ∈ 𝑉) |
Ref | Expression |
---|---|
dmexd | ⊢ (𝜑 → dom 𝐴 ∈ V) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dmexd.1 | . 2 ⊢ (𝜑 → 𝐴 ∈ 𝑉) | |
2 | dmexg 7375 | . 2 ⊢ (𝐴 ∈ 𝑉 → dom 𝐴 ∈ V) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → dom 𝐴 ∈ V) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2106 Vcvv 3397 dom cdm 5355 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 ax-5 1953 ax-6 2021 ax-7 2054 ax-8 2108 ax-9 2115 ax-10 2134 ax-11 2149 ax-12 2162 ax-13 2333 ax-ext 2753 ax-sep 5017 ax-nul 5025 ax-pr 5138 ax-un 7226 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 837 df-3an 1073 df-tru 1605 df-ex 1824 df-nf 1828 df-sb 2012 df-mo 2550 df-eu 2586 df-clab 2763 df-cleq 2769 df-clel 2773 df-nfc 2920 df-rex 3095 df-rab 3098 df-v 3399 df-dif 3794 df-un 3796 df-in 3798 df-ss 3805 df-nul 4141 df-if 4307 df-sn 4398 df-pr 4400 df-op 4404 df-uni 4672 df-br 4887 df-opab 4949 df-cnv 5363 df-dm 5365 df-rn 5366 |
This theorem is referenced by: unxpwdom2 8782 wemapwe 8891 imadomg 9691 fpwwe2lem12 9798 fpwwe2lem13 9799 hashdmpropge2 13579 prdsplusg 16504 prdsmulr 16505 prdsvsca 16506 prdshom 16513 ssclem 16864 subsubc 16898 efgrcl 18512 dprdgrp 18791 dprdf 18792 dprdssv 18802 f1lindf 20565 decpmatval0 20976 pmatcollpw3lem 20995 ordtrest2lem 21415 ordtrest2 21416 mbfmulc2re 23852 mbfneg 23854 dchrptlem3 25443 gsummpt2d 30357 trclubgNEW 38874 omecl 41636 sssmf 41866 mbfresmf 41867 smfpimltxr 41875 smfpimgtxr 41907 smfres 41916 smfco 41928 isomgreqve 42730 |
Copyright terms: Public domain | W3C validator |