Theorem dmss 5039

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 3412	. . . 4 |- ( A C_ B -> ( <. x , y >. e. A -> <. x , y >. e. B ) )
2	1	eximdv 1772	. . 3 |- ( A C_ B -> ( E. y <. x , y >. e. A -> E. y <. x , y >. e. B ) )
3		vex 3034	. . . 4 |- x e. _V
4	3	eldm2 5038	. . 3 |- ( x e. dom A <-> E. y <. x , y >. e. A )
5	3	eldm2 5038	. . 3 |- ( x e. dom B <-> E. y <. x , y >. e. B )
6	2, 4, 5	3imtr4g 278	. 2 |- ( A C_ B -> ( x e. dom A -> x e. dom B ) )
7	6	ssrdv 3424	1 |- ( A C_ B -> dom A C_ dom B )

Syntax hints:   -> wi 4   E.wex 1671   e. wcel 1904   C_ wss 3390   <.cop 3965   dom cdm 4839

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451

This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3an 1009  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-rab 2765  df-v 3033  df-dif 3393  df-un 3395  df-in 3397  df-ss 3404  df-nul 3723  df-if 3873  df-sn 3960  df-pr 3962  df-op 3966  df-br 4396  df-dm 4849

This theorem is referenced by:  dmeq  5040  dmv  5056  rnss  5069  dmiin  5084  ssxpb  5277  sofld  5290  relrelss  5366  funssxp  5754  fndmdif  6001  fneqeql2  6006  dff3  6050  frxp  6925  fnwelem  6930  funsssuppss  6960  tposss  6992  wfrlem16  7069  smores  7089  smores2  7091  tfrlem13  7126  imafi  7885  hartogslem1  8075  wemapso  8084  r0weon  8461  infxpenlem  8462  brdom3  8974  brdom5  8975  brdom4  8976  fpwwe2lem13  9085  fpwwe2  9086  canth4  9090  canthwelem  9093  pwfseqlem4  9105  nqerf  9373  dmrecnq  9411  uzrdgfni  12210  dmtrclfv  13159  rlimpm  13641  isstruct2  15208  strlemor1  15295  strleun  15298  imasaddfnlem  15512  imasvscafn  15521  isohom  15759  catcoppccl  16081  tsrss  16547  ledm  16548  dirdm  16558  f1omvdmvd  17162  mvdco  17164  f1omvdconj  17165  pmtrfb  17184  pmtrfconj  17185  symggen  17189  symggen2  17190  pmtrdifellem1  17195  pmtrdifellem2  17196  psgnunilem1  17212  gsum2d  17682  lspextmo  18357  dsmmfi  19378  lindfres  19458  mdetdiaglem  19700  tsmsxp  21247  ustssco  21307  setsmstopn  21571  metustexhalf  21649  tngtopn  21736  equivcau  22348  cmetss  22362  dvbssntr  22934  pserdv  23463  uhgrares  25114  umgrares  25130  usgrares  25175  hlimcaui  26970  metideq  28770  esum2d  28988  fundmpss  30478  fixssdm  30744  filnetlem3  31107  filnetlem4  31108  ssbnd  32184  bnd2lem  32187  ismrcd1  35611  istopclsd  35613  mptrcllem  36291  cnvrcl0  36303  dmtrcl  36305  dfrcl2  36337  relexpss1d  36368  rp-imass  36437  fourierdlem80  38162  structgrssvtxlem  39278  subgreldmiedg  39519  uhgres  40199