Theorem dmss 5033

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 3425	. . . 4 |- ( A C_ B -> ( <. x , y >. e. A -> <. x , y >. e. B ) )
2	1	eximdv 1763	. . 3 |- ( A C_ B -> ( E. y <. x , y >. e. A -> E. y <. x , y >. e. B ) )
3		vex 3047	. . . 4 |- x e. _V
4	3	eldm2 5032	. . 3 |- ( x e. dom A <-> E. y <. x , y >. e. A )
5	3	eldm2 5032	. . 3 |- ( x e. dom B <-> E. y <. x , y >. e. B )
6	2, 4, 5	3imtr4g 274	. 2 |- ( A C_ B -> ( x e. dom A -> x e. dom B ) )
7	6	ssrdv 3437	1 |- ( A C_ B -> dom A C_ dom B )

Syntax hints:   -> wi 4   E.wex 1662   e. wcel 1886   C_ wss 3403   <.cop 3973   dom cdm 4833

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757  ax-6 1804  ax-7 1850  ax-10 1914  ax-11 1919  ax-12 1932  ax-13 2090  ax-ext 2430

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 986  df-tru 1446  df-ex 1663  df-nf 1667  df-sb 1797  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2580  df-rab 2745  df-v 3046  df-dif 3406  df-un 3408  df-in 3410  df-ss 3417  df-nul 3731  df-if 3881  df-sn 3968  df-pr 3970  df-op 3974  df-br 4402  df-dm 4843

This theorem is referenced by:  dmeq  5034  dmv  5049  rnss  5062  dmiin  5077  ssxpb  5270  sofld  5283  relrelss  5358  funssxp  5740  fndmdif  5984  fneqeql2  5989  dff3  6033  frxp  6903  fnwelem  6908  funsssuppss  6938  tposss  6971  wfrlem16  7048  smores  7068  smores2  7070  tfrlem13  7105  imafi  7864  hartogslem1  8054  wemapso  8063  r0weon  8440  infxpenlem  8441  brdom3  8953  brdom5  8954  brdom4  8955  fpwwe2lem13  9064  fpwwe2  9065  canth4  9069  canthwelem  9072  pwfseqlem4  9084  nqerf  9352  dmrecnq  9390  uzrdgfni  12169  dmtrclfv  13075  rlimpm  13557  isstruct2  15123  strlemor1  15210  strleun  15213  imasaddfnlem  15427  imasvscafn  15436  isohom  15674  catcoppccl  15996  tsrss  16462  ledm  16463  dirdm  16473  f1omvdmvd  17077  mvdco  17079  f1omvdconj  17080  pmtrfb  17099  pmtrfconj  17100  symggen  17104  symggen2  17105  pmtrdifellem1  17110  pmtrdifellem2  17111  psgnunilem1  17127  gsum2d  17597  lspextmo  18272  dsmmfi  19294  lindfres  19374  mdetdiaglem  19616  tsmsxp  21162  ustssco  21222  setsmstopn  21486  metustexhalf  21564  tngtopn  21651  equivcau  22263  cmetss  22277  dvbssntr  22848  pserdv  23377  uhgrares  25028  umgrares  25044  usgrares  25089  hlimcaui  26882  metideq  28689  esum2d  28907  fundmpss  30400  fixssdm  30666  filnetlem3  31029  filnetlem4  31030  ssbnd  32113  bnd2lem  32116  ismrcd1  35534  istopclsd  35536  mptrcllem  36214  cnvrcl0  36226  dmtrcl  36228  dfrcl2  36260  relexpss1d  36291  rp-imass  36360  fourierdlem80  38044  structgrssvtxlem  39111  subgreldmiedg  39338  uhgres  39678