Theorem dmss 5883

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 3933	. . . 4 ⊢ (𝐴 ⊆ 𝐵 → (⟨𝑥, 𝑦⟩ ∈ 𝐴 → ⟨𝑥, 𝑦⟩ ∈ 𝐵))
2	1	eximdv 1940	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐴 → ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐵))
3		vex 3461	. . . 4 ⊢ 𝑥 ∈ V
4	3	eldm2 5882	. . 3 ⊢ (𝑥 ∈ dom 𝐴 ↔ ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐴)
5	3	eldm2 5882	. . 3 ⊢ (𝑥 ∈ dom 𝐵 ↔ ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐵)
6	2, 4, 5	3imtr4g 299	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ dom 𝐴 → 𝑥 ∈ dom 𝐵))
7	6	ssrdv 3945	1 ⊢ (𝐴 ⊆ 𝐵 → dom 𝐴 ⊆ dom 𝐵)

Syntax hints:   → wi 4  ∃wex 1802   ∈ wcel 2145   ⊆ wss 3907  ⟨cop 4591  dom cdm 5652

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3418  df-v 3459  df-dif 3910  df-un 3912  df-ss 3924  df-nul 4289  df-if 4484  df-sn 4586  df-pr 4588  df-op 4592  df-br 5106  df-dm 5662

This theorem is referenced by:  dmeq  5884  dmv  5903  rnss  5920  dmiin  5934  dmresss  6001  ssxpb  6164  sofld  6177  resssxp  6261  relrelss  6264  funssxp  6724  fndmdif  7027  fneqeql2  7032  dff3  7085  frxp  8110  fnwelem  8115  frxp2  8128  frxp3  8135  funsssuppss  8174  tposss  8211  frrlem8  8278  frrlem14  8284  smores  8327  smores2  8329  tfrlem13  8365  imafi  9263  hartogslem1  9492  wemapso  9501  dmttrcl  9678  r0weon  9984  infxpenlem  9985  brdom3  10500  brdom5  10501  brdom4  10502  fpwwe2lem12  10615  fpwwe2  10616  canth4  10620  canthwelem  10623  pwfseqlem4  10635  nqerf  10903  dmrecnq  10941  uzrdgfni  13985  hashdmpropge2  14510  dmtrclfv  15045  rlimpm  15541  isstruct2  17199  strleun  17207  imasaddfnlem  17572  imasvscafn  17581  isohom  17823  catcoppccl  18164  tsrss  18635  ledm  18636  dirdm  18646  f1omvdmvd  19504  mvdco  19506  f1omvdconj  19507  pmtrfb  19526  pmtrfconj  19527  symggen  19531  symggen2  19532  pmtrdifellem1  19537  pmtrdifellem2  19538  psgnunilem1  19554  gsum2d  20033  lspextmo  21146  dsmmfi  21848  lindfres  21933  mdetdiaglem  22716  tsmsxp  24273  ustssco  24333  setsmstopn  24596  metustexhalf  24674  tngtopn  24768  equivcau  25420  metsscmetcld  25435  dvbssntr  26020  pserdv  26550  noseqrdgfn  28457  subgreldmiedg  29542  hlimcaui  31497  nfpconfp  32889  gsumfs2d  33294  symgcom2  33317  pmtrcnel  33322  pmtrcnel2  33323  pmtrcnelor  33324  cycpmrn  33376  metideq  34200  esum2d  34400  subgrwlk  35495  fundmpss  36130  fixssdm  36267  filnetlem3  36753  filnetlem4  36754  ssbnd  38299  bnd2lem  38302  ismrcd1  43291  istopclsd  43293  mptrcllem  44201  cnvrcl0  44213  dmtrcl  44215  dfrcl2  44262  relexpss1d  44293  rfovcnvf1od  44592  fourierdlem80  46758  issmflem  47299