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

Theorem dmss 4878
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 3174 . . . 4  |-  ( A 
C_  B  ->  ( <. x ,  y >.  e.  A  ->  <. x ,  y >.  e.  B
) )
21eximdv 1608 . . 3  |-  ( A 
C_  B  ->  ( E. y <. x ,  y
>.  e.  A  ->  E. y <. x ,  y >.  e.  B ) )
3 vex 2791 . . . 4  |-  x  e. 
_V
43eldm2 4877 . . 3  |-  ( x  e.  dom  A  <->  E. y <. x ,  y >.  e.  A )
53eldm2 4877 . . 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 3185 1  |-  ( A 
C_  B  ->  dom  A 
C_  dom  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4   E.wex 1528    e. wcel 1684    C_ wss 3152   <.cop 3643   dom cdm 4689
This theorem is referenced by:  dmeq  4879  dmv  4894  rnss  4907  dmiin  4922  ssxpb  5110  sofld  5121  relrelss  5196  funssxp  5402  fndmdif  5629  fneqeql2  5634  dff3  5673  frxp  6225  fnwelem  6230  tposss  6235  smores  6369  smores2  6371  tfrlem13  6406  imafi  7148  hartogslem1  7257  wemapso  7266  r0weon  7640  infxpenlem  7641  brdom3  8153  brdom5  8154  brdom4  8155  fpwwe2lem13  8264  fpwwe2  8265  canth4  8269  canthwelem  8272  pwfseqlem4  8284  nqerf  8554  dmrecnq  8592  uzrdgfni  11021  rlimpm  11974  isstruct2  13157  strlemor1  13235  strleun  13238  imasaddfnlem  13430  imasvscafn  13439  isohom  13674  catcoppccl  13940  tsrss  14332  ledm  14346  dirdm  14356  gsum2d  15223  lspextmo  15813  tsmsxp  17837  setsmstopn  18024  tngtopn  18166  equivcau  18726  cmetss  18740  dvbssntr  19250  pserdv  19805  hlimcaui  21816  umgrares  23876  fundmpss  24122  wfrlem16  24271  fixssdm  24446  reldded  25741  dmrngcmp  25751  reldcat  25762  obsubc2  25850  morsubc  25855  filnetlem3  26329  filnetlem4  26330  ssbnd  26512  bnd2lem  26515  ismrcd1  26773  istopclsd  26775  dsmmfi  27204  lindfres  27293  f1omvdmvd  27386  mvdco  27388  f1omvdconj  27389  pmtrfb  27406  pmtrfconj  27407  symggen  27411  symggen2  27412  psgnunilem1  27416  psgnghm2  27438  usgrares  28115
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-rab 2552  df-v 2790  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-br 4024  df-dm 4699
  Copyright terms: Public domain W3C validator