![]() |
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 3815 | . . . 4 ⊢ (𝐴 ⊆ 𝐵 → (〈𝑥, 𝑦〉 ∈ 𝐴 → 〈𝑥, 𝑦〉 ∈ 𝐵)) | |
2 | 1 | eximdv 1960 | . . 3 ⊢ (𝐴 ⊆ 𝐵 → (∃𝑦〈𝑥, 𝑦〉 ∈ 𝐴 → ∃𝑦〈𝑥, 𝑦〉 ∈ 𝐵)) |
3 | vex 3401 | . . . 4 ⊢ 𝑥 ∈ V | |
4 | 3 | eldm2 5567 | . . 3 ⊢ (𝑥 ∈ dom 𝐴 ↔ ∃𝑦〈𝑥, 𝑦〉 ∈ 𝐴) |
5 | 3 | eldm2 5567 | . . 3 ⊢ (𝑥 ∈ dom 𝐵 ↔ ∃𝑦〈𝑥, 𝑦〉 ∈ 𝐵) |
6 | 2, 4, 5 | 3imtr4g 288 | . 2 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ dom 𝐴 → 𝑥 ∈ dom 𝐵)) |
7 | 6 | ssrdv 3827 | 1 ⊢ (𝐴 ⊆ 𝐵 → dom 𝐴 ⊆ dom 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∃wex 1823 ∈ wcel 2107 ⊆ wss 3792 〈cop 4404 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 2055 ax-9 2116 ax-10 2135 ax-11 2150 ax-12 2163 ax-13 2334 ax-ext 2754 |
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-clab 2764 df-cleq 2770 df-clel 2774 df-nfc 2921 df-rab 3099 df-v 3400 df-dif 3795 df-un 3797 df-in 3799 df-ss 3806 df-nul 4142 df-if 4308 df-sn 4399 df-pr 4401 df-op 4405 df-br 4887 df-dm 5365 |
This theorem is referenced by: dmeq 5569 dmv 5586 rnss 5599 dmiin 5615 ssxpb 5822 sofld 5835 relrelss 5913 funssxp 6311 fndmdif 6584 fneqeql2 6589 dff3 6636 frxp 7568 fnwelem 7573 funsssuppss 7603 tposss 7635 wfrlem16 7713 smores 7732 smores2 7734 tfrlem13 7769 imafi 8547 hartogslem1 8736 wemapso 8745 r0weon 9168 infxpenlem 9169 brdom3 9685 brdom5 9686 brdom4 9687 fpwwe2lem13 9799 fpwwe2 9800 canth4 9804 canthwelem 9807 pwfseqlem4 9819 nqerf 10087 dmrecnq 10125 uzrdgfni 13076 hashdmpropge2 13579 dmtrclfv 14166 rlimpm 14639 isstruct2 16265 strleun 16364 imasaddfnlem 16574 imasvscafn 16583 isohom 16821 catcoppccl 17143 tsrss 17609 ledm 17610 dirdm 17620 f1omvdmvd 18246 mvdco 18248 f1omvdconj 18249 pmtrfb 18268 pmtrfconj 18269 symggen 18273 symggen2 18274 pmtrdifellem1 18279 pmtrdifellem2 18280 psgnunilem1 18296 gsum2d 18757 lspextmo 19451 dsmmfi 20481 lindfres 20566 mdetdiaglem 20809 tsmsxp 22366 ustssco 22426 setsmstopn 22691 metustexhalf 22769 tngtopn 22862 equivcau 23506 metsscmetcld 23521 dvbssntr 24101 pserdv 24620 subgreldmiedg 26630 hlimcaui 28665 metideq 30534 esum2d 30753 fundmpss 32257 fixssdm 32602 filnetlem3 32963 filnetlem4 32964 ssbnd 34213 bnd2lem 34216 ismrcd1 38225 istopclsd 38227 mptrcllem 38881 cnvrcl0 38893 dmtrcl 38895 dfrcl2 38927 relexpss1d 38958 rp-imass 39025 rfovcnvf1od 39258 fourierdlem80 41334 issmflem 41867 |
Copyright terms: Public domain | W3C validator |