MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dmss Structured version   Visualization version   GIF version

Theorem dmss 5493
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.
StepHypRef Expression
1 ssel 3757 . . . 4 (𝐴𝐵 → (⟨𝑥, 𝑦⟩ ∈ 𝐴 → ⟨𝑥, 𝑦⟩ ∈ 𝐵))
21eximdv 2012 . . 3 (𝐴𝐵 → (∃𝑦𝑥, 𝑦⟩ ∈ 𝐴 → ∃𝑦𝑥, 𝑦⟩ ∈ 𝐵))
3 vex 3353 . . . 4 𝑥 ∈ V
43eldm2 5492 . . 3 (𝑥 ∈ dom 𝐴 ↔ ∃𝑦𝑥, 𝑦⟩ ∈ 𝐴)
53eldm2 5492 . . 3 (𝑥 ∈ dom 𝐵 ↔ ∃𝑦𝑥, 𝑦⟩ ∈ 𝐵)
62, 4, 53imtr4g 287 . 2 (𝐴𝐵 → (𝑥 ∈ dom 𝐴𝑥 ∈ dom 𝐵))
76ssrdv 3769 1 (𝐴𝐵 → dom 𝐴 ⊆ dom 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wex 1874  wcel 2155  wss 3734  cop 4342  dom cdm 5279
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-rab 3064  df-v 3352  df-dif 3737  df-un 3739  df-in 3741  df-ss 3748  df-nul 4082  df-if 4246  df-sn 4337  df-pr 4339  df-op 4343  df-br 4812  df-dm 5289
This theorem is referenced by:  dmeq  5494  dmv  5511  rnss  5524  dmiin  5540  ssxpb  5753  sofld  5766  relrelss  5847  funssxp  6245  fndmdif  6515  fneqeql2  6520  dff3  6566  frxp  7493  fnwelem  7498  funsssuppss  7528  tposss  7560  wfrlem16  7638  smores  7657  smores2  7659  tfrlem13  7694  imafi  8470  hartogslem1  8658  wemapso  8667  r0weon  9090  infxpenlem  9091  brdom3  9607  brdom5  9608  brdom4  9609  fpwwe2lem13  9721  fpwwe2  9722  canth4  9726  canthwelem  9729  pwfseqlem4  9741  nqerf  10009  dmrecnq  10047  uzrdgfni  12970  hashdmpropge2  13471  dmtrclfv  14058  rlimpm  14530  isstruct2  16154  strlemor1OLD  16255  strleun  16258  imasaddfnlem  16468  imasvscafn  16477  isohom  16715  catcoppccl  17037  tsrss  17503  ledm  17504  dirdm  17514  f1omvdmvd  18140  mvdco  18142  f1omvdconj  18143  pmtrfb  18162  pmtrfconj  18163  symggen  18167  symggen2  18168  pmtrdifellem1  18173  pmtrdifellem2  18174  psgnunilem1  18190  gsum2d  18651  lspextmo  19342  dsmmfi  20372  lindfres  20452  mdetdiaglem  20695  tsmsxp  22251  ustssco  22311  setsmstopn  22576  metustexhalf  22654  tngtopn  22747  equivcau  23391  metsscmetcld  23406  dvbssntr  23969  pserdv  24488  subgreldmiedg  26468  hlimcaui  28570  metideq  30404  esum2d  30623  fundmpss  32130  fixssdm  32478  filnetlem3  32839  filnetlem4  32840  ssbnd  34030  bnd2lem  34033  ismrcd1  37963  istopclsd  37965  mptrcllem  38619  cnvrcl0  38631  dmtrcl  38633  dfrcl2  38665  relexpss1d  38696  rp-imass  38763  rfovcnvf1od  38996  fourierdlem80  41064  issmflem  41600
  Copyright terms: Public domain W3C validator