Theorem dmss 5894

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 3932	. . . 4 ⊢ (𝐴 ⊆ 𝐵 → (⟨𝑥, 𝑦⟩ ∈ 𝐴 → ⟨𝑥, 𝑦⟩ ∈ 𝐵))
2	1	eximdv 1947	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐴 → ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐵))
3		vex 3459	. . . 4 ⊢ 𝑥 ∈ V
4	3	eldm2 5893	. . 3 ⊢ (𝑥 ∈ dom 𝐴 ↔ ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐴)
5	3	eldm2 5893	. . 3 ⊢ (𝑥 ∈ dom 𝐵 ↔ ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐵)
6	2, 4, 5	3imtr4g 299	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ dom 𝐴 → 𝑥 ∈ dom 𝐵))
7	6	ssrdv 3944	1 ⊢ (𝐴 ⊆ 𝐵 → dom 𝐴 ⊆ dom 𝐵)

Syntax hints:   → wi 4  ∃wex 1809   ∈ wcel 2143   ⊆ wss 3906  ⟨cop 4596  dom cdm 5663

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4288  df-if 4489  df-sn 4591  df-pr 4593  df-op 4597  df-br 5111  df-dm 5673

This theorem is referenced by:  dmeq  5895  dmv  5914  rnss  5931  dmiin  5945  dmresss  6012  ssxpb  6174  sofld  6187  resssxp  6273  relrelss  6276  funssxp  6736  fndmdif  7039  fneqeql2  7044  dff3  7097  frxp  8123  fnwelem  8128  frxp2  8141  frxp3  8148  funsssuppss  8187  tposss  8224  frrlem8  8291  frrlem14  8297  smores  8340  smores2  8342  tfrlem13  8378  imafi  9276  hartogslem1  9505  wemapso  9514  dmttrcl  9691  r0weon  9997  infxpenlem  9998  brdom3  10513  brdom5  10514  brdom4  10515  fpwwe2lem12  10628  fpwwe2  10629  canth4  10633  canthwelem  10636  pwfseqlem4  10648  nqerf  10916  dmrecnq  10954  uzrdgfni  13996  hashdmpropge2  14522  dmtrclfv  15057  rlimpm  15553  isstruct2  17210  strleun  17218  imasaddfnlem  17583  imasvscafn  17592  isohom  17834  catcoppccl  18175  tsrss  18646  ledm  18647  dirdm  18657  f1omvdmvd  19514  mvdco  19516  f1omvdconj  19517  pmtrfb  19536  pmtrfconj  19537  symggen  19541  symggen2  19542  pmtrdifellem1  19547  pmtrdifellem2  19548  psgnunilem1  19564  gsum2d  20043  lspextmo  21158  dsmmfi  21869  lindfres  21954  mdetdiaglem  22736  tsmsxp  24293  ustssco  24353  setsmstopn  24616  metustexhalf  24694  tngtopn  24788  equivcau  25440  metsscmetcld  25455  dvbssntr  26040  pserdv  26573  noseqrdgfn  28480  subgreldmiedg  29614  hlimcaui  31569  nfpconfp  32958  gsumfs2d  33362  symgcom2  33385  pmtrcnel  33390  pmtrcnel2  33391  pmtrcnelor  33392  cycpmrn  33444  metideq  34264  esum2d  34464  subgrwlk  35605  fundmpss  36240  fixssdm  36377  filnetlem3  36872  filnetlem4  36873  ssbnd  38420  bnd2lem  38423  ismrcd1  43412  istopclsd  43414  mptrcllem  44322  cnvrcl0  44334  dmtrcl  44336  dfrcl2  44383  relexpss1d  44414  rfovcnvf1od  44713  fourierdlem80  46883  issmflem  47424