Theorem 3sstr4d 4030

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 4016	. 2 ⊢ (𝜑 → (𝐶 ⊆ 𝐷 ↔ 𝐴 ⊆ 𝐵))
5	1, 4	mpbird 257	1 ⊢ (𝜑 → 𝐶 ⊆ 𝐷)

Syntax hints:   → wi 4   = wceq 1542   ⊆ wss 3949

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 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3956  df-ss 3966

This theorem is referenced by:  rescnvimafod  7076  suppimacnvss  8158  suppimacnv  8159  ressuppss  8168  suppun  8169  ressuppssdif  8170  suppfnss  8174  suppssov1  8183  suppssfv  8187  omwordri  8572  oewordri  8592  oaabs2  8648  naddssim  8684  fiss  9419  harword  9558  fin1a2lem12  10406  fzoss1  13659  fzoss2  13660  swrd0  14608  cshimadifsn  14780  trclfvss  14953  trclfvcotrg  14963  relexpnnrn  14992  vdwlem6  16919  vdwlem8  16921  hashbcss  16937  mrcss  17560  snsymgefmndeq  19262  gsumzf1o  19780  gsumzaddlem  19789  dprdres  19898  dprdz  19900  dprdf1o  19902  mptscmfsupp0  20537  lspss  20595  lspsntrim  20709  aspss  21431  resspsrbas  21535  resspsradd  21536  resspsrmul  21537  clsss  22558  ntrss  22559  sslm  22803  1stcfb  22949  txss12  23109  prdstopn  23132  imasncls  23196  fmss  23450  flfssfcf  23542  cnpfcfi  23544  ressprdsds  23877  metss2lem  24020  metustto  24062  pi1addval  24564  pi1xfrcnv  24573  equivcau  24817  rrxmvallem  24921  uniiccvol  25097  dyaddisjlem  25112  volsup2  25122  itg2monolem1  25268  itg2gt0  25278  plyss  25713  lgamucov  26542  madess  27372  ifpsnprss  28911  wlkp1lem7  28967  occon  30571  spanss  30632  shlej1  30644  chscllem1  30921  chscllem2  30922  chscllem3  30923  ofrn2  31896  resf1o  31986  fpwrelmap  31989  fldgenss  32437  orvclteinc  33505  dstfrvclim1  33507  reprss  33660  reprinfz1  33665  revwlk  34146  ss2mcls  34590  heiborlem6  36732  lpssat  37931  lssat  37934  paddass  38757  pclssN  38813  2polssN  38834  polcon3N  38836  paddunN  38846  dibss  40088  dicssdvh  40105  dih2dimb  40163  dih2dimbALTN  40164  dihord5b  40178  dochss  40284  dochspss  40297  dvh3dim3N  40368  lclkrlem2r  40443  lclkr  40452  lclkrs  40458  hgmaprnlem2N  40816  hbtlem4  41916  hbtlem3  41917  itgoss  41953  omabs2  42130  naddgeoa  42193  naddwordnexlem4  42200  trrelind  42464  trrelsuperreldg  42467  trrelsuperrel2dg  42470  relexpss1d  42504  trclrelexplem  42510  relexpaddss  42517  frege97d  42551  frege109d  42556  frege131d  42563  clsk1indlem3  42842  limclner  44415  fourierdlem49  44919  fourierdlem92  44962  ovolval5lem3  45418  rngchomfval  46912  rngccofval  46916  rnghmsscmap2  46919  rnghmsscmap  46920  ringchomfval  46958  ringccofval  46962  rhmsscmap2  46965  rhmsscmap  46966  rhmsscrnghm  46972  rngcresringcat  46976  srhmsubc  47022  fldhmsubc  47030  rhmsubclem3  47034  srhmsubcALTV  47040  fldhmsubcALTV  47048  rhmsubcALTVlem4  47053  rmsuppss  47094  mndpsuppss  47095  scmsuppss  47096  setrecsss  47794