Theorem dmss 5049

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 3458	. . . 4 |- ( A C_ B -> ( <. x , y >. e. A -> <. x , y >. e. B ) )
2	1	eximdv 1754	. . 3 |- ( A C_ B -> ( E. y <. x , y >. e. A -> E. y <. x , y >. e. B ) )
3		vex 3084	. . . 4 |- x e. _V
4	3	eldm2 5048	. . 3 |- ( x e. dom A <-> E. y <. x , y >. e. A )
5	3	eldm2 5048	. . 3 |- ( x e. dom B <-> E. y <. x , y >. e. B )
6	2, 4, 5	3imtr4g 273	. 2 |- ( A C_ B -> ( x e. dom A -> x e. dom B ) )
7	6	ssrdv 3470	1 |- ( A C_ B -> dom A C_ dom B )

Syntax hints:   -> wi 4   E.wex 1659   e. wcel 1868   C_ wss 3436   <.cop 4002   dom cdm 4849

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-rab 2784  df-v 3083  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3910  df-sn 3997  df-pr 3999  df-op 4003  df-br 4421  df-dm 4859

This theorem is referenced by:  dmeq  5050  dmv  5065  rnss  5078  dmiin  5093  ssxpb  5286  sofld  5299  relrelss  5374  funssxp  5755  fndmdif  5997  fneqeql2  6002  dff3  6046  frxp  6913  fnwelem  6918  funsssuppss  6948  tposss  6978  wfrlem16  7055  smores  7075  smores2  7077  tfrlem13  7112  imafi  7869  hartogslem1  8059  wemapso  8068  r0weon  8444  infxpenlem  8445  brdom3  8956  brdom5  8957  brdom4  8958  fpwwe2lem13  9067  fpwwe2  9068  canth4  9072  canthwelem  9075  pwfseqlem4  9087  nqerf  9355  dmrecnq  9393  uzrdgfni  12171  dmtrclfv  13070  rlimpm  13551  isstruct2  15117  strlemor1  15204  strleun  15207  imasaddfnlem  15421  imasvscafn  15430  isohom  15668  catcoppccl  15990  tsrss  16456  ledm  16457  dirdm  16467  f1omvdmvd  17071  mvdco  17073  f1omvdconj  17074  pmtrfb  17093  pmtrfconj  17094  symggen  17098  symggen2  17099  pmtrdifellem1  17104  pmtrdifellem2  17105  psgnunilem1  17121  gsum2d  17591  lspextmo  18266  dsmmfi  19287  lindfres  19367  mdetdiaglem  19609  tsmsxp  21155  ustssco  21215  setsmstopn  21479  metustexhalf  21557  tngtopn  21644  equivcau  22256  cmetss  22270  dvbssntr  22841  pserdv  23370  uhgrares  25021  umgrares  25037  usgrares  25082  hlimcaui  26874  metideq  28691  esum2d  28909  fundmpss  30401  fixssdm  30665  filnetlem3  31028  filnetlem4  31029  ssbnd  32033  bnd2lem  32036  ismrcd1  35458  istopclsd  35460  dfrcl2  36125  relexpss1d  36156  rp-imass  36223  fourierdlem80  37869  struct1vtxvallem  38788  uhgrreslem  38828  usgrres  38894  uhgres  38962