Theorem dmss 5773

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 3963	. . . 4 ⊢ (𝐴 ⊆ 𝐵 → (⟨𝑥, 𝑦⟩ ∈ 𝐴 → ⟨𝑥, 𝑦⟩ ∈ 𝐵))
2	1	eximdv 1918	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐴 → ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐵))
3		vex 3499	. . . 4 ⊢ 𝑥 ∈ V
4	3	eldm2 5772	. . 3 ⊢ (𝑥 ∈ dom 𝐴 ↔ ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐴)
5	3	eldm2 5772	. . 3 ⊢ (𝑥 ∈ dom 𝐵 ↔ ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐵)
6	2, 4, 5	3imtr4g 298	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ dom 𝐴 → 𝑥 ∈ dom 𝐵))
7	6	ssrdv 3975	1 ⊢ (𝐴 ⊆ 𝐵 → dom 𝐴 ⊆ dom 𝐵)

Syntax hints:   → wi 4  ∃wex 1780   ∈ wcel 2114   ⊆ wss 3938  ⟨cop 4575  dom cdm 5557

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-rab 3149  df-v 3498  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-nul 4294  df-if 4470  df-sn 4570  df-pr 4572  df-op 4576  df-br 5069  df-dm 5567

This theorem is referenced by:  dmeq  5774  dmv  5794  rnss  5811  dmiin  5827  ssxpb  6033  sofld  6046  relrelss  6126  funssxp  6537  fndmdif  6814  fneqeql2  6819  dff3  6868  frxp  7822  fnwelem  7827  funsssuppss  7858  tposss  7895  wfrlem16  7972  smores  7991  smores2  7993  tfrlem13  8028  imafi  8819  hartogslem1  9008  wemapso  9017  r0weon  9440  infxpenlem  9441  brdom3  9952  brdom5  9953  brdom4  9954  fpwwe2lem13  10066  fpwwe2  10067  canth4  10071  canthwelem  10074  pwfseqlem4  10086  nqerf  10354  dmrecnq  10392  uzrdgfni  13329  hashdmpropge2  13844  dmtrclfv  14380  rlimpm  14859  isstruct2  16495  strleun  16593  imasaddfnlem  16803  imasvscafn  16812  isohom  17048  catcoppccl  17370  tsrss  17835  ledm  17836  dirdm  17846  f1omvdmvd  18573  mvdco  18575  f1omvdconj  18576  pmtrfb  18595  pmtrfconj  18596  symggen  18600  symggen2  18601  pmtrdifellem1  18606  pmtrdifellem2  18607  psgnunilem1  18623  gsum2d  19094  lspextmo  19830  dsmmfi  20884  lindfres  20969  mdetdiaglem  21209  tsmsxp  22765  ustssco  22825  setsmstopn  23090  metustexhalf  23168  tngtopn  23261  equivcau  23905  metsscmetcld  23920  dvbssntr  24500  pserdv  25019  subgreldmiedg  27067  hlimcaui  29015  nfpconfp  30379  symgcom2  30730  pmtrcnel  30735  pmtrcnel2  30736  pmtrcnelor  30737  cycpmrn  30787  metideq  31135  esum2d  31354  subgrwlk  32381  fundmpss  33011  frrlem8  33132  frrlem14  33138  fixssdm  33369  filnetlem3  33730  filnetlem4  33731  ssbnd  35068  bnd2lem  35071  ismrcd1  39302  istopclsd  39304  mptrcllem  39980  cnvrcl0  39992  dmtrcl  39994  dfrcl2  40026  relexpss1d  40057  rp-imass  40124  rfovcnvf1od  40357  fourierdlem80  42478  issmflem  43011