Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > dmss | Structured version Visualization version GIF version |
Description: Subset theorem for domain. (Contributed by NM, 11-Aug-1994.) |
Ref | Expression |
---|---|
dmss | ⊢ (𝐴 ⊆ 𝐵 → dom 𝐴 ⊆ dom 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ssel 3918 | . . . 4 ⊢ (𝐴 ⊆ 𝐵 → (〈𝑥, 𝑦〉 ∈ 𝐴 → 〈𝑥, 𝑦〉 ∈ 𝐵)) | |
2 | 1 | eximdv 1923 | . . 3 ⊢ (𝐴 ⊆ 𝐵 → (∃𝑦〈𝑥, 𝑦〉 ∈ 𝐴 → ∃𝑦〈𝑥, 𝑦〉 ∈ 𝐵)) |
3 | vex 3434 | . . . 4 ⊢ 𝑥 ∈ V | |
4 | 3 | eldm2 5807 | . . 3 ⊢ (𝑥 ∈ dom 𝐴 ↔ ∃𝑦〈𝑥, 𝑦〉 ∈ 𝐴) |
5 | 3 | eldm2 5807 | . . 3 ⊢ (𝑥 ∈ dom 𝐵 ↔ ∃𝑦〈𝑥, 𝑦〉 ∈ 𝐵) |
6 | 2, 4, 5 | 3imtr4g 295 | . 2 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ dom 𝐴 → 𝑥 ∈ dom 𝐵)) |
7 | 6 | ssrdv 3931 | 1 ⊢ (𝐴 ⊆ 𝐵 → dom 𝐴 ⊆ dom 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∃wex 1785 ∈ wcel 2109 ⊆ wss 3891 〈cop 4572 dom cdm 5588 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1801 ax-4 1815 ax-5 1916 ax-6 1974 ax-7 2014 ax-8 2111 ax-9 2119 ax-ext 2710 |
This theorem depends on definitions: df-bi 206 df-an 396 df-or 844 df-3an 1087 df-tru 1544 df-fal 1554 df-ex 1786 df-sb 2071 df-clab 2717 df-cleq 2731 df-clel 2817 df-rab 3074 df-v 3432 df-dif 3894 df-un 3896 df-in 3898 df-ss 3908 df-nul 4262 df-if 4465 df-sn 4567 df-pr 4569 df-op 4573 df-br 5079 df-dm 5598 |
This theorem is referenced by: dmeq 5809 dmv 5828 rnss 5845 dmiin 5859 ssxpb 6074 sofld 6087 resssxp 6170 relrelss 6173 funssxp 6625 fndmdif 6913 fneqeql2 6918 dff3 6970 frxp 7951 fnwelem 7956 funsssuppss 7990 tposss 8027 frrlem8 8093 frrlem14 8099 wfrlem16OLD 8139 smores 8167 smores2 8169 tfrlem13 8205 imafiALT 9073 hartogslem1 9262 wemapso 9271 dmttrcl 9440 r0weon 9752 infxpenlem 9753 brdom3 10268 brdom5 10269 brdom4 10270 fpwwe2lem12 10382 fpwwe2 10383 canth4 10387 canthwelem 10390 pwfseqlem4 10402 nqerf 10670 dmrecnq 10708 uzrdgfni 13659 hashdmpropge2 14178 dmtrclfv 14710 rlimpm 15190 isstruct2 16831 strleun 16839 imasaddfnlem 17220 imasvscafn 17229 isohom 17469 catcoppccl 17813 catcoppcclOLD 17814 tsrss 18288 ledm 18289 dirdm 18299 f1omvdmvd 19032 mvdco 19034 f1omvdconj 19035 pmtrfb 19054 pmtrfconj 19055 symggen 19059 symggen2 19060 pmtrdifellem1 19065 pmtrdifellem2 19066 psgnunilem1 19082 gsum2d 19554 lspextmo 20299 dsmmfi 20926 lindfres 21011 mdetdiaglem 21728 tsmsxp 23287 ustssco 23347 setsmstopn 23614 metustexhalf 23693 tngtopn 23795 equivcau 24445 metsscmetcld 24460 dvbssntr 25045 pserdv 25569 subgreldmiedg 27631 hlimcaui 29577 nfpconfp 30946 symgcom2 31332 pmtrcnel 31337 pmtrcnel2 31338 pmtrcnelor 31339 cycpmrn 31389 metideq 31822 esum2d 32040 subgrwlk 33073 fundmpss 33719 frxp2 33770 frxp3 33776 fixssdm 34187 filnetlem3 34548 filnetlem4 34549 ssbnd 35925 bnd2lem 35928 ismrcd1 40500 istopclsd 40502 mptrcllem 41174 cnvrcl0 41186 dmtrcl 41188 dfrcl2 41235 relexpss1d 41266 rfovcnvf1od 41565 fourierdlem80 43681 issmflem 44214 |
Copyright terms: Public domain | W3C validator |