Theorem dmss 5028

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 3302	. . . 4 |- ( A C_ B -> ( <. x , y >. e. A -> <. x , y >. e. B ) )
2	1	eximdv 1629	. . 3 |- ( A C_ B -> ( E. y <. x , y >. e. A -> E. y <. x , y >. e. B ) )
3		vex 2919	. . . 4 |- x e. _V
4	3	eldm2 5027	. . 3 |- ( x e. dom A <-> E. y <. x , y >. e. A )
5	3	eldm2 5027	. . 3 |- ( x e. dom B <-> E. y <. x , y >. e. B )
6	2, 4, 5	3imtr4g 262	. 2 |- ( A C_ B -> ( x e. dom A -> x e. dom B ) )
7	6	ssrdv 3314	1 |- ( A C_ B -> dom A C_ dom B )

Syntax hints:   -> wi 4   E.wex 1547   e. wcel 1721   C_ wss 3280   <.cop 3777   dom cdm 4837

This theorem is referenced by:  dmeq  5029  dmv  5044  rnss  5057  dmiin  5072  ssxpb  5262  sofld  5277  relrelss  5352  funssxp  5563  fndmdif  5793  fneqeql2  5798  dff3  5841  frxp  6415  fnwelem  6420  tposss  6439  smores  6573  smores2  6575  tfrlem13  6610  imafi  7357  hartogslem1  7467  wemapso  7476  r0weon  7850  infxpenlem  7851  brdom3  8362  brdom5  8363  brdom4  8364  fpwwe2lem13  8473  fpwwe2  8474  canth4  8478  canthwelem  8481  pwfseqlem4  8493  nqerf  8763  dmrecnq  8801  uzrdgfni  11253  rlimpm  12249  isstruct2  13433  strlemor1  13511  strleun  13514  imasaddfnlem  13708  imasvscafn  13717  isohom  13952  catcoppccl  14218  tsrss  14610  ledm  14624  dirdm  14634  gsum2d  15501  lspextmo  16087  tsmsxp  18137  ustssco  18197  setsmstopn  18461  metustexhalfOLD  18546  metustexhalf  18547  tngtopn  18644  equivcau  19206  cmetss  19220  dvbssntr  19740  pserdv  20298  uhgrares  21296  umgrares  21312  usgrares  21342  hlimcaui  22692  metideq  24241  fundmpss  25336  wfrlem16  25485  fixssdm  25660  filnetlem3  26299  filnetlem4  26300  ssbnd  26387  bnd2lem  26390  ismrcd1  26642  istopclsd  26644  dsmmfi  27072  lindfres  27161  f1omvdmvd  27254  mvdco  27256  f1omvdconj  27257  pmtrfb  27274  pmtrfconj  27275  symggen  27279  symggen2  27280  psgnunilem1  27284  psgnghm2  27306

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385

This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-rab 2675  df-v 2918  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-sn 3780  df-pr 3781  df-op 3783  df-br 4173  df-dm 4847