Theorem 3sstr4d 3940

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

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

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 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-ext 2730

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1542  df-ex 1783  df-sb 2071  df-clab 2737  df-cleq 2751  df-clel 2831  df-v 3412  df-in 3866  df-ss 3876

This theorem is referenced by:  suppimacnvss  7845  suppimacnv  7846  ressuppss  7855  suppun  7856  ressuppssdif  7857  suppfnss  7861  suppssov1  7870  suppssfv  7874  omwordri  8206  oewordri  8226  oaabs2  8280  fiss  8911  harword  9050  fin1a2lem12  9861  fzoss1  13103  fzoss2  13104  swrd0  14057  cshimadifsn  14228  trclfvss  14403  trclfvcotrg  14413  relexpnnrn  14442  vdwlem6  16367  vdwlem8  16369  hashbcss  16385  mrcss  16935  snsymgefmndeq  18580  gsumzf1o  19090  gsumzaddlem  19099  dprdres  19208  dprdz  19210  dprdf1o  19212  mptscmfsupp0  19757  lspss  19814  lspsntrim  19928  aspss  20629  resspsrbas  20733  resspsradd  20734  resspsrmul  20735  clsss  21744  ntrss  21745  sslm  21989  1stcfb  22135  txss12  22295  prdstopn  22318  imasncls  22382  fmss  22636  flfssfcf  22728  cnpfcfi  22730  ressprdsds  23063  metss2lem  23203  metustto  23245  pi1addval  23739  pi1xfrcnv  23748  equivcau  23990  rrxmvallem  24094  uniiccvol  24270  dyaddisjlem  24285  volsup2  24295  itg2monolem1  24440  itg2gt0  24450  plyss  24885  lgamucov  25712  ifpsnprss  27501  wlkp1lem7  27558  occon  29159  spanss  29220  shlej1  29232  chscllem1  29509  chscllem2  29510  chscllem3  29511  ofrn2  30489  resf1o  30579  fpwrelmap  30582  orvclteinc  31951  dstfrvclim1  31953  reprss  32106  reprinfz1  32111  revwlk  32592  ss2mcls  33036  madess  33606  heiborlem6  35524  lpssat  36579  lssat  36582  paddass  37404  pclssN  37460  2polssN  37481  polcon3N  37483  paddunN  37493  dibss  38735  dicssdvh  38752  dih2dimb  38810  dih2dimbALTN  38811  dihord5b  38825  dochss  38931  dochspss  38944  dvh3dim3N  39015  lclkrlem2r  39090  lclkr  39099  lclkrs  39105  hgmaprnlem2N  39463  hbtlem4  40433  hbtlem3  40434  itgoss  40470  trrelind  40729  trrelsuperreldg  40732  trrelsuperrel2dg  40735  relexpss1d  40769  trclrelexplem  40775  relexpaddss  40782  frege97d  40816  frege109d  40821  frege131d  40828  clsk1indlem3  41109  limclner  42649  fourierdlem49  43153  fourierdlem92  43196  rngchomfval  44947  rngccofval  44951  rnghmsscmap2  44954  rnghmsscmap  44955  ringchomfval  44993  ringccofval  44997  rhmsscmap2  45000  rhmsscmap  45001  rhmsscrnghm  45007  rngcresringcat  45011  srhmsubc  45057  fldhmsubc  45065  rhmsubclem3  45069  srhmsubcALTV  45075  fldhmsubcALTV  45083  rhmsubcALTVlem4  45088  rmsuppss  45129  mndpsuppss  45130  scmsuppss  45131  setrecsss  45585