Theorem dmss 5026

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.

Step	Hyp	Ref	Expression
1		ssel 3338	. . . 4 |- ( A C_ B -> ( <. x , y >. e. A -> <. x , y >. e. B ) )
2	1	eximdv 1675	. . 3 |- ( A C_ B -> ( E. y <. x , y >. e. A -> E. y <. x , y >. e. B ) )
3		vex 2965	. . . 4 |- x e. _V
4	3	eldm2 5025	. . 3 |- ( x e. dom A <-> E. y <. x , y >. e. A )
5	3	eldm2 5025	. . 3 |- ( x e. dom B <-> E. y <. x , y >. e. B )
6	2, 4, 5	3imtr4g 270	. 2 |- ( A C_ B -> ( x e. dom A -> x e. dom B ) )
7	6	ssrdv 3350	1 |- ( A C_ B -> dom A C_ dom B )

Syntax hints:   -> wi 4   E.wex 1589   e. wcel 1755   C_ wss 3316   <.cop 3871   dom cdm 4827

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-rab 2714  df-v 2964  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-nul 3626  df-if 3780  df-sn 3866  df-pr 3868  df-op 3872  df-br 4281  df-dm 4837

This theorem is referenced by:  dmeq  5027  dmv  5042  rnss  5055  dmiin  5070  ssxpb  5260  sofld  5274  relrelss  5349  funssxp  5559  fndmdif  5795  fneqeql2  5800  dff3  5844  frxp  6671  fnwelem  6676  funsssuppss  6704  tposss  6735  smores  6799  smores2  6801  tfrlem13  6835  imafi  7592  hartogslem1  7744  wemapso  7753  r0weon  8167  infxpenlem  8168  brdom3  8683  brdom5  8684  brdom4  8685  fpwwe2lem13  8797  fpwwe2  8798  canth4  8802  canthwelem  8805  pwfseqlem4  8817  nqerf  9087  dmrecnq  9125  uzrdgfni  11765  rlimpm  12962  isstruct2  14166  strlemor1  14248  strleun  14251  imasaddfnlem  14449  imasvscafn  14458  isohom  14693  catcoppccl  14959  tsrss  15376  ledm  15377  dirdm  15387  f1omvdmvd  15929  mvdco  15931  f1omvdconj  15932  pmtrfb  15951  pmtrfconj  15952  symggen  15956  symggen2  15957  pmtrdifellem1  15962  pmtrdifellem2  15963  psgnunilem1  15979  gsum2d  16437  gsum2dOLD  16438  lspextmo  17059  psgnghm2  17853  dsmmfi  18005  lindfres  18094  mdet1  18250  tsmsxp  19571  ustssco  19631  setsmstopn  19895  metustexhalfOLD  19980  metustexhalf  19981  tngtopn  20078  equivcau  20653  cmetss  20667  dvbssntr  21217  pserdv  21779  uhgrares  23065  umgrares  23081  usgrares  23111  hlimcaui  24462  metideq  26174  fundmpss  27424  wfrlem16  27586  fixssdm  27784  filnetlem3  28445  filnetlem4  28446  ssbnd  28531  bnd2lem  28534  ismrcd1  28879  istopclsd  28881