MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dmss Structured version   Visualization version   GIF version

Theorem dmss 5808
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.
StepHypRef Expression
1 ssel 3918 . . . 4 (𝐴𝐵 → (⟨𝑥, 𝑦⟩ ∈ 𝐴 → ⟨𝑥, 𝑦⟩ ∈ 𝐵))
21eximdv 1923 . . 3 (𝐴𝐵 → (∃𝑦𝑥, 𝑦⟩ ∈ 𝐴 → ∃𝑦𝑥, 𝑦⟩ ∈ 𝐵))
3 vex 3434 . . . 4 𝑥 ∈ V
43eldm2 5807 . . 3 (𝑥 ∈ dom 𝐴 ↔ ∃𝑦𝑥, 𝑦⟩ ∈ 𝐴)
53eldm2 5807 . . 3 (𝑥 ∈ dom 𝐵 ↔ ∃𝑦𝑥, 𝑦⟩ ∈ 𝐵)
62, 4, 53imtr4g 295 . 2 (𝐴𝐵 → (𝑥 ∈ dom 𝐴𝑥 ∈ dom 𝐵))
76ssrdv 3931 1 (𝐴𝐵 → dom 𝐴 ⊆ dom 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wex 1785  wcel 2109  wss 3891  cop 4572  dom cdm 5588
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-ext 2710
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1544  df-fal 1554  df-ex 1786  df-sb 2071  df-clab 2717  df-cleq 2731  df-clel 2817  df-rab 3074  df-v 3432  df-dif 3894  df-un 3896  df-in 3898  df-ss 3908  df-nul 4262  df-if 4465  df-sn 4567  df-pr 4569  df-op 4573  df-br 5079  df-dm 5598
This theorem is referenced by:  dmeq  5809  dmv  5828  rnss  5845  dmiin  5859  ssxpb  6074  sofld  6087  resssxp  6170  relrelss  6173  funssxp  6625  fndmdif  6913  fneqeql2  6918  dff3  6970  frxp  7951  fnwelem  7956  funsssuppss  7990  tposss  8027  frrlem8  8093  frrlem14  8099  wfrlem16OLD  8139  smores  8167  smores2  8169  tfrlem13  8205  imafiALT  9073  hartogslem1  9262  wemapso  9271  dmttrcl  9440  r0weon  9752  infxpenlem  9753  brdom3  10268  brdom5  10269  brdom4  10270  fpwwe2lem12  10382  fpwwe2  10383  canth4  10387  canthwelem  10390  pwfseqlem4  10402  nqerf  10670  dmrecnq  10708  uzrdgfni  13659  hashdmpropge2  14178  dmtrclfv  14710  rlimpm  15190  isstruct2  16831  strleun  16839  imasaddfnlem  17220  imasvscafn  17229  isohom  17469  catcoppccl  17813  catcoppcclOLD  17814  tsrss  18288  ledm  18289  dirdm  18299  f1omvdmvd  19032  mvdco  19034  f1omvdconj  19035  pmtrfb  19054  pmtrfconj  19055  symggen  19059  symggen2  19060  pmtrdifellem1  19065  pmtrdifellem2  19066  psgnunilem1  19082  gsum2d  19554  lspextmo  20299  dsmmfi  20926  lindfres  21011  mdetdiaglem  21728  tsmsxp  23287  ustssco  23347  setsmstopn  23614  metustexhalf  23693  tngtopn  23795  equivcau  24445  metsscmetcld  24460  dvbssntr  25045  pserdv  25569  subgreldmiedg  27631  hlimcaui  29577  nfpconfp  30946  symgcom2  31332  pmtrcnel  31337  pmtrcnel2  31338  pmtrcnelor  31339  cycpmrn  31389  metideq  31822  esum2d  32040  subgrwlk  33073  fundmpss  33719  frxp2  33770  frxp3  33776  fixssdm  34187  filnetlem3  34548  filnetlem4  34549  ssbnd  35925  bnd2lem  35928  ismrcd1  40500  istopclsd  40502  mptrcllem  41174  cnvrcl0  41186  dmtrcl  41188  dfrcl2  41235  relexpss1d  41266  rfovcnvf1od  41565  fourierdlem80  43681  issmflem  44214
  Copyright terms: Public domain W3C validator