Theorem dmss 5883

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 3902	. . . 4 ⊢ (𝐴 ⊆ 𝐵 → (⟨𝑥, 𝑦⟩ ∈ 𝐴 → ⟨𝑥, 𝑦⟩ ∈ 𝐵))
2	1	eximdv 1949	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐴 → ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐵))
3		vex 3454	. . . 4 ⊢ 𝑥 ∈ V
4	3	eldm2 5882	. . 3 ⊢ (𝑥 ∈ dom 𝐴 ↔ ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐴)
5	3	eldm2 5882	. . 3 ⊢ (𝑥 ∈ dom 𝐵 ↔ ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐵)
6	2, 4, 5	3imtr4g 299	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ dom 𝐴 → 𝑥 ∈ dom 𝐵))
7	6	ssrdv 3914	1 ⊢ (𝐴 ⊆ 𝐵 → dom 𝐴 ⊆ dom 𝐵)

This proof depends on syntax axioms:   → wi 4  ∃wex 1811   ∈ wcel 2144   ⊆ wss 3895  ⟨cop 4834  dom cdm 5650

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-un 4151  df-nul 4279  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-br 5103  df-dm 5660

This theorem is used by:  dmeq  5884  dmv  5903  rnss  5920  dmiin  5934  dmresss  6001  ssxpb  6165  sofld  6178  resssxp  6272  relrelss  6275  funssxp  6738  fndmdif  7041  fneqeql2  7046  dff3  7100  frxp  8140  fnwelem  8145  frxp2  8163  frxp3  8170  funsssuppss  8210  tposss  8247  frrlem8  8314  frrlem14  8320  smores2  8365  tfrlem13  8401  imafi  9310  hartogslem1  9539  wemapso  9548  dmttrcl  9725  r0weon  10094  infxpenlem  10095  brdom3  10610  brdom5  10611  brdom4  10612  fpwwe2lem12  10730  fpwwe2  10731  canth4  10735  canthwelem  10738  pwfseqlem4  10750  nqerf  11018  dmrecnq  11056  uzrdgfni  14104  hashdmpropge2  14631  dmtrclfv  15176  rlimpm  15672  isstruct2  17332  strleun  17340  imasaddfnlem  17705  imasvscafn  17714  isohom  17956  catcoppccl  18297  tsrss  18768  ledm  18769  dirdm  18779  f1omvdmvd  19662  mvdco  19664  f1omvdconj  19665  pmtrfb  19684  pmtrfconj  19685  symggen  19689  symggen2  19690  pmtrdifellem1  19695  pmtrdifellem2  19696  psgnunilem1  19712  gsum2d  20191  lspextmo  21336  dsmmfi  22049  lindfres  22134  mdetdiaglem  22918  tsmsxp  24479  ustssco  24539  setsmstopn  24802  metustexhalf  24880  tngtopn  24974  equivcau  25626  metsscmetcld  25641  dvbssntr  26225  pserdv  26761  noseqrdgfn  28697  subgreldmiedg  29869  subgrwlk  30274  hlimcaui  31843  nfpconfp  33273  gsumfs2d  33668  symgcom2  33691  pmtrcnel  33696  pmtrcnel2  33697  pmtrcnelor  33698  cycpmrn  33750  metideq  34571  esum2d  34771  fundmpss  36624  fixssdm  36760  filnetlem3  37260  filnetlem4  37261  ssbnd  38815  bnd2lem  38818  ismrcd1  43802  istopclsd  43804  mptrcllem  44706  cnvrcl0  44718  dmtrcl  44720  dfrcl2  44767  relexpss1d  44798  rfovcnvf1od  45097  fourierdlem80  47289  issmflem  47830