Theorem dmss 5323

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 3597	. . . 4 |- ( A C_ B -> ( <. x , y >. e. A -> <. x , y >. e. B ) )
2	1	eximdv 1846	. . 3 |- ( A C_ B -> ( E. y <. x , y >. e. A -> E. y <. x , y >. e. B ) )
3		vex 3203	. . . 4 |- x e. _V
4	3	eldm2 5322	. . 3 |- ( x e. dom A <-> E. y <. x , y >. e. A )
5	3	eldm2 5322	. . 3 |- ( x e. dom B <-> E. y <. x , y >. e. B )
6	2, 4, 5	3imtr4g 285	. 2 |- ( A C_ B -> ( x e. dom A -> x e. dom B ) )
7	6	ssrdv 3609	1 |- ( A C_ B -> dom A C_ dom B )

Syntax hints:   -> wi 4   E.wex 1704   e. wcel 1990   C_ wss 3574   <.cop 4183   dom cdm 5114

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-br 4654  df-dm 5124

This theorem is referenced by:  dmeq  5324  dmv  5341  rnss  5354  dmiin  5369  ssxpb  5568  sofld  5581  relrelss  5659  funssxp  6061  fndmdif  6321  fneqeql2  6326  dff3  6372  frxp  7287  fnwelem  7292  funsssuppss  7321  tposss  7353  wfrlem16  7430  smores  7449  smores2  7451  tfrlem13  7486  imafi  8259  hartogslem1  8447  wemapso  8456  r0weon  8835  infxpenlem  8836  brdom3  9350  brdom5  9351  brdom4  9352  fpwwe2lem13  9464  fpwwe2  9465  canth4  9469  canthwelem  9472  pwfseqlem4  9484  nqerf  9752  dmrecnq  9790  uzrdgfni  12757  hashdmpropge2  13265  dmtrclfv  13759  rlimpm  14231  isstruct2  15867  strlemor1OLD  15969  strleun  15972  imasaddfnlem  16188  imasvscafn  16197  isohom  16436  catcoppccl  16758  tsrss  17223  ledm  17224  dirdm  17234  f1omvdmvd  17863  mvdco  17865  f1omvdconj  17866  pmtrfb  17885  pmtrfconj  17886  symggen  17890  symggen2  17891  pmtrdifellem1  17896  pmtrdifellem2  17897  psgnunilem1  17913  gsum2d  18371  lspextmo  19056  dsmmfi  20082  lindfres  20162  mdetdiaglem  20404  tsmsxp  21958  ustssco  22018  setsmstopn  22283  metustexhalf  22361  tngtopn  22454  equivcau  23098  cmetss  23113  dvbssntr  23664  pserdv  24183  structgrssvtxlemOLD  25915  subgreldmiedg  26175  hlimcaui  28093  metideq  29936  esum2d  30155  fundmpss  31664  fixssdm  32013  filnetlem3  32375  filnetlem4  32376  ssbnd  33587  bnd2lem  33590  ismrcd1  37261  istopclsd  37263  mptrcllem  37920  cnvrcl0  37932  dmtrcl  37934  dfrcl2  37966  relexpss1d  37997  rp-imass  38065  rfovcnvf1od  38298  fourierdlem80  40403  issmflem  40936