Theorem 3sstr4d 3611

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

Syntax hints:   → wi 4   = wceq 1475   ⊆ wss 3540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-in 3547  df-ss 3554

This theorem is referenced by:  suppimacnvss  7192  suppimacnv  7193  ressuppss  7201  suppun  7202  ressuppssdif  7203  suppfnss  7207  suppssov1  7214  suppssfv  7218  omwordri  7539  oewordri  7559  oaabs2  7612  fiss  8213  harword  8353  fin1a2lem12  9116  fzoss1  12364  fzoss2  12365  swrd0  13286  cshimadifsn  13426  trclfvss  13595  trclfvcotrg  13605  relexpnnrn  13633  vdwlem6  15528  vdwlem8  15530  hashbcss  15546  mrcss  16099  gsumzf1o  18136  gsumzaddlem  18144  dprdres  18250  dprdz  18252  dprdf1o  18254  mptscmfsupp0  18751  lspss  18805  lspsntrim  18919  aspss  19153  resspsrbas  19236  resspsradd  19237  resspsrmul  19238  clsss  20668  ntrss  20669  sslm  20913  1stcfb  21058  txss12  21218  prdstopn  21241  imasncls  21305  fmss  21560  flfssfcf  21652  cnpfcfi  21654  ressprdsds  21986  metss2lem  22126  metustto  22168  pi1addval  22656  pi1xfrcnv  22665  equivcau  22906  rrxmvallem  22995  uniiccvol  23154  dyaddisjlem  23169  volsup2  23179  itg2monolem1  23323  itg2gt0  23333  plyss  23759  lgamucov  24564  occon  27530  spanss  27591  shlej1  27603  chscllem1  27880  chscllem2  27881  chscllem3  27882  ofrn2  28822  resf1o  28893  fpwrelmap  28896  orvclteinc  29864  dstfrvclim1  29866  ss2mcls  30719  heiborlem6  32785  lpssat  33318  lssat  33321  paddass  34142  pclssN  34198  2polssN  34219  polcon3N  34221  paddunN  34231  dibss  35476  dicssdvh  35493  dih2dimb  35551  dih2dimbALTN  35552  dihord5b  35566  dochss  35672  dochspss  35685  dvh3dim3N  35756  lclkrlem2r  35831  lclkr  35840  lclkrs  35846  hgmaprnlem2N  36207  hbtlem4  36715  hbtlem3  36716  itgoss  36752  trrelind  36976  trrelsuperreldg  36979  trrelsuperrel2dg  36982  relexpss1d  37016  trclrelexplem  37022  relexpaddss  37029  frege97d  37063  frege109d  37068  frege131d  37075  clsk1indlem3  37361  limclner  38718  fourierdlem49  39048  fourierdlem92  39091  1wlkvtxeledglem  40827  1wlkp1lem7  40888  rngchomfval  41758  rngccofval  41762  rnghmsscmap2  41765  rnghmsscmap  41766  ringchomfval  41804  ringccofval  41808  rhmsscmap2  41811  rhmsscmap  41812  rhmsscrnghm  41818  rngcresringcat  41822  srhmsubc  41868  fldhmsubc  41876  rhmsubclem3  41880  srhmsubcALTV  41887  fldhmsubcALTV  41895  rhmsubcALTVlem4  41900  rmsuppss  41945  mndpsuppss  41946  scmsuppss  41947