Theorem sseqtrrd 4023

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 2734	. 2 ⊢ (𝜑 → 𝐵 = 𝐶)
4	1, 3	sseqtrd 4022	1 ⊢ (𝜑 → 𝐴 ⊆ 𝐶)

Syntax hints:   → wi 4   = wceq 1533   ⊆ wss 3949

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2699

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2706  df-cleq 2720  df-clel 2806  df-v 3475  df-in 3956  df-ss 3966

This theorem is referenced by:  fssrescdmd  7141  funfvima2d  7250  fnfvima  7251  frrlem8  8307  frrlem10  8309  fprresex  8324  wfrlem17OLD  8354  oaordi  8575  omordi  8595  omlimcl  8607  oen0  8615  domunsncan  9105  f1opwfi  9390  cantnfle  9704  cantnflt  9705  cantnflem1d  9721  ttrcltr  9749  r1pwss  9817  rankxplim3  9914  acndom2  10087  fodomfi2  10093  cflm  10283  cflim2  10296  isf34lem5  10411  isf34lem7  10412  isf34lem6  10413  axdc2lem  10481  ttukeylem5  10546  wunex2  10771  ssfzunsn  13589  ccatass  14580  swrdval2  14638  splfv2a  14748  revccat  14758  cshimadifsn  14822  cshimadifsn0  14823  rtrclreclem1  15046  rtrclreclem2  15048  sumrblem  15699  prodrblem  15915  dfphi2  16752  vdwlem1  16959  basprssdmsets  17202  imasaddfnlem  17519  imasaddvallem  17520  imasvscafn  17528  imasvscaval  17529  mreexexlem4d  17636  mreexfidimd  17639  sscpwex  17807  acsmap2d  18556  gsumress  18651  subsubmgm  18679  subsubm  18782  frmdsssubm  18827  frmdss2  18829  subsubg  19118  cntzmhm2  19307  cntzcmnf  19814  ablcntzd  19826  gsumzsubmcl  19887  gsumconst  19903  gsumzmhm  19906  subgdmdprd  20005  dprdcntz2  20009  dprd2da  20013  dmdprdsplit2lem  20016  ablfac1eu  20044  pgpfaclem1  20052  pgpfaclem2  20053  subsubrng  20514  subsubrg  20551  issubdrg  20682  subdrgint  20705  lmhmlsp  20948  lspsntri  20996  lspindpi  21034  lidldvgen  21238  gsumfsum  21381  mrccss  21640  frlmsslsp  21744  opsrtoslem2  22017  ressply1evl  22308  scmatsgrp1  22452  toponss  22857  ssntr  22990  elcls3  23015  toponmre  23025  neiptoptop  23063  neiptopnei  23064  neitr  23112  ordtbas  23124  ordtopn1  23126  ordtopn2  23127  iscnp3  23176  tgcn  23184  tgcnp  23185  ssidcn  23187  cnclsi  23204  cncls  23206  cncnp  23212  lmcld  23235  tgcmp  23333  cnconn  23354  connima  23357  clsconn  23362  conncompcld  23366  1stccnp  23394  kgentopon  23470  llycmpkgen2  23482  1stckgen  23486  kgencn2  23489  ptopn  23515  txcls  23536  ptpjcn  23543  ptclsg  23547  xkoccn  23551  txcnp  23552  ptcnplem  23553  txcmplem2  23574  xkoptsub  23586  xkopt  23587  xkoco2cn  23590  xkococnlem  23591  xkoinjcn  23619  imasnopn  23622  imasncld  23623  imasncls  23624  qtopkgen  23642  basqtop  23643  tgqtop  23644  qtoprest  23649  kqsat  23663  kqcldsat  23665  kqnrmlem1  23675  kqnrmlem2  23676  hmeontr  23701  reghmph  23725  nrmhmph  23726  fmfnfmlem4  23889  fmfnfm  23890  flimopn  23907  flimclslem  23916  flfnei  23923  lmflf  23937  txflf  23938  fclsopn  23946  fclsfnflim  23959  alexsublem  23976  ptcmplem3  23986  cnextcn  23999  efmndtmd  24033  submtmd  24036  subgtgp  24037  symgtgp  24038  clssubg  24041  clsnsg  24042  tgpconncompeqg  24044  snclseqg  24048  tsmscls  24070  trust  24162  restutop  24170  restutopopn  24171  utop3cls  24184  utopreg  24185  trcfilu  24227  blssec  24369  prdsbl  24428  blssopn  24432  metcnp  24478  cfilucfil  24496  psmetutop  24504  iccntr  24765  icccmplem2  24767  reconnlem1  24770  metnrmlem1a  24802  metnrmlem1  24803  metnrmlem2  24804  metnrmlem3  24805  cnheibor  24909  lebnumlem1  24915  lebnumlem3  24917  lebnumii  24920  clsocv  25206  iscfil2  25222  iscmet3  25249  cmetss  25272  relcmpcmet  25274  bcthlem5  25284  itg1addlem5  25658  perfdvf  25860  dvres3  25870  dvres3a  25871  dvcmul  25903  dvcmulf  25904  dvlip2  25956  lhop1lem  25974  dvcnvrelem1  25978  dvcnvrelem2  25979  dvcnvre  25980  dvcvx  25981  plyco0  26154  plyaddlem1  26175  plymullem1  26176  aalioulem3  26297  ulmdvlem1  26364  precsexlem6  28138  precsexlem7  28139  axcontlem10  28812  eengtrkg  28825  wlkp1lem7  29521  1wlkdlem4  29978  hsupunss  31181  pjpjpre  31257  ssmd2  32150  superpos  32192  atexch  32219  curry2ima  32517  pfxf1  32694  gsumhashmul  32799  symgcom2  32836  pmtrcnelor  32843  cycpmco2lem7  32882  cycpmconjvlem  32891  cycpmconjv  32892  cyc3conja  32907  nsgmgc  33155  nsgqusf1olem3  33158  elrspunidl  33177  mxidlprm  33216  rprmdvdsprod  33281  lssdimle  33346  dimkerim  33366  fedgmullem1  33368  fedgmullem2  33369  fedgmul  33370  madjusmdetlem2  33470  zarclsun  33512  rhmpreimacnlem  33526  ordtconnlem1  33566  measiuns  33877  imambfm  33923  cnmbfm  33924  dya2iocnrect  33942  omsfval  33955  omssubaddlem  33960  omssubadd  33961  totprobd  34087  fzssfzo  34212  signstfvn  34242  bnj999  34630  bnj1408  34708  bnj1442  34721  bnj1450  34722  bnj1501  34739  fnrelpredd  34753  revwlk  34775  cvmsss2  34925  cvmliftmolem1  34932  cvmliftlem3  34938  cvmlift2lem9  34962  cvmlift2lem11  34964  cvmlift3lem6  34975  cvmlift3lem7  34976  ssmclslem  35216  mclsax  35220  mclsppslem  35234  mclspps  35235  dfrdg2  35432  neiin  35857  neibastop2  35886  filnetlem4  35906  rdgssun  36898  lindsdom  37128  poimirlem11  37145  poimirlem12  37146  itg2addnclem2  37186  cnres2  37277  sstotbnd2  37288  sstotbnd  37289  prdstotbnd  37308  heibor1lem  37323  igenval2  37580  lshpnelb  38496  lcvexchlem4  38549  lsatexch  38555  l1cvat  38567  lkrscss  38610  lkrss  38680  lkreqN  38682  paddunN  39440  osumcllem2N  39470  pmapojoinN  39481  pl42lem2N  39493  dibglbN  40679  diblss  40683  dicvaddcl  40703  dicvscacl  40704  diclss  40706  cdlemn5pre  40713  dihord5apre  40775  dihglblem3N  40808  dihglb2  40855  dochsat  40896  dochshpncl  40897  djhspss  40919  dihsumssj  40921  mapdlsm  41177  hdmaprnlem3eN  41371  hdmaplkr  41426  fnwe2lem2  42524  lnmlsslnm  42554  lmhmfgima  42557  hbtlem6  42602  omabs2  42810  tfsconcatrev  42826  naddwordnexlem0  42875  trrelsuperreldg  43147  iunrelexpuztr  43198  clsk1indlem2  43521  grumnudlem  43771  dvsconst  43816  dvsinax  45348  dvbdfbdioolem1  45363  itgsinexplem1  45389  itgperiod  45416  stoweidlem39  45474  dirkeritg  45537  fourierdlem48  45589  fourierdlem49  45590  fourierdlem70  45611  fourierdlem71  45612  fourierdlem81  45622  issalgend  45773  f1oresf1o  46717  rmsuppss  47530  restcls2lem  48027  iscnrm3rlem7  48061