Theorem dmss 5849

Description: Subset theorem for domain. (Contributed by NM, 11-Aug-1994.)

Assertion

Ref	Expression
dmss	⊢ (𝐴 ⊆ 𝐵 → dom 𝐴 ⊆ dom 𝐵)

Proof of Theorem dmss

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ssel 3916	. . . 4 ⊢ (𝐴 ⊆ 𝐵 → (⟨𝑥, 𝑦⟩ ∈ 𝐴 → ⟨𝑥, 𝑦⟩ ∈ 𝐵))
2	1	eximdv 1919	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐴 → ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐵))
3		vex 3434	. . . 4 ⊢ 𝑥 ∈ V
4	3	eldm2 5848	. . 3 ⊢ (𝑥 ∈ dom 𝐴 ↔ ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐴)
5	3	eldm2 5848	. . 3 ⊢ (𝑥 ∈ dom 𝐵 ↔ ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐵)
6	2, 4, 5	3imtr4g 296	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ dom 𝐴 → 𝑥 ∈ dom 𝐵))
7	6	ssrdv 3928	1 ⊢ (𝐴 ⊆ 𝐵 → dom 𝐴 ⊆ dom 𝐵)

Syntax hints:   → wi 4  ∃wex 1781   ∈ wcel 2114   ⊆ wss 3890  ⟨cop 4574  dom cdm 5622

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-br 5087  df-dm 5632

This theorem is referenced by:  dmeq  5850  dmv  5869  rnss  5886  dmiin  5900  dmresss  5968  ssxpb  6130  sofld  6143  resssxp  6226  relrelss  6229  funssxp  6688  fndmdif  6986  fneqeql2  6991  dff3  7044  frxp  8067  fnwelem  8072  frxp2  8085  frxp3  8092  funsssuppss  8131  tposss  8168  frrlem8  8234  frrlem14  8240  smores  8283  smores2  8285  tfrlem13  8320  imafi  9216  hartogslem1  9448  wemapso  9457  dmttrcl  9631  r0weon  9923  infxpenlem  9924  brdom3  10439  brdom5  10440  brdom4  10441  fpwwe2lem12  10554  fpwwe2  10555  canth4  10559  canthwelem  10562  pwfseqlem4  10574  nqerf  10842  dmrecnq  10880  uzrdgfni  13882  hashdmpropge2  14407  dmtrclfv  14942  rlimpm  15424  isstruct2  17077  strleun  17085  imasaddfnlem  17450  imasvscafn  17459  isohom  17701  catcoppccl  18042  tsrss  18513  ledm  18514  dirdm  18524  f1omvdmvd  19376  mvdco  19378  f1omvdconj  19379  pmtrfb  19398  pmtrfconj  19399  symggen  19403  symggen2  19404  pmtrdifellem1  19409  pmtrdifellem2  19410  psgnunilem1  19426  gsum2d  19905  lspextmo  21010  dsmmfi  21695  lindfres  21780  mdetdiaglem  22541  tsmsxp  24098  ustssco  24158  setsmstopn  24421  metustexhalf  24499  tngtopn  24593  equivcau  25245  metsscmetcld  25260  dvbssntr  25845  pserdv  26379  noseqrdgfn  28286  subgreldmiedg  29340  hlimcaui  31296  nfpconfp  32694  gsumfs2d  33127  symgcom2  33150  pmtrcnel  33155  pmtrcnel2  33156  pmtrcnelor  33157  cycpmrn  33209  metideq  34043  esum2d  34243  subgrwlk  35320  fundmpss  35955  fixssdm  36092  filnetlem3  36568  filnetlem4  36569  ssbnd  38100  bnd2lem  38103  ismrcd1  43129  istopclsd  43131  mptrcllem  44043  cnvrcl0  44055  dmtrcl  44057  dfrcl2  44104  relexpss1d  44135  rfovcnvf1od  44434  fourierdlem80  46618  issmflem  47159