Theorem dmss 4865

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 3177	. . . 4 |- ( A C_ B -> ( <. x , y >. e. A -> <. x , y >. e. B ) )
2	1	eximdv 1894	. . 3 |- ( A C_ B -> ( E. y <. x , y >. e. A -> E. y <. x , y >. e. B ) )
3		vex 2766	. . . 4 |- x e. _V
4	3	eldm2 4864	. . 3 |- ( x e. dom A <-> E. y <. x , y >. e. A )
5	3	eldm2 4864	. . 3 |- ( x e. dom B <-> E. y <. x , y >. e. B )
6	2, 4, 5	3imtr4g 205	. 2 |- ( A C_ B -> ( x e. dom A -> x e. dom B ) )
7	6	ssrdv 3189	1 |- ( A C_ B -> dom A C_ dom B )

Syntax hints:   -> wi 4   E.wex 1506   e. wcel 2167   C_ wss 3157   <.cop 3625   dom cdm 4663

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-v 2765  df-un 3161  df-in 3163  df-ss 3170  df-sn 3628  df-pr 3629  df-op 3631  df-br 4034  df-dm 4673

This theorem is referenced by:  dmeq  4866  dmv  4882  rnss  4896  dmiin  4912  dmxpss2  5102  ssxpbm  5105  ssxp1  5106  cocnvres  5194  relrelss  5196  funssxp  5427  fvun1  5627  fndmdif  5667  fneqeql2  5671  tposss  6304  smores  6350  smores2  6352  tfrlemibfn  6386  tfrlemiubacc  6388  tfr1onlembfn  6402  tfr1onlemubacc  6404  tfr1onlemres  6407  tfrcllembfn  6415  tfrcllemubacc  6417  tfrcllemres  6420  frecuzrdgtcl  10504  frecuzrdgdomlem  10509  ennnfonelemex  12631  strleund  12781  strleun  12782  imasaddfnlemg  12957  dvbssntrcntop  14920