Theorem dmss 5568

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 3815	. . . 4 ⊢ (𝐴 ⊆ 𝐵 → (⟨𝑥, 𝑦⟩ ∈ 𝐴 → ⟨𝑥, 𝑦⟩ ∈ 𝐵))
2	1	eximdv 1960	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐴 → ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐵))
3		vex 3401	. . . 4 ⊢ 𝑥 ∈ V
4	3	eldm2 5567	. . 3 ⊢ (𝑥 ∈ dom 𝐴 ↔ ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐴)
5	3	eldm2 5567	. . 3 ⊢ (𝑥 ∈ dom 𝐵 ↔ ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐵)
6	2, 4, 5	3imtr4g 288	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ dom 𝐴 → 𝑥 ∈ dom 𝐵))
7	6	ssrdv 3827	1 ⊢ (𝐴 ⊆ 𝐵 → dom 𝐴 ⊆ dom 𝐵)

Syntax hints:   → wi 4  ∃wex 1823   ∈ wcel 2107   ⊆ wss 3792  ⟨cop 4404  dom cdm 5355

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-rab 3099  df-v 3400  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-nul 4142  df-if 4308  df-sn 4399  df-pr 4401  df-op 4405  df-br 4887  df-dm 5365

This theorem is referenced by:  dmeq  5569  dmv  5586  rnss  5599  dmiin  5615  ssxpb  5822  sofld  5835  relrelss  5913  funssxp  6311  fndmdif  6584  fneqeql2  6589  dff3  6636  frxp  7568  fnwelem  7573  funsssuppss  7603  tposss  7635  wfrlem16  7713  smores  7732  smores2  7734  tfrlem13  7769  imafi  8547  hartogslem1  8736  wemapso  8745  r0weon  9168  infxpenlem  9169  brdom3  9685  brdom5  9686  brdom4  9687  fpwwe2lem13  9799  fpwwe2  9800  canth4  9804  canthwelem  9807  pwfseqlem4  9819  nqerf  10087  dmrecnq  10125  uzrdgfni  13076  hashdmpropge2  13579  dmtrclfv  14166  rlimpm  14639  isstruct2  16265  strleun  16364  imasaddfnlem  16574  imasvscafn  16583  isohom  16821  catcoppccl  17143  tsrss  17609  ledm  17610  dirdm  17620  f1omvdmvd  18246  mvdco  18248  f1omvdconj  18249  pmtrfb  18268  pmtrfconj  18269  symggen  18273  symggen2  18274  pmtrdifellem1  18279  pmtrdifellem2  18280  psgnunilem1  18296  gsum2d  18757  lspextmo  19451  dsmmfi  20481  lindfres  20566  mdetdiaglem  20809  tsmsxp  22366  ustssco  22426  setsmstopn  22691  metustexhalf  22769  tngtopn  22862  equivcau  23506  metsscmetcld  23521  dvbssntr  24101  pserdv  24620  subgreldmiedg  26630  hlimcaui  28665  metideq  30534  esum2d  30753  fundmpss  32257  fixssdm  32602  filnetlem3  32963  filnetlem4  32964  ssbnd  34213  bnd2lem  34216  ismrcd1  38225  istopclsd  38227  mptrcllem  38881  cnvrcl0  38893  dmtrcl  38895  dfrcl2  38927  relexpss1d  38958  rp-imass  39025  rfovcnvf1od  39258  fourierdlem80  41334  issmflem  41867