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 3960 | . . . 4 ⊢ (𝐴 ⊆ 𝐵 → (〈𝑥, 𝑦〉 ∈ 𝐴 → 〈𝑥, 𝑦〉 ∈ 𝐵)) | |
2 | 1 | eximdv 1914 | . . 3 ⊢ (𝐴 ⊆ 𝐵 → (∃𝑦〈𝑥, 𝑦〉 ∈ 𝐴 → ∃𝑦〈𝑥, 𝑦〉 ∈ 𝐵)) |
3 | vex 3497 | . . . 4 ⊢ 𝑥 ∈ V | |
4 | 3 | eldm2 5764 | . . 3 ⊢ (𝑥 ∈ dom 𝐴 ↔ ∃𝑦〈𝑥, 𝑦〉 ∈ 𝐴) |
5 | 3 | eldm2 5764 | . . 3 ⊢ (𝑥 ∈ dom 𝐵 ↔ ∃𝑦〈𝑥, 𝑦〉 ∈ 𝐵) |
6 | 2, 4, 5 | 3imtr4g 298 | . 2 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ dom 𝐴 → 𝑥 ∈ dom 𝐵)) |
7 | 6 | ssrdv 3972 | 1 ⊢ (𝐴 ⊆ 𝐵 → dom 𝐴 ⊆ dom 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∃wex 1776 ∈ wcel 2110 ⊆ wss 3935 〈cop 4566 dom cdm 5549 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1907 ax-6 1966 ax-7 2011 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2157 ax-12 2173 ax-ext 2793 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3an 1085 df-tru 1536 df-ex 1777 df-nf 1781 df-sb 2066 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-rab 3147 df-v 3496 df-dif 3938 df-un 3940 df-in 3942 df-ss 3951 df-nul 4291 df-if 4467 df-sn 4561 df-pr 4563 df-op 4567 df-br 5059 df-dm 5559 |
This theorem is referenced by: dmeq 5766 dmv 5786 rnss 5803 dmiin 5819 ssxpb 6025 sofld 6038 relrelss 6118 funssxp 6529 fndmdif 6806 fneqeql2 6811 dff3 6860 frxp 7814 fnwelem 7819 funsssuppss 7850 tposss 7887 wfrlem16 7964 smores 7983 smores2 7985 tfrlem13 8020 imafi 8811 hartogslem1 9000 wemapso 9009 r0weon 9432 infxpenlem 9433 brdom3 9944 brdom5 9945 brdom4 9946 fpwwe2lem13 10058 fpwwe2 10059 canth4 10063 canthwelem 10066 pwfseqlem4 10078 nqerf 10346 dmrecnq 10384 uzrdgfni 13320 hashdmpropge2 13835 dmtrclfv 14372 rlimpm 14851 isstruct2 16487 strleun 16585 imasaddfnlem 16795 imasvscafn 16804 isohom 17040 catcoppccl 17362 tsrss 17827 ledm 17828 dirdm 17838 f1omvdmvd 18565 mvdco 18567 f1omvdconj 18568 pmtrfb 18587 pmtrfconj 18588 symggen 18592 symggen2 18593 pmtrdifellem1 18598 pmtrdifellem2 18599 psgnunilem1 18615 gsum2d 19086 lspextmo 19822 dsmmfi 20876 lindfres 20961 mdetdiaglem 21201 tsmsxp 22757 ustssco 22817 setsmstopn 23082 metustexhalf 23160 tngtopn 23253 equivcau 23897 metsscmetcld 23912 dvbssntr 24492 pserdv 25011 subgreldmiedg 27059 hlimcaui 29007 nfpconfp 30371 symgcom2 30723 pmtrcnel 30728 pmtrcnel2 30729 pmtrcnelor 30730 cycpmrn 30780 metideq 31128 esum2d 31347 subgrwlk 32374 fundmpss 33004 frrlem8 33125 frrlem14 33131 fixssdm 33362 filnetlem3 33723 filnetlem4 33724 ssbnd 35060 bnd2lem 35063 ismrcd1 39288 istopclsd 39290 mptrcllem 39966 cnvrcl0 39978 dmtrcl 39980 dfrcl2 40012 relexpss1d 40043 rp-imass 40110 rfovcnvf1od 40343 fourierdlem80 42465 issmflem 42998 |
Copyright terms: Public domain | W3C validator |