![]() |
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 3425 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | eximdv 1763 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | vex 3047 |
. . . 4
![]() ![]() ![]() ![]() | |
4 | 3 | eldm2 5032 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 3 | eldm2 5032 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | 2, 4, 5 | 3imtr4g 274 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
7 | 6 | ssrdv 3437 |
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 1668 ax-4 1681 ax-5 1757 ax-6 1804 ax-7 1850 ax-10 1914 ax-11 1919 ax-12 1932 ax-13 2090 ax-ext 2430 |
This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3an 986 df-tru 1446 df-ex 1663 df-nf 1667 df-sb 1797 df-clab 2437 df-cleq 2443 df-clel 2446 df-nfc 2580 df-rab 2745 df-v 3046 df-dif 3406 df-un 3408 df-in 3410 df-ss 3417 df-nul 3731 df-if 3881 df-sn 3968 df-pr 3970 df-op 3974 df-br 4402 df-dm 4843 |
This theorem is referenced by: dmeq 5034 dmv 5049 rnss 5062 dmiin 5077 ssxpb 5270 sofld 5283 relrelss 5358 funssxp 5740 fndmdif 5984 fneqeql2 5989 dff3 6033 frxp 6903 fnwelem 6908 funsssuppss 6938 tposss 6971 wfrlem16 7048 smores 7068 smores2 7070 tfrlem13 7105 imafi 7864 hartogslem1 8054 wemapso 8063 r0weon 8440 infxpenlem 8441 brdom3 8953 brdom5 8954 brdom4 8955 fpwwe2lem13 9064 fpwwe2 9065 canth4 9069 canthwelem 9072 pwfseqlem4 9084 nqerf 9352 dmrecnq 9390 uzrdgfni 12169 dmtrclfv 13075 rlimpm 13557 isstruct2 15123 strlemor1 15210 strleun 15213 imasaddfnlem 15427 imasvscafn 15436 isohom 15674 catcoppccl 15996 tsrss 16462 ledm 16463 dirdm 16473 f1omvdmvd 17077 mvdco 17079 f1omvdconj 17080 pmtrfb 17099 pmtrfconj 17100 symggen 17104 symggen2 17105 pmtrdifellem1 17110 pmtrdifellem2 17111 psgnunilem1 17127 gsum2d 17597 lspextmo 18272 dsmmfi 19294 lindfres 19374 mdetdiaglem 19616 tsmsxp 21162 ustssco 21222 setsmstopn 21486 metustexhalf 21564 tngtopn 21651 equivcau 22263 cmetss 22277 dvbssntr 22848 pserdv 23377 uhgrares 25028 umgrares 25044 usgrares 25089 hlimcaui 26882 metideq 28689 esum2d 28907 fundmpss 30400 fixssdm 30666 filnetlem3 31029 filnetlem4 31030 ssbnd 32113 bnd2lem 32116 ismrcd1 35534 istopclsd 35536 mptrcllem 36214 cnvrcl0 36226 dmtrcl 36228 dfrcl2 36260 relexpss1d 36291 rp-imass 36360 fourierdlem80 38044 structgrssvtxlem 39111 subgreldmiedg 39338 uhgres 39678 |
Copyright terms: Public domain | W3C validator |