Theorem dmss 5848

Description: Subset theorem for domain. (Contributed by NM, 11-Aug-1994.)

Assertion

Ref	Expression
dmss	⊢ (𝐴 ⊆ 𝐵 → dom 𝐴 ⊆ dom 𝐵)

Proof of Theorem dmss

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ssel 3924	. . . 4 ⊢ (𝐴 ⊆ 𝐵 → (⟨𝑥, 𝑦⟩ ∈ 𝐴 → ⟨𝑥, 𝑦⟩ ∈ 𝐵))
2	1	eximdv 1918	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐴 → ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐵))
3		vex 3441	. . . 4 ⊢ 𝑥 ∈ V
4	3	eldm2 5847	. . 3 ⊢ (𝑥 ∈ dom 𝐴 ↔ ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐴)
5	3	eldm2 5847	. . 3 ⊢ (𝑥 ∈ dom 𝐵 ↔ ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐵)
6	2, 4, 5	3imtr4g 296	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ dom 𝐴 → 𝑥 ∈ dom 𝐵))
7	6	ssrdv 3936	1 ⊢ (𝐴 ⊆ 𝐵 → dom 𝐴 ⊆ dom 𝐵)

Syntax hints:   → wi 4  ∃wex 1780   ∈ wcel 2113   ⊆ wss 3898  ⟨cop 4583  dom cdm 5621

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-ss 3915  df-nul 4283  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-br 5096  df-dm 5631

This theorem is referenced by:  dmeq  5849  dmv  5868  rnss  5885  dmiin  5899  dmresss  5966  ssxpb  6128  sofld  6141  resssxp  6224  relrelss  6227  funssxp  6686  fndmdif  6983  fneqeql2  6988  dff3  7041  frxp  8064  fnwelem  8069  frxp2  8082  frxp3  8089  funsssuppss  8128  tposss  8165  frrlem8  8231  frrlem14  8237  smores  8280  smores2  8282  tfrlem13  8317  imafi  9208  hartogslem1  9437  wemapso  9446  dmttrcl  9620  r0weon  9912  infxpenlem  9913  brdom3  10428  brdom5  10429  brdom4  10430  fpwwe2lem12  10542  fpwwe2  10543  canth4  10547  canthwelem  10550  pwfseqlem4  10562  nqerf  10830  dmrecnq  10868  uzrdgfni  13869  hashdmpropge2  14394  dmtrclfv  14929  rlimpm  15411  isstruct2  17064  strleun  17072  imasaddfnlem  17436  imasvscafn  17445  isohom  17687  catcoppccl  18028  tsrss  18499  ledm  18500  dirdm  18510  f1omvdmvd  19359  mvdco  19361  f1omvdconj  19362  pmtrfb  19381  pmtrfconj  19382  symggen  19386  symggen2  19387  pmtrdifellem1  19392  pmtrdifellem2  19393  psgnunilem1  19409  gsum2d  19888  lspextmo  20994  dsmmfi  21679  lindfres  21764  mdetdiaglem  22516  tsmsxp  24073  ustssco  24133  setsmstopn  24396  metustexhalf  24474  tngtopn  24568  equivcau  25230  metsscmetcld  25245  dvbssntr  25831  pserdv  26369  noseqrdgfn  28239  subgreldmiedg  29265  hlimcaui  31220  nfpconfp  32618  gsumfs2d  33044  symgcom2  33062  pmtrcnel  33067  pmtrcnel2  33068  pmtrcnelor  33069  cycpmrn  33121  metideq  33929  esum2d  34129  subgrwlk  35199  fundmpss  35834  fixssdm  35971  filnetlem3  36447  filnetlem4  36448  ssbnd  37851  bnd2lem  37854  ismrcd1  42818  istopclsd  42820  mptrcllem  43733  cnvrcl0  43745  dmtrcl  43747  dfrcl2  43794  relexpss1d  43825  rfovcnvf1od  44124  fourierdlem80  46311  issmflem  46852