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

Theorem dmss 5071
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 3344 . . . 4  |-  ( A 
C_  B  ->  ( <. x ,  y >.  e.  A  ->  <. x ,  y >.  e.  B
) )
21eximdv 1633 . . 3  |-  ( A 
C_  B  ->  ( E. y <. x ,  y
>.  e.  A  ->  E. y <. x ,  y >.  e.  B ) )
3 vex 2961 . . . 4  |-  x  e. 
_V
43eldm2 5070 . . 3  |-  ( x  e.  dom  A  <->  E. y <. x ,  y >.  e.  A )
53eldm2 5070 . . 3  |-  ( x  e.  dom  B  <->  E. y <. x ,  y >.  e.  B )
62, 4, 53imtr4g 263 . 2  |-  ( A 
C_  B  ->  (
x  e.  dom  A  ->  x  e.  dom  B
) )
76ssrdv 3356 1  |-  ( A 
C_  B  ->  dom  A 
C_  dom  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4   E.wex 1551    e. wcel 1726    C_ wss 3322   <.cop 3819   dom cdm 4880
This theorem is referenced by:  dmeq  5072  dmv  5087  rnss  5100  dmiin  5115  ssxpb  5305  sofld  5320  relrelss  5395  funssxp  5606  fndmdif  5836  fneqeql2  5841  dff3  5884  frxp  6458  fnwelem  6463  tposss  6482  smores  6616  smores2  6618  tfrlem13  6653  imafi  7401  hartogslem1  7513  wemapso  7522  r0weon  7896  infxpenlem  7897  brdom3  8408  brdom5  8409  brdom4  8410  fpwwe2lem13  8519  fpwwe2  8520  canth4  8524  canthwelem  8527  pwfseqlem4  8539  nqerf  8809  dmrecnq  8847  uzrdgfni  11300  rlimpm  12296  isstruct2  13480  strlemor1  13558  strleun  13561  imasaddfnlem  13755  imasvscafn  13764  isohom  13999  catcoppccl  14265  tsrss  14657  ledm  14671  dirdm  14681  gsum2d  15548  lspextmo  16134  tsmsxp  18186  ustssco  18246  setsmstopn  18510  metustexhalfOLD  18595  metustexhalf  18596  tngtopn  18693  equivcau  19255  cmetss  19269  dvbssntr  19789  pserdv  20347  uhgrares  21345  umgrares  21361  usgrares  21391  hlimcaui  22741  metideq  24290  fundmpss  25392  wfrlem16  25555  fixssdm  25753  filnetlem3  26411  filnetlem4  26412  ssbnd  26499  bnd2lem  26502  ismrcd1  26754  istopclsd  26756  dsmmfi  27183  lindfres  27272  f1omvdmvd  27365  mvdco  27367  f1omvdconj  27368  pmtrfb  27385  pmtrfconj  27386  symggen  27390  symggen2  27391  psgnunilem1  27395  psgnghm2  27417
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-rab 2716  df-v 2960  df-dif 3325  df-un 3327  df-in 3329  df-ss 3336  df-nul 3631  df-if 3742  df-sn 3822  df-pr 3823  df-op 3825  df-br 4215  df-dm 4890
  Copyright terms: Public domain W3C validator