![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > dmss | Structured version Visualization version Unicode version |
Description: Subset theorem for domain. (Contributed by NM, 11-Aug-1994.) |
Ref | Expression |
---|---|
dmss |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ssel 3412 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | eximdv 1772 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | vex 3034 |
. . . 4
![]() ![]() ![]() ![]() | |
4 | 3 | eldm2 5038 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 3 | eldm2 5038 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | 2, 4, 5 | 3imtr4g 278 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
7 | 6 | ssrdv 3424 |
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 1677 ax-4 1690 ax-5 1766 ax-6 1813 ax-7 1859 ax-10 1932 ax-11 1937 ax-12 1950 ax-13 2104 ax-ext 2451 |
This theorem depends on definitions: df-bi 190 df-or 377 df-an 378 df-3an 1009 df-tru 1455 df-ex 1672 df-nf 1676 df-sb 1806 df-clab 2458 df-cleq 2464 df-clel 2467 df-nfc 2601 df-rab 2765 df-v 3033 df-dif 3393 df-un 3395 df-in 3397 df-ss 3404 df-nul 3723 df-if 3873 df-sn 3960 df-pr 3962 df-op 3966 df-br 4396 df-dm 4849 |
This theorem is referenced by: dmeq 5040 dmv 5056 rnss 5069 dmiin 5084 ssxpb 5277 sofld 5290 relrelss 5366 funssxp 5754 fndmdif 6001 fneqeql2 6006 dff3 6050 frxp 6925 fnwelem 6930 funsssuppss 6960 tposss 6992 wfrlem16 7069 smores 7089 smores2 7091 tfrlem13 7126 imafi 7885 hartogslem1 8075 wemapso 8084 r0weon 8461 infxpenlem 8462 brdom3 8974 brdom5 8975 brdom4 8976 fpwwe2lem13 9085 fpwwe2 9086 canth4 9090 canthwelem 9093 pwfseqlem4 9105 nqerf 9373 dmrecnq 9411 uzrdgfni 12210 dmtrclfv 13159 rlimpm 13641 isstruct2 15208 strlemor1 15295 strleun 15298 imasaddfnlem 15512 imasvscafn 15521 isohom 15759 catcoppccl 16081 tsrss 16547 ledm 16548 dirdm 16558 f1omvdmvd 17162 mvdco 17164 f1omvdconj 17165 pmtrfb 17184 pmtrfconj 17185 symggen 17189 symggen2 17190 pmtrdifellem1 17195 pmtrdifellem2 17196 psgnunilem1 17212 gsum2d 17682 lspextmo 18357 dsmmfi 19378 lindfres 19458 mdetdiaglem 19700 tsmsxp 21247 ustssco 21307 setsmstopn 21571 metustexhalf 21649 tngtopn 21736 equivcau 22348 cmetss 22362 dvbssntr 22934 pserdv 23463 uhgrares 25114 umgrares 25130 usgrares 25175 hlimcaui 26970 metideq 28770 esum2d 28988 fundmpss 30478 fixssdm 30744 filnetlem3 31107 filnetlem4 31108 ssbnd 32184 bnd2lem 32187 ismrcd1 35611 istopclsd 35613 mptrcllem 36291 cnvrcl0 36303 dmtrcl 36305 dfrcl2 36337 relexpss1d 36368 rp-imass 36437 fourierdlem80 38162 structgrssvtxlem 39278 subgreldmiedg 39519 uhgres 40199 |
Copyright terms: Public domain | W3C validator |