Theorem dmss 5851

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 3916	. . . 4 ⊢ (𝐴 ⊆ 𝐵 → (⟨𝑥, 𝑦⟩ ∈ 𝐴 → ⟨𝑥, 𝑦⟩ ∈ 𝐵))
2	1	eximdv 1919	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐴 → ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐵))
3		vex 3434	. . . 4 ⊢ 𝑥 ∈ V
4	3	eldm2 5850	. . 3 ⊢ (𝑥 ∈ dom 𝐴 ↔ ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐴)
5	3	eldm2 5850	. . 3 ⊢ (𝑥 ∈ dom 𝐵 ↔ ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐵)
6	2, 4, 5	3imtr4g 296	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ dom 𝐴 → 𝑥 ∈ dom 𝐵))
7	6	ssrdv 3928	1 ⊢ (𝐴 ⊆ 𝐵 → dom 𝐴 ⊆ dom 𝐵)

Syntax hints:   → wi 4  ∃wex 1781   ∈ wcel 2114   ⊆ wss 3890  ⟨cop 4574  dom cdm 5624

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-br 5087  df-dm 5634

This theorem is referenced by:  dmeq  5852  dmv  5871  rnss  5888  dmiin  5902  dmresss  5970  ssxpb  6132  sofld  6145  resssxp  6228  relrelss  6231  funssxp  6690  fndmdif  6988  fneqeql2  6993  dff3  7046  frxp  8069  fnwelem  8074  frxp2  8087  frxp3  8094  funsssuppss  8133  tposss  8170  frrlem8  8236  frrlem14  8242  smores  8285  smores2  8287  tfrlem13  8322  imafi  9218  hartogslem1  9450  wemapso  9459  dmttrcl  9633  r0weon  9925  infxpenlem  9926  brdom3  10441  brdom5  10442  brdom4  10443  fpwwe2lem12  10556  fpwwe2  10557  canth4  10561  canthwelem  10564  pwfseqlem4  10576  nqerf  10844  dmrecnq  10882  uzrdgfni  13911  hashdmpropge2  14436  dmtrclfv  14971  rlimpm  15453  isstruct2  17110  strleun  17118  imasaddfnlem  17483  imasvscafn  17492  isohom  17734  catcoppccl  18075  tsrss  18546  ledm  18547  dirdm  18557  f1omvdmvd  19409  mvdco  19411  f1omvdconj  19412  pmtrfb  19431  pmtrfconj  19432  symggen  19436  symggen2  19437  pmtrdifellem1  19442  pmtrdifellem2  19443  psgnunilem1  19459  gsum2d  19938  lspextmo  21043  dsmmfi  21728  lindfres  21813  mdetdiaglem  22573  tsmsxp  24130  ustssco  24190  setsmstopn  24453  metustexhalf  24531  tngtopn  24625  equivcau  25277  metsscmetcld  25292  dvbssntr  25877  pserdv  26407  noseqrdgfn  28312  subgreldmiedg  29366  hlimcaui  31322  nfpconfp  32720  gsumfs2d  33137  symgcom2  33160  pmtrcnel  33165  pmtrcnel2  33166  pmtrcnelor  33167  cycpmrn  33219  metideq  34053  esum2d  34253  subgrwlk  35330  fundmpss  35965  fixssdm  36102  filnetlem3  36578  filnetlem4  36579  ssbnd  38123  bnd2lem  38126  ismrcd1  43144  istopclsd  43146  mptrcllem  44058  cnvrcl0  44070  dmtrcl  44072  dfrcl2  44119  relexpss1d  44150  rfovcnvf1od  44449  fourierdlem80  46632  issmflem  47173