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

Theorem dmss 4894
Description: Subset theorem for domain. (Contributed by NM, 11-Aug-1994.)
Assertion
Ref Expression
dmss  |-  ( A 
C_  B  ->  dom  A 
C_  dom  B )

Proof of Theorem dmss
Dummy variables  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ssel 3187 . . . 4  |-  ( A 
C_  B  ->  ( <. x ,  y >.  e.  A  ->  <. x ,  y >.  e.  B
) )
21eximdv 1612 . . 3  |-  ( A 
C_  B  ->  ( E. y <. x ,  y
>.  e.  A  ->  E. y <. x ,  y >.  e.  B ) )
3 vex 2804 . . . 4  |-  x  e. 
_V
43eldm2 4893 . . 3  |-  ( x  e.  dom  A  <->  E. y <. x ,  y >.  e.  A )
53eldm2 4893 . . 3  |-  ( x  e.  dom  B  <->  E. y <. x ,  y >.  e.  B )
62, 4, 53imtr4g 261 . 2  |-  ( A 
C_  B  ->  (
x  e.  dom  A  ->  x  e.  dom  B
) )
76ssrdv 3198 1  |-  ( A 
C_  B  ->  dom  A 
C_  dom  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4   E.wex 1531    e. wcel 1696    C_ wss 3165   <.cop 3656   dom cdm 4705
This theorem is referenced by:  dmeq  4895  dmv  4910  rnss  4923  dmiin  4938  ssxpb  5126  sofld  5137  relrelss  5212  funssxp  5418  fndmdif  5645  fneqeql2  5650  dff3  5689  frxp  6241  fnwelem  6246  tposss  6251  smores  6385  smores2  6387  tfrlem13  6422  imafi  7164  hartogslem1  7273  wemapso  7282  r0weon  7656  infxpenlem  7657  brdom3  8169  brdom5  8170  brdom4  8171  fpwwe2lem13  8280  fpwwe2  8281  canth4  8285  canthwelem  8288  pwfseqlem4  8300  nqerf  8570  dmrecnq  8608  uzrdgfni  11037  rlimpm  11990  isstruct2  13173  strlemor1  13251  strleun  13254  imasaddfnlem  13446  imasvscafn  13455  isohom  13690  catcoppccl  13956  tsrss  14348  ledm  14362  dirdm  14372  gsum2d  15239  lspextmo  15829  tsmsxp  17853  setsmstopn  18040  tngtopn  18182  equivcau  18742  cmetss  18756  dvbssntr  19266  pserdv  19821  hlimcaui  21832  umgrares  23891  fundmpss  24193  wfrlem16  24342  fixssdm  24517  reldded  25844  dmrngcmp  25854  reldcat  25865  obsubc2  25953  morsubc  25958  filnetlem3  26432  filnetlem4  26433  ssbnd  26615  bnd2lem  26618  ismrcd1  26876  istopclsd  26878  dsmmfi  27307  lindfres  27396  f1omvdmvd  27489  mvdco  27491  f1omvdconj  27492  pmtrfb  27509  pmtrfconj  27510  symggen  27514  symggen2  27515  psgnunilem1  27519  psgnghm2  27541  usgrares  28249
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-rab 2565  df-v 2803  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-nul 3469  df-if 3579  df-sn 3659  df-pr 3660  df-op 3662  df-br 4040  df-dm 4715
  Copyright terms: Public domain W3C validator