Theorem 3sstr4d 4014

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

Syntax hints:   → wi 4   = wceq 1537   ⊆ wss 3936

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-in 3943  df-ss 3952

This theorem is referenced by:  suppimacnvss  7840  suppimacnv  7841  ressuppss  7849  suppun  7850  ressuppssdif  7851  suppfnss  7855  suppssov1  7862  suppssfv  7866  omwordri  8198  oewordri  8218  oaabs2  8272  fiss  8888  harword  9029  fin1a2lem12  9833  fzoss1  13065  fzoss2  13066  swrd0  14020  cshimadifsn  14191  trclfvss  14366  trclfvcotrg  14376  relexpnnrn  14404  vdwlem6  16322  vdwlem8  16324  hashbcss  16340  mrcss  16887  snsymgefmndeq  18523  gsumzf1o  19032  gsumzaddlem  19041  dprdres  19150  dprdz  19152  dprdf1o  19154  mptscmfsupp0  19699  lspss  19756  lspsntrim  19870  aspss  20106  resspsrbas  20195  resspsradd  20196  resspsrmul  20197  clsss  21662  ntrss  21663  sslm  21907  1stcfb  22053  txss12  22213  prdstopn  22236  imasncls  22300  fmss  22554  flfssfcf  22646  cnpfcfi  22648  ressprdsds  22981  metss2lem  23121  metustto  23163  pi1addval  23652  pi1xfrcnv  23661  equivcau  23903  rrxmvallem  24007  uniiccvol  24181  dyaddisjlem  24196  volsup2  24206  itg2monolem1  24351  itg2gt0  24361  plyss  24789  lgamucov  25615  ifpsnprss  27404  wlkp1lem7  27461  occon  29064  spanss  29125  shlej1  29137  chscllem1  29414  chscllem2  29415  chscllem3  29416  ofrn2  30387  resf1o  30466  fpwrelmap  30469  orvclteinc  31733  dstfrvclim1  31735  reprss  31888  reprinfz1  31893  revwlk  32371  ss2mcls  32815  noetalem4  33220  heiborlem6  35109  lpssat  36164  lssat  36167  paddass  36989  pclssN  37045  2polssN  37066  polcon3N  37068  paddunN  37078  dibss  38320  dicssdvh  38337  dih2dimb  38395  dih2dimbALTN  38396  dihord5b  38410  dochss  38516  dochspss  38529  dvh3dim3N  38600  lclkrlem2r  38675  lclkr  38684  lclkrs  38690  hgmaprnlem2N  39048  hbtlem4  39746  hbtlem3  39747  itgoss  39783  trrelind  40030  trrelsuperreldg  40033  trrelsuperrel2dg  40036  relexpss1d  40070  trclrelexplem  40076  relexpaddss  40083  frege97d  40117  frege109d  40122  frege131d  40129  clsk1indlem3  40413  limclner  41952  fourierdlem49  42460  fourierdlem92  42503  rngchomfval  44257  rngccofval  44261  rnghmsscmap2  44264  rnghmsscmap  44265  ringchomfval  44303  ringccofval  44307  rhmsscmap2  44310  rhmsscmap  44311  rhmsscrnghm  44317  rngcresringcat  44321  srhmsubc  44367  fldhmsubc  44375  rhmsubclem3  44379  srhmsubcALTV  44385  fldhmsubcALTV  44393  rhmsubcALTVlem4  44398  rmsuppss  44438  mndpsuppss  44439  scmsuppss  44440  setrecsss  44823