Theorem dmss 5150

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 3461	. . . 4 |- ( A C_ B -> ( <. x , y >. e. A -> <. x , y >. e. B ) )
2	1	eximdv 1677	. . 3 |- ( A C_ B -> ( E. y <. x , y >. e. A -> E. y <. x , y >. e. B ) )
3		vex 3081	. . . 4 |- x e. _V
4	3	eldm2 5149	. . 3 |- ( x e. dom A <-> E. y <. x , y >. e. A )
5	3	eldm2 5149	. . 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 3473	1 |- ( A C_ B -> dom A C_ dom B )

Syntax hints:   -> wi 4   E.wex 1587   e. wcel 1758   C_ wss 3439   <.cop 3994   dom cdm 4951

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-rab 2808  df-v 3080  df-dif 3442  df-un 3444  df-in 3446  df-ss 3453  df-nul 3749  df-if 3903  df-sn 3989  df-pr 3991  df-op 3995  df-br 4404  df-dm 4961

This theorem is referenced by:  dmeq  5151  dmv  5166  rnss  5179  dmiin  5194  ssxpb  5383  sofld  5397  relrelss  5472  funssxp  5682  fndmdif  5919  fneqeql2  5924  dff3  5968  frxp  6795  fnwelem  6800  funsssuppss  6828  tposss  6859  smores  6926  smores2  6928  tfrlem13  6962  imafi  7718  hartogslem1  7870  wemapso  7879  r0weon  8293  infxpenlem  8294  brdom3  8809  brdom5  8810  brdom4  8811  fpwwe2lem13  8923  fpwwe2  8924  canth4  8928  canthwelem  8931  pwfseqlem4  8943  nqerf  9213  dmrecnq  9251  uzrdgfni  11901  rlimpm  13099  isstruct2  14304  strlemor1  14387  strleun  14390  imasaddfnlem  14588  imasvscafn  14597  isohom  14832  catcoppccl  15098  tsrss  15515  ledm  15516  dirdm  15526  f1omvdmvd  16071  mvdco  16073  f1omvdconj  16074  pmtrfb  16093  pmtrfconj  16094  symggen  16098  symggen2  16099  pmtrdifellem1  16104  pmtrdifellem2  16105  psgnunilem1  16121  gsum2d  16588  gsum2dOLD  16589  lspextmo  17263  psgnghm2  18139  dsmmfi  18291  lindfres  18380  mdetdiaglem  18539  tsmsxp  19864  ustssco  19924  setsmstopn  20188  metustexhalfOLD  20273  metustexhalf  20274  tngtopn  20371  equivcau  20946  cmetss  20960  dvbssntr  21511  pserdv  22030  uhgrares  23414  umgrares  23430  usgrares  23460  hlimcaui  24811  metideq  26485  fundmpss  27741  wfrlem16  27903  fixssdm  28101  filnetlem3  28769  filnetlem4  28770  ssbnd  28855  bnd2lem  28858  ismrcd1  29202  istopclsd  29204