Theorem 3sstr4d 4028

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

Syntax hints:   → wi 4   = wceq 1541   ⊆ wss 3947

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-in 3954  df-ss 3964

This theorem is referenced by:  rescnvimafod  7072  suppimacnvss  8154  suppimacnv  8155  ressuppss  8164  suppun  8165  ressuppssdif  8166  suppfnss  8170  suppssov1  8179  suppssfv  8183  omwordri  8568  oewordri  8588  oaabs2  8644  naddssim  8680  fiss  9415  harword  9554  fin1a2lem12  10402  fzoss1  13655  fzoss2  13656  swrd0  14604  cshimadifsn  14776  trclfvss  14949  trclfvcotrg  14959  relexpnnrn  14988  vdwlem6  16915  vdwlem8  16917  hashbcss  16933  mrcss  17556  snsymgefmndeq  19256  gsumzf1o  19774  gsumzaddlem  19783  dprdres  19892  dprdz  19894  dprdf1o  19896  mptscmfsupp0  20529  lspss  20587  lspsntrim  20701  aspss  21422  resspsrbas  21526  resspsradd  21527  resspsrmul  21528  clsss  22549  ntrss  22550  sslm  22794  1stcfb  22940  txss12  23100  prdstopn  23123  imasncls  23187  fmss  23441  flfssfcf  23533  cnpfcfi  23535  ressprdsds  23868  metss2lem  24011  metustto  24053  pi1addval  24555  pi1xfrcnv  24564  equivcau  24808  rrxmvallem  24912  uniiccvol  25088  dyaddisjlem  25103  volsup2  25113  itg2monolem1  25259  itg2gt0  25269  plyss  25704  lgamucov  26531  madess  27360  ifpsnprss  28869  wlkp1lem7  28925  occon  30527  spanss  30588  shlej1  30600  chscllem1  30877  chscllem2  30878  chscllem3  30879  ofrn2  31852  resf1o  31942  fpwrelmap  31945  fldgenss  32394  orvclteinc  33462  dstfrvclim1  33464  reprss  33617  reprinfz1  33622  revwlk  34103  ss2mcls  34547  heiborlem6  36672  lpssat  37871  lssat  37874  paddass  38697  pclssN  38753  2polssN  38774  polcon3N  38776  paddunN  38786  dibss  40028  dicssdvh  40045  dih2dimb  40103  dih2dimbALTN  40104  dihord5b  40118  dochss  40224  dochspss  40237  dvh3dim3N  40308  lclkrlem2r  40383  lclkr  40392  lclkrs  40398  hgmaprnlem2N  40756  hbtlem4  41853  hbtlem3  41854  itgoss  41890  omabs2  42067  naddgeoa  42130  naddwordnexlem4  42137  trrelind  42401  trrelsuperreldg  42404  trrelsuperrel2dg  42407  relexpss1d  42441  trclrelexplem  42447  relexpaddss  42454  frege97d  42488  frege109d  42493  frege131d  42500  clsk1indlem3  42779  limclner  44353  fourierdlem49  44857  fourierdlem92  44900  ovolval5lem3  45356  rngchomfval  46817  rngccofval  46821  rnghmsscmap2  46824  rnghmsscmap  46825  ringchomfval  46863  ringccofval  46867  rhmsscmap2  46870  rhmsscmap  46871  rhmsscrnghm  46877  rngcresringcat  46881  srhmsubc  46927  fldhmsubc  46935  rhmsubclem3  46939  srhmsubcALTV  46945  fldhmsubcALTV  46953  rhmsubcALTVlem4  46958  rmsuppss  46999  mndpsuppss  47000  scmsuppss  47001  setrecsss  47699