Theorem sseqtrrd 3956

Description: Substitution of equality into a subclass relationship. (Contributed by NM, 25-Apr-2004.)

Hypotheses

Ref	Expression
sseqtrrd.1	⊢ (𝜑 → 𝐴 ⊆ 𝐵)
sseqtrrd.2	⊢ (𝜑 → 𝐶 = 𝐵)

Assertion

Ref	Expression
sseqtrrd	⊢ (𝜑 → 𝐴 ⊆ 𝐶)

Proof of Theorem sseqtrrd

Step	Hyp	Ref	Expression
1		sseqtrrd.1	. 2 ⊢ (𝜑 → 𝐴 ⊆ 𝐵)
2		sseqtrrd.2	. . 3 ⊢ (𝜑 → 𝐶 = 𝐵)
3	2	eqcomd 2804	. 2 ⊢ (𝜑 → 𝐵 = 𝐶)
4	1, 3	sseqtrd 3955	1 ⊢ (𝜑 → 𝐴 ⊆ 𝐶)

Syntax hints:   → wi 4   = wceq 1538   ⊆ wss 3881

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-in 3888  df-ss 3898

This theorem is referenced by:  sseqtrrid  3968  funfvima2d  6972  fnfvima  6973  wfrlem17  7954  oaordi  8155  omordi  8175  omlimcl  8187  oen0  8195  domunsncan  8600  f1opwfi  8812  cantnfle  9118  cantnflt  9119  cantnflem1d  9135  r1pwss  9197  rankxplim3  9294  acndom2  9465  fodomfi2  9471  cflm  9661  cflim2  9674  isf34lem5  9789  isf34lem7  9790  isf34lem6  9791  axdc2lem  9859  ttukeylem5  9924  wunex2  10149  ssfzunsn  12948  ccatass  13933  swrdval2  13999  splfv2a  14109  revccat  14119  cshimadifsn  14182  cshimadifsn0  14183  rtrclreclem1  14408  rtrclreclem2  14410  sumrblem  15060  prodrblem  15275  dfphi2  16101  vdwlem1  16307  basprssdmsets  16541  imasaddfnlem  16793  imasaddvallem  16794  imasvscafn  16802  imasvscaval  16803  mreexexlem4d  16910  mreexfidimd  16913  sscpwex  17077  acsmap2d  17781  gsumress  17884  subsubm  17973  frmdsssubm  18018  frmdss2  18020  subsubg  18294  cntzmhm2  18462  cntzcmnf  18958  ablcntzd  18970  gsumzsubmcl  19031  gsumconst  19047  gsumzmhm  19050  subgdmdprd  19149  dprdcntz2  19153  dprd2da  19157  dmdprdsplit2lem  19160  ablfac1eu  19188  pgpfaclem1  19196  pgpfaclem2  19197  issubdrg  19553  subsubrg  19554  subdrgint  19575  lmhmlsp  19814  lspsntri  19862  lspindpi  19897  lidldvgen  20021  gsumfsum  20158  mrccss  20383  frlmsslsp  20485  opsrtoslem2  20724  scmatsgrp1  21127  toponss  21532  ssntr  21663  elcls3  21688  toponmre  21698  neiptoptop  21736  neiptopnei  21737  neitr  21785  ordtbas  21797  ordtopn1  21799  ordtopn2  21800  iscnp3  21849  tgcn  21857  tgcnp  21858  ssidcn  21860  cnclsi  21877  cncls  21879  cncnp  21885  lmcld  21908  tgcmp  22006  cnconn  22027  connima  22030  clsconn  22035  conncompcld  22039  1stccnp  22067  kgentopon  22143  llycmpkgen2  22155  1stckgen  22159  kgencn2  22162  ptopn  22188  txcls  22209  ptpjcn  22216  ptclsg  22220  xkoccn  22224  txcnp  22225  ptcnplem  22226  txcmplem2  22247  xkoptsub  22259  xkopt  22260  xkoco2cn  22263  xkococnlem  22264  xkoinjcn  22292  imasnopn  22295  imasncld  22296  imasncls  22297  qtopkgen  22315  basqtop  22316  tgqtop  22317  qtoprest  22322  kqsat  22336  kqcldsat  22338  kqnrmlem1  22348  kqnrmlem2  22349  hmeontr  22374  reghmph  22398  nrmhmph  22399  fmfnfmlem4  22562  fmfnfm  22563  flimopn  22580  flimclslem  22589  flfnei  22596  lmflf  22610  txflf  22611  fclsopn  22619  fclsfnflim  22632  alexsublem  22649  ptcmplem3  22659  cnextcn  22672  efmndtmd  22706  submtmd  22709  subgtgp  22710  symgtgp  22711  clssubg  22714  clsnsg  22715  tgpconncompeqg  22717  snclseqg  22721  tsmscls  22743  trust  22835  restutop  22843  restutopopn  22844  utop3cls  22857  utopreg  22858  trcfilu  22900  blssec  23042  prdsbl  23098  blssopn  23102  metcnp  23148  cfilucfil  23166  psmetutop  23174  iccntr  23426  icccmplem2  23428  reconnlem1  23431  metnrmlem1a  23463  metnrmlem1  23464  metnrmlem2  23465  metnrmlem3  23466  cnheibor  23560  lebnumlem1  23566  lebnumlem3  23568  lebnumii  23571  clsocv  23854  iscfil2  23870  iscmet3  23897  cmetss  23920  relcmpcmet  23922  bcthlem5  23932  itg1addlem5  24304  perfdvf  24506  dvres3  24516  dvres3a  24517  dvcmul  24547  dvcmulf  24548  dvlip2  24598  lhop1lem  24616  dvcnvrelem1  24620  dvcnvrelem2  24621  dvcnvre  24622  dvcvx  24623  plyco0  24789  plyaddlem1  24810  plymullem1  24811  aalioulem3  24930  ulmdvlem1  24995  axcontlem10  26767  eengtrkg  26780  wlkp1lem7  27469  1wlkdlem4  27925  hsupunss  29126  pjpjpre  29202  ssmd2  30095  superpos  30137  atexch  30164  curry2ima  30468  pfxf1  30644  gsumhashmul  30741  symgcom2  30778  pmtrcnelor  30785  cycpmco2lem7  30824  cycpmconjvlem  30833  cycpmconjv  30834  cyc3conja  30849  elrspunidl  31014  mxidlprm  31048  lssdimle  31094  dimkerim  31111  fedgmullem1  31113  fedgmullem2  31114  fedgmul  31115  madjusmdetlem2  31181  zarclsun  31223  rhmpreimacnlem  31237  ordtconnlem1  31277  measiuns  31586  imambfm  31630  cnmbfm  31631  dya2iocnrect  31649  omsfval  31662  omssubaddlem  31667  omssubadd  31668  totprobd  31794  fzssfzo  31919  signstfvn  31949  bnj999  32340  bnj1408  32418  bnj1442  32431  bnj1450  32432  bnj1501  32449  fnrelpredd  32472  revwlk  32484  cvmsss2  32634  cvmliftmolem1  32641  cvmliftlem3  32647  cvmlift2lem9  32671  cvmlift2lem11  32673  cvmlift3lem6  32684  cvmlift3lem7  32685  ssmclslem  32925  mclsax  32929  mclsppslem  32943  mclspps  32944  dfrdg2  33153  trpredtr  33182  frrlem8  33243  frrlem10  33245  neiin  33793  neibastop2  33822  filnetlem4  33842  rdgssun  34795  lindsdom  35051  poimirlem11  35068  poimirlem12  35069  itg2addnclem2  35109  cnres2  35201  sstotbnd2  35212  sstotbnd  35213  prdstotbnd  35232  heibor1lem  35247  igenval2  35504  lshpnelb  36280  lcvexchlem4  36333  lsatexch  36339  l1cvat  36351  lkrscss  36394  lkrss  36464  lkreqN  36466  paddunN  37223  osumcllem2N  37253  pmapojoinN  37264  pl42lem2N  37276  dibglbN  38462  diblss  38466  dicvaddcl  38486  dicvscacl  38487  diclss  38489  cdlemn5pre  38496  dihord5apre  38558  dihglblem3N  38591  dihglb2  38638  dochsat  38679  dochshpncl  38680  djhspss  38702  dihsumssj  38704  mapdlsm  38960  hdmaprnlem3eN  39154  hdmaplkr  39209  fnwe2lem2  39995  lnmlsslnm  40025  lmhmfgima  40028  hbtlem6  40073  trrelsuperreldg  40369  iunrelexpuztr  40420  clsk1indlem2  40745  grumnudlem  40993  dvsconst  41034  dvsinax  42555  dvbdfbdioolem1  42570  itgsinexplem1  42596  itgperiod  42623  stoweidlem39  42681  dirkeritg  42744  fourierdlem48  42796  fourierdlem49  42797  fourierdlem70  42818  fourierdlem71  42819  fourierdlem81  42829  issalgend  42978  f1oresf1o  43846  subsubmgm  44417  rmsuppss  44772