Theorem dmss 5034

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 3345	. . . 4 |- ( A C_ B -> ( <. x , y >. e. A -> <. x , y >. e. B ) )
2	1	eximdv 1676	. . 3 |- ( A C_ B -> ( E. y <. x , y >. e. A -> E. y <. x , y >. e. B ) )
3		vex 2970	. . . 4 |- x e. _V
4	3	eldm2 5033	. . 3 |- ( x e. dom A <-> E. y <. x , y >. e. A )
5	3	eldm2 5033	. . 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 3357	1 |- ( A C_ B -> dom A C_ dom B )

Syntax hints:   -> wi 4   E.wex 1586   e. wcel 1756   C_ wss 3323   <.cop 3878   dom cdm 4835

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-rab 2719  df-v 2969  df-dif 3326  df-un 3328  df-in 3330  df-ss 3337  df-nul 3633  df-if 3787  df-sn 3873  df-pr 3875  df-op 3879  df-br 4288  df-dm 4845

This theorem is referenced by:  dmeq  5035  dmv  5050  rnss  5063  dmiin  5078  ssxpb  5267  sofld  5281  relrelss  5356  funssxp  5566  fndmdif  5802  fneqeql2  5807  dff3  5851  frxp  6677  fnwelem  6682  funsssuppss  6710  tposss  6741  smores  6805  smores2  6807  tfrlem13  6841  imafi  7596  hartogslem1  7748  wemapso  7757  r0weon  8171  infxpenlem  8172  brdom3  8687  brdom5  8688  brdom4  8689  fpwwe2lem13  8801  fpwwe2  8802  canth4  8806  canthwelem  8809  pwfseqlem4  8821  nqerf  9091  dmrecnq  9129  uzrdgfni  11773  rlimpm  12970  isstruct2  14175  strlemor1  14257  strleun  14260  imasaddfnlem  14458  imasvscafn  14467  isohom  14702  catcoppccl  14968  tsrss  15385  ledm  15386  dirdm  15396  f1omvdmvd  15940  mvdco  15942  f1omvdconj  15943  pmtrfb  15962  pmtrfconj  15963  symggen  15967  symggen2  15968  pmtrdifellem1  15973  pmtrdifellem2  15974  psgnunilem1  15990  gsum2d  16451  gsum2dOLD  16452  lspextmo  17114  psgnghm2  17986  dsmmfi  18138  lindfres  18227  mdet1  18383  tsmsxp  19704  ustssco  19764  setsmstopn  20028  metustexhalfOLD  20113  metustexhalf  20114  tngtopn  20211  equivcau  20786  cmetss  20800  dvbssntr  21350  pserdv  21869  uhgrares  23193  umgrares  23209  usgrares  23239  hlimcaui  24590  metideq  26272  fundmpss  27528  wfrlem16  27690  fixssdm  27888  filnetlem3  28554  filnetlem4  28555  ssbnd  28640  bnd2lem  28643  ismrcd1  28987  istopclsd  28989  mdetdiaglem  30824