Theorem sseqtrrd 4018

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

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

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 2697

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2704  df-cleq 2718  df-clel 2804  df-v 3470  df-in 3950  df-ss 3960

This theorem is referenced by:  funfvima2d  7229  fnfvima  7230  frrlem8  8279  frrlem10  8281  fprresex  8296  wfrlem17OLD  8326  oaordi  8547  omordi  8567  omlimcl  8579  oen0  8587  domunsncan  9074  f1opwfi  9358  cantnfle  9668  cantnflt  9669  cantnflem1d  9685  ttrcltr  9713  r1pwss  9781  rankxplim3  9878  acndom2  10051  fodomfi2  10057  cflm  10247  cflim2  10260  isf34lem5  10375  isf34lem7  10376  isf34lem6  10377  axdc2lem  10445  ttukeylem5  10510  wunex2  10735  ssfzunsn  13553  ccatass  14544  swrdval2  14602  splfv2a  14712  revccat  14722  cshimadifsn  14786  cshimadifsn0  14787  rtrclreclem1  15010  rtrclreclem2  15012  sumrblem  15663  prodrblem  15879  dfphi2  16716  vdwlem1  16923  basprssdmsets  17166  imasaddfnlem  17483  imasaddvallem  17484  imasvscafn  17492  imasvscaval  17493  mreexexlem4d  17600  mreexfidimd  17603  sscpwex  17771  acsmap2d  18520  gsumress  18615  subsubmgm  18643  subsubm  18741  frmdsssubm  18786  frmdss2  18788  subsubg  19076  cntzmhm2  19258  cntzcmnf  19765  ablcntzd  19777  gsumzsubmcl  19838  gsumconst  19854  gsumzmhm  19857  subgdmdprd  19956  dprdcntz2  19960  dprd2da  19964  dmdprdsplit2lem  19967  ablfac1eu  19995  pgpfaclem1  20003  pgpfaclem2  20004  subsubrng  20463  subsubrg  20500  issubdrg  20631  subdrgint  20654  lmhmlsp  20897  lspsntri  20945  lspindpi  20983  lidldvgen  21187  gsumfsum  21328  mrccss  21587  frlmsslsp  21691  opsrtoslem2  21959  scmatsgrp1  22379  toponss  22784  ssntr  22917  elcls3  22942  toponmre  22952  neiptoptop  22990  neiptopnei  22991  neitr  23039  ordtbas  23051  ordtopn1  23053  ordtopn2  23054  iscnp3  23103  tgcn  23111  tgcnp  23112  ssidcn  23114  cnclsi  23131  cncls  23133  cncnp  23139  lmcld  23162  tgcmp  23260  cnconn  23281  connima  23284  clsconn  23289  conncompcld  23293  1stccnp  23321  kgentopon  23397  llycmpkgen2  23409  1stckgen  23413  kgencn2  23416  ptopn  23442  txcls  23463  ptpjcn  23470  ptclsg  23474  xkoccn  23478  txcnp  23479  ptcnplem  23480  txcmplem2  23501  xkoptsub  23513  xkopt  23514  xkoco2cn  23517  xkococnlem  23518  xkoinjcn  23546  imasnopn  23549  imasncld  23550  imasncls  23551  qtopkgen  23569  basqtop  23570  tgqtop  23571  qtoprest  23576  kqsat  23590  kqcldsat  23592  kqnrmlem1  23602  kqnrmlem2  23603  hmeontr  23628  reghmph  23652  nrmhmph  23653  fmfnfmlem4  23816  fmfnfm  23817  flimopn  23834  flimclslem  23843  flfnei  23850  lmflf  23864  txflf  23865  fclsopn  23873  fclsfnflim  23886  alexsublem  23903  ptcmplem3  23913  cnextcn  23926  efmndtmd  23960  submtmd  23963  subgtgp  23964  symgtgp  23965  clssubg  23968  clsnsg  23969  tgpconncompeqg  23971  snclseqg  23975  tsmscls  23997  trust  24089  restutop  24097  restutopopn  24098  utop3cls  24111  utopreg  24112  trcfilu  24154  blssec  24296  prdsbl  24355  blssopn  24359  metcnp  24405  cfilucfil  24423  psmetutop  24431  iccntr  24692  icccmplem2  24694  reconnlem1  24697  metnrmlem1a  24729  metnrmlem1  24730  metnrmlem2  24731  metnrmlem3  24732  cnheibor  24836  lebnumlem1  24842  lebnumlem3  24844  lebnumii  24847  clsocv  25133  iscfil2  25149  iscmet3  25176  cmetss  25199  relcmpcmet  25201  bcthlem5  25211  itg1addlem5  25585  perfdvf  25787  dvres3  25797  dvres3a  25798  dvcmul  25830  dvcmulf  25831  dvlip2  25883  lhop1lem  25901  dvcnvrelem1  25905  dvcnvrelem2  25906  dvcnvre  25907  dvcvx  25908  plyco0  26081  plyaddlem1  26102  plymullem1  26103  aalioulem3  26224  ulmdvlem1  26291  precsexlem6  28065  precsexlem7  28066  axcontlem10  28739  eengtrkg  28752  wlkp1lem7  29445  1wlkdlem4  29902  hsupunss  31105  pjpjpre  31181  ssmd2  32074  superpos  32116  atexch  32143  curry2ima  32437  pfxf1  32613  gsumhashmul  32714  symgcom2  32751  pmtrcnelor  32758  cycpmco2lem7  32797  cycpmconjvlem  32806  cycpmconjv  32807  cyc3conja  32822  nsgmgc  33029  nsgqusf1olem3  33032  elrspunidl  33052  mxidlprm  33092  ressply1evl  33156  lssdimle  33210  dimkerim  33230  fedgmullem1  33232  fedgmullem2  33233  fedgmul  33234  madjusmdetlem2  33338  zarclsun  33380  rhmpreimacnlem  33394  ordtconnlem1  33434  measiuns  33745  imambfm  33791  cnmbfm  33792  dya2iocnrect  33810  omsfval  33823  omssubaddlem  33828  omssubadd  33829  totprobd  33955  fzssfzo  34080  signstfvn  34110  bnj999  34498  bnj1408  34576  bnj1442  34589  bnj1450  34590  bnj1501  34607  fnrelpredd  34621  revwlk  34643  cvmsss2  34793  cvmliftmolem1  34800  cvmliftlem3  34806  cvmlift2lem9  34830  cvmlift2lem11  34832  cvmlift3lem6  34843  cvmlift3lem7  34844  ssmclslem  35084  mclsax  35088  mclsppslem  35102  mclspps  35103  dfrdg2  35300  neiin  35725  neibastop2  35754  filnetlem4  35774  rdgssun  36766  lindsdom  36995  poimirlem11  37012  poimirlem12  37013  itg2addnclem2  37053  cnres2  37144  sstotbnd2  37155  sstotbnd  37156  prdstotbnd  37175  heibor1lem  37190  igenval2  37447  lshpnelb  38367  lcvexchlem4  38420  lsatexch  38426  l1cvat  38438  lkrscss  38481  lkrss  38551  lkreqN  38553  paddunN  39311  osumcllem2N  39341  pmapojoinN  39352  pl42lem2N  39364  dibglbN  40550  diblss  40554  dicvaddcl  40574  dicvscacl  40575  diclss  40577  cdlemn5pre  40584  dihord5apre  40646  dihglblem3N  40679  dihglb2  40726  dochsat  40767  dochshpncl  40768  djhspss  40790  dihsumssj  40792  mapdlsm  41048  hdmaprnlem3eN  41242  hdmaplkr  41297  fnwe2lem2  42371  lnmlsslnm  42401  lmhmfgima  42404  hbtlem6  42449  omabs2  42658  tfsconcatrev  42674  naddwordnexlem0  42723  trrelsuperreldg  42995  iunrelexpuztr  43046  clsk1indlem2  43369  grumnudlem  43620  dvsconst  43665  dvsinax  45201  dvbdfbdioolem1  45216  itgsinexplem1  45242  itgperiod  45269  stoweidlem39  45327  dirkeritg  45390  fourierdlem48  45442  fourierdlem49  45443  fourierdlem70  45464  fourierdlem71  45465  fourierdlem81  45475  issalgend  45626  f1oresf1o  46570  rmsuppss  47322  restcls2lem  47819  iscnrm3rlem7  47853