![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > dmexg | Structured version Visualization version Unicode version |
Description: The domain of a set is a set. Corollary 6.8(2) of [TakeutiZaring] p. 26. (Contributed by NM, 7-Apr-1995.) |
Ref | Expression |
---|---|
dmexg |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | uniexg 6615 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | uniexg 6615 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | ssun1 3609 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | dmrnssfld 5112 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 3, 4 | sstri 3453 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | ssexg 4563 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
7 | 5, 6 | mpan 681 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
8 | 1, 2, 7 | 3syl 18 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1680 ax-4 1693 ax-5 1769 ax-6 1816 ax-7 1862 ax-8 1900 ax-9 1907 ax-10 1926 ax-11 1931 ax-12 1944 ax-13 2102 ax-ext 2442 ax-sep 4539 ax-nul 4548 ax-pr 4653 ax-un 6610 |
This theorem depends on definitions: df-bi 190 df-or 376 df-an 377 df-3an 993 df-tru 1458 df-ex 1675 df-nf 1679 df-sb 1809 df-eu 2314 df-mo 2315 df-clab 2449 df-cleq 2455 df-clel 2458 df-nfc 2592 df-ne 2635 df-rex 2755 df-rab 2758 df-v 3059 df-dif 3419 df-un 3421 df-in 3423 df-ss 3430 df-nul 3744 df-if 3894 df-sn 3981 df-pr 3983 df-op 3987 df-uni 4213 df-br 4417 df-opab 4476 df-cnv 4861 df-dm 4863 df-rn 4864 |
This theorem is referenced by: dmex 6753 iprc 6755 exse2 6759 xpexr2 6761 xpexcnv 6762 soex 6763 cnvexg 6766 coexg 6771 dmfex 6778 cofunexg 6784 offval3 6814 suppval 6943 funsssuppss 6968 suppss 6972 suppssov1 6974 suppssfv 6978 tposexg 7013 tfrlem12 7133 tfrlem13 7134 erexb 7414 f1vrnfibi 7885 oion 8077 unxpwdom2 8129 wemapwe 8228 imadomg 8988 fpwwe2lem3 9084 fpwwe2lem12 9092 fpwwe2lem13 9093 hashfn 12586 hashimarn 12643 trclexlem 13107 relexp0g 13134 relexpsucnnr 13137 o1of2 13725 prdsplusg 15405 prdsmulr 15406 prdsvsca 15407 prdshom 15414 isofn 15729 ssclem 15773 ssc2 15776 ssctr 15779 subsubc 15807 resf1st 15848 resf2nd 15849 funcres 15850 efgrcl 17414 dprddomprc 17681 dprdval0prc 17683 dprdgrp 17686 dprdf 17687 dprdssv 17698 subgdmdprd 17716 dprd2da 17724 f1lindf 19429 decpmatval0 19837 pmatcollpw3lem 19856 ordtbaslem 20253 ordtuni 20255 ordtbas2 20256 ordtbas 20257 ordttopon 20258 ordtopn1 20259 ordtopn2 20260 ordtrest2lem 20268 ordtrest2 20269 txindislem 20697 ordthmeolem 20865 ptcmplem2 21117 tuslem 21331 mbfmulc2re 22653 mbfneg 22655 dvnff 22926 dchrptlem3 24243 fiusgraedgfi 25184 sizeusglecusg 25263 wlks 25296 wlkres 25299 trls 25315 crcts 25399 cycls 25400 vdusgraval 25684 vdgrnn0pnf 25686 hashnbgravdg 25690 usgravd0nedg 25695 iseupa 25742 vdgn0frgrav2 25801 vdgn1frgrav2 25803 vdgfrgragt2 25804 ismgmOLD 26097 gsummpt2d 28593 ofcfval3 28972 braew 29114 omsval 29166 omsvalOLD 29170 sibfof 29222 sitmcl 29233 cndprobval 29315 bdayval 30584 bdayfo 30613 tailf 31080 tailfb 31082 rclexi 36267 rtrclexlem 36268 trclubgNEW 36270 cnvrcl0 36277 dfrtrcl5 36281 relexpmulg 36347 relexp01min 36350 relexpxpmin 36354 unidmex 37426 caragenval 38352 omecl 38362 caragenunidm 38367 opabn1stprc 39047 fundmge2nop 39068 fun2dmnop 39069 structgrssvtxlem 39171 vtxdgf 39581 offval0 40576 |
Copyright terms: Public domain | W3C validator |