Theorem 3sstr4d 3969

Description: Substitution of equality into both sides of a subclass relationship. (Contributed by NM, 30-Nov-1995.) (Proof shortened by Eric Schmidt, 26-Jan-2007.)

Hypotheses

Ref	Expression
3sstr4d.1	⊢ (𝜑 → 𝐴 ⊆ 𝐵)
3sstr4d.2	⊢ (𝜑 → 𝐶 = 𝐴)
3sstr4d.3	⊢ (𝜑 → 𝐷 = 𝐵)

Assertion

Ref	Expression
3sstr4d	⊢ (𝜑 → 𝐶 ⊆ 𝐷)

Proof of Theorem 3sstr4d

Step	Hyp	Ref	Expression
1		3sstr4d.1	. 2 ⊢ (𝜑 → 𝐴 ⊆ 𝐵)
2		3sstr4d.2	. . 3 ⊢ (𝜑 → 𝐶 = 𝐴)
3		3sstr4d.3	. . 3 ⊢ (𝜑 → 𝐷 = 𝐵)
4	2, 3	sseq12d 3955	. 2 ⊢ (𝜑 → (𝐶 ⊆ 𝐷 ↔ 𝐴 ⊆ 𝐵))
5	1, 4	mpbird 256	1 ⊢ (𝜑 → 𝐶 ⊆ 𝐷)

Syntax hints:   → wi 4   = wceq 1539   ⊆ wss 3888

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-v 3435  df-in 3895  df-ss 3905

This theorem is referenced by:  rescnvimafod  6960  suppimacnvss  7998  suppimacnv  7999  ressuppss  8008  suppun  8009  ressuppssdif  8010  suppfnss  8014  suppssov1  8023  suppssfv  8027  omwordri  8412  oewordri  8432  oaabs2  8488  fiss  9192  harword  9331  fin1a2lem12  10176  fzoss1  13423  fzoss2  13424  swrd0  14380  cshimadifsn  14551  trclfvss  14726  trclfvcotrg  14736  relexpnnrn  14765  vdwlem6  16696  vdwlem8  16698  hashbcss  16714  mrcss  17334  snsymgefmndeq  19011  gsumzf1o  19522  gsumzaddlem  19531  dprdres  19640  dprdz  19642  dprdf1o  19644  mptscmfsupp0  20197  lspss  20255  lspsntrim  20369  aspss  21090  resspsrbas  21193  resspsradd  21194  resspsrmul  21195  clsss  22214  ntrss  22215  sslm  22459  1stcfb  22605  txss12  22765  prdstopn  22788  imasncls  22852  fmss  23106  flfssfcf  23198  cnpfcfi  23200  ressprdsds  23533  metss2lem  23676  metustto  23718  pi1addval  24220  pi1xfrcnv  24229  equivcau  24473  rrxmvallem  24577  uniiccvol  24753  dyaddisjlem  24768  volsup2  24778  itg2monolem1  24924  itg2gt0  24934  plyss  25369  lgamucov  26196  ifpsnprss  27999  wlkp1lem7  28056  occon  29658  spanss  29719  shlej1  29731  chscllem1  30008  chscllem2  30009  chscllem3  30010  ofrn2  30986  resf1o  31074  fpwrelmap  31077  orvclteinc  32451  dstfrvclim1  32453  reprss  32606  reprinfz1  32611  revwlk  33095  ss2mcls  33539  naddssim  33846  madess  34068  heiborlem6  35983  lpssat  37034  lssat  37037  paddass  37859  pclssN  37915  2polssN  37936  polcon3N  37938  paddunN  37948  dibss  39190  dicssdvh  39207  dih2dimb  39265  dih2dimbALTN  39266  dihord5b  39280  dochss  39386  dochspss  39399  dvh3dim3N  39470  lclkrlem2r  39545  lclkr  39554  lclkrs  39560  hgmaprnlem2N  39918  hbtlem4  40958  hbtlem3  40959  itgoss  40995  trrelind  41280  trrelsuperreldg  41283  trrelsuperrel2dg  41286  relexpss1d  41320  trclrelexplem  41326  relexpaddss  41333  frege97d  41367  frege109d  41372  frege131d  41379  clsk1indlem3  41660  limclner  43199  fourierdlem49  43703  fourierdlem92  43746  rngchomfval  45535  rngccofval  45539  rnghmsscmap2  45542  rnghmsscmap  45543  ringchomfval  45581  ringccofval  45585  rhmsscmap2  45588  rhmsscmap  45589  rhmsscrnghm  45595  rngcresringcat  45599  srhmsubc  45645  fldhmsubc  45653  rhmsubclem3  45657  srhmsubcALTV  45663  fldhmsubcALTV  45671  rhmsubcALTVlem4  45676  rmsuppss  45717  mndpsuppss  45718  scmsuppss  45719  setrecsss  46417