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 4589  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 4584  df-pr 4586  df-op 4590  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  8138  fnwelem  8143  frxp2  8161  frxp3  8168  funsssuppss  8207  tposss  8244  frrlem8  8311  frrlem14  8317  smores  8360  smores2  8362  tfrlem13  8398  imafi  9307  hartogslem1  9536  wemapso  9545  dmttrcl  9722  r0weon  10091  infxpenlem  10092  brdom3  10607  brdom5  10608  brdom4  10609  fpwwe2lem12  10727  fpwwe2  10728  canth4  10732  canthwelem  10735  pwfseqlem4  10747  nqerf  11015  dmrecnq  11053  uzrdgfni  14101  hashdmpropge2  14628  dmtrclfv  15171  rlimpm  15667  isstruct2  17327  strleun  17335  imasaddfnlem  17700  imasvscafn  17709  isohom  17951  catcoppccl  18292  tsrss  18763  ledm  18764  dirdm  18774  f1omvdmvd  19657  mvdco  19659  f1omvdconj  19660  pmtrfb  19679  pmtrfconj  19680  symggen  19684  symggen2  19685  pmtrdifellem1  19690  pmtrdifellem2  19691  psgnunilem1  19707  gsum2d  20186  lspextmo  21331  dsmmfi  22044  lindfres  22129  mdetdiaglem  22913  tsmsxp  24474  ustssco  24534  setsmstopn  24797  metustexhalf  24875  tngtopn  24969  equivcau  25621  metsscmetcld  25636  dvbssntr  26220  pserdv  26756  noseqrdgfn  28692  subgreldmiedg  29864  subgrwlk  30269  hlimcaui  31838  nfpconfp  33268  gsumfs2d  33664  symgcom2  33687  pmtrcnel  33692  pmtrcnel2  33693  pmtrcnelor  33694  cycpmrn  33746  metideq  34567  esum2d  34767  fundmpss  36574  fixssdm  36710  filnetlem3  37210  filnetlem4  37211  ssbnd  38765  bnd2lem  38768  ismrcd1  43752  istopclsd  43754  mptrcllem  44656  cnvrcl0  44668  dmtrcl  44670  dfrcl2  44717  relexpss1d  44748  rfovcnvf1od  45047  fourierdlem80  47239  issmflem  47780