Theorem dmss 5293

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 3582	. . . 4 ⊢ (𝐴 ⊆ 𝐵 → (⟨𝑥, 𝑦⟩ ∈ 𝐴 → ⟨𝑥, 𝑦⟩ ∈ 𝐵))
2	1	eximdv 1843	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐴 → ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐵))
3		vex 3193	. . . 4 ⊢ 𝑥 ∈ V
4	3	eldm2 5292	. . 3 ⊢ (𝑥 ∈ dom 𝐴 ↔ ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐴)
5	3	eldm2 5292	. . 3 ⊢ (𝑥 ∈ dom 𝐵 ↔ ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐵)
6	2, 4, 5	3imtr4g 285	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ dom 𝐴 → 𝑥 ∈ dom 𝐵))
7	6	ssrdv 3594	1 ⊢ (𝐴 ⊆ 𝐵 → dom 𝐴 ⊆ dom 𝐵)

Syntax hints:   → wi 4  ∃wex 1701   ∈ wcel 1987   ⊆ wss 3560  ⟨cop 4161  dom cdm 5084

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-rab 2917  df-v 3192  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-nul 3898  df-if 4065  df-sn 4156  df-pr 4158  df-op 4162  df-br 4624  df-dm 5094

This theorem is referenced by:  dmeq  5294  dmv  5311  rnss  5324  dmiin  5339  ssxpb  5537  sofld  5550  relrelss  5628  funssxp  6028  fndmdif  6287  fneqeql2  6292  dff3  6338  frxp  7247  fnwelem  7252  funsssuppss  7281  tposss  7313  wfrlem16  7390  smores  7409  smores2  7411  tfrlem13  7446  imafi  8219  hartogslem1  8407  wemapso  8416  r0weon  8795  infxpenlem  8796  brdom3  9310  brdom5  9311  brdom4  9312  fpwwe2lem13  9424  fpwwe2  9425  canth4  9429  canthwelem  9432  pwfseqlem4  9444  nqerf  9712  dmrecnq  9750  uzrdgfni  12713  hashdmpropge2  13219  dmtrclfv  13709  rlimpm  14181  isstruct2  15809  strlemor1OLD  15909  strleun  15912  imasaddfnlem  16128  imasvscafn  16137  isohom  16376  catcoppccl  16698  tsrss  17163  ledm  17164  dirdm  17174  f1omvdmvd  17803  mvdco  17805  f1omvdconj  17806  pmtrfb  17825  pmtrfconj  17826  symggen  17830  symggen2  17831  pmtrdifellem1  17836  pmtrdifellem2  17837  psgnunilem1  17853  gsum2d  18311  lspextmo  18996  dsmmfi  20022  lindfres  20102  mdetdiaglem  20344  tsmsxp  21898  ustssco  21958  setsmstopn  22223  metustexhalf  22301  tngtopn  22394  equivcau  23038  cmetss  23053  dvbssntr  23604  pserdv  24121  structgrssvtxlemOLD  25849  subgreldmiedg  26102  hlimcaui  27981  metideq  29760  esum2d  29978  fundmpss  31421  fixssdm  31708  filnetlem3  32070  filnetlem4  32071  ssbnd  33258  bnd2lem  33261  ismrcd1  36780  istopclsd  36782  mptrcllem  37440  cnvrcl0  37452  dmtrcl  37454  dfrcl2  37486  relexpss1d  37517  rp-imass  37586  rfovcnvf1od  37819  fourierdlem80  39740  issmflem  40273