Theorem dmss 5857

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 3915	. . . 4 ⊢ (𝐴 ⊆ 𝐵 → (⟨𝑥, 𝑦⟩ ∈ 𝐴 → ⟨𝑥, 𝑦⟩ ∈ 𝐵))
2	1	eximdv 1919	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐴 → ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐵))
3		vex 3433	. . . 4 ⊢ 𝑥 ∈ V
4	3	eldm2 5856	. . 3 ⊢ (𝑥 ∈ dom 𝐴 ↔ ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐴)
5	3	eldm2 5856	. . 3 ⊢ (𝑥 ∈ dom 𝐵 ↔ ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐵)
6	2, 4, 5	3imtr4g 296	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ dom 𝐴 → 𝑥 ∈ dom 𝐵))
7	6	ssrdv 3927	1 ⊢ (𝐴 ⊆ 𝐵 → dom 𝐴 ⊆ dom 𝐵)

Syntax hints:   → wi 4  ∃wex 1781   ∈ wcel 2114   ⊆ wss 3889  ⟨cop 4573  dom cdm 5631

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 2708

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 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-br 5086  df-dm 5641

This theorem is referenced by:  dmeq  5858  dmv  5877  rnss  5894  dmiin  5908  dmresss  5976  ssxpb  6138  sofld  6151  resssxp  6234  relrelss  6237  funssxp  6696  fndmdif  6994  fneqeql2  6999  dff3  7052  frxp  8076  fnwelem  8081  frxp2  8094  frxp3  8101  funsssuppss  8140  tposss  8177  frrlem8  8243  frrlem14  8249  smores  8292  smores2  8294  tfrlem13  8329  imafi  9225  hartogslem1  9457  wemapso  9466  dmttrcl  9642  r0weon  9934  infxpenlem  9935  brdom3  10450  brdom5  10451  brdom4  10452  fpwwe2lem12  10565  fpwwe2  10566  canth4  10570  canthwelem  10573  pwfseqlem4  10585  nqerf  10853  dmrecnq  10891  uzrdgfni  13920  hashdmpropge2  14445  dmtrclfv  14980  rlimpm  15462  isstruct2  17119  strleun  17127  imasaddfnlem  17492  imasvscafn  17501  isohom  17743  catcoppccl  18084  tsrss  18555  ledm  18556  dirdm  18566  f1omvdmvd  19418  mvdco  19420  f1omvdconj  19421  pmtrfb  19440  pmtrfconj  19441  symggen  19445  symggen2  19446  pmtrdifellem1  19451  pmtrdifellem2  19452  psgnunilem1  19468  gsum2d  19947  lspextmo  21051  dsmmfi  21718  lindfres  21803  mdetdiaglem  22563  tsmsxp  24120  ustssco  24180  setsmstopn  24443  metustexhalf  24521  tngtopn  24615  equivcau  25267  metsscmetcld  25282  dvbssntr  25867  pserdv  26394  noseqrdgfn  28298  subgreldmiedg  29352  hlimcaui  31307  nfpconfp  32705  gsumfs2d  33122  symgcom2  33145  pmtrcnel  33150  pmtrcnel2  33151  pmtrcnelor  33152  cycpmrn  33204  metideq  34037  esum2d  34237  subgrwlk  35314  fundmpss  35949  fixssdm  36086  filnetlem3  36562  filnetlem4  36563  ssbnd  38109  bnd2lem  38112  ismrcd1  43130  istopclsd  43132  mptrcllem  44040  cnvrcl0  44052  dmtrcl  44054  dfrcl2  44101  relexpss1d  44132  rfovcnvf1od  44431  fourierdlem80  46614  issmflem  47155