Theorem dmss 5212

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 3493	. . . 4 |- ( A C_ B -> ( <. x , y >. e. A -> <. x , y >. e. B ) )
2	1	eximdv 1711	. . 3 |- ( A C_ B -> ( E. y <. x , y >. e. A -> E. y <. x , y >. e. B ) )
3		vex 3112	. . . 4 |- x e. _V
4	3	eldm2 5211	. . 3 |- ( x e. dom A <-> E. y <. x , y >. e. A )
5	3	eldm2 5211	. . 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 3505	1 |- ( A C_ B -> dom A C_ dom B )

Syntax hints:   -> wi 4   E.wex 1613   e. wcel 1819   C_ wss 3471   <.cop 4038   dom cdm 5008

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-rab 2816  df-v 3111  df-dif 3474  df-un 3476  df-in 3478  df-ss 3485  df-nul 3794  df-if 3945  df-sn 4033  df-pr 4035  df-op 4039  df-br 4457  df-dm 5018

This theorem is referenced by:  dmeq  5213  dmv  5228  rnss  5241  dmiin  5256  ssxpb  5448  sofld  5461  relrelss  5537  funssxp  5750  fndmdif  5992  fneqeql2  5997  dff3  6045  frxp  6909  fnwelem  6914  funsssuppss  6944  tposss  6974  smores  7041  smores2  7043  tfrlem13  7077  imafi  7831  hartogslem1  7985  wemapso  7994  r0weon  8407  infxpenlem  8408  brdom3  8923  brdom5  8924  brdom4  8925  fpwwe2lem13  9037  fpwwe2  9038  canth4  9042  canthwelem  9045  pwfseqlem4  9057  nqerf  9325  dmrecnq  9363  uzrdgfni  12072  rlimpm  13335  isstruct2  14653  strlemor1  14739  strleun  14742  imasaddfnlem  14945  imasvscafn  14954  isohom  15192  catcoppccl  15514  tsrss  15980  ledm  15981  dirdm  15991  f1omvdmvd  16595  mvdco  16597  f1omvdconj  16598  pmtrfb  16617  pmtrfconj  16618  symggen  16622  symggen2  16623  pmtrdifellem1  16628  pmtrdifellem2  16629  psgnunilem1  16645  gsum2d  17126  gsum2dOLD  17127  lspextmo  17829  dsmmfi  18896  lindfres  18985  mdetdiaglem  19227  tsmsxp  20783  ustssco  20843  setsmstopn  21107  metustexhalfOLD  21192  metustexhalf  21193  tngtopn  21290  equivcau  21865  cmetss  21879  dvbssntr  22430  pserdv  22950  uhgrares  24435  umgrares  24451  usgrares  24496  hlimcaui  26281  metideq  28033  esum2d  28265  fundmpss  29414  wfrlem16  29575  fixssdm  29761  filnetlem3  30403  filnetlem4  30404  ssbnd  30489  bnd2lem  30492  ismrcd1  30835  istopclsd  30837  fourierdlem80  32172  uhgres  32641  dmtrclfv  37978  rp-imass  37985