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

Syntax hints:   → wi 4   = wceq 1542   ⊆ wss 3948

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3955  df-ss 3965

This theorem is referenced by:  funfvima2d  7231  fnfvima  7232  frrlem8  8275  frrlem10  8277  fprresex  8292  wfrlem17OLD  8322  oaordi  8543  omordi  8563  omlimcl  8575  oen0  8583  domunsncan  9069  f1opwfi  9353  cantnfle  9663  cantnflt  9664  cantnflem1d  9680  ttrcltr  9708  r1pwss  9776  rankxplim3  9873  acndom2  10046  fodomfi2  10052  cflm  10242  cflim2  10255  isf34lem5  10370  isf34lem7  10371  isf34lem6  10372  axdc2lem  10440  ttukeylem5  10505  wunex2  10730  ssfzunsn  13544  ccatass  14535  swrdval2  14593  splfv2a  14703  revccat  14713  cshimadifsn  14777  cshimadifsn0  14778  rtrclreclem1  15001  rtrclreclem2  15003  sumrblem  15654  prodrblem  15870  dfphi2  16704  vdwlem1  16911  basprssdmsets  17154  imasaddfnlem  17471  imasaddvallem  17472  imasvscafn  17480  imasvscaval  17481  mreexexlem4d  17588  mreexfidimd  17591  sscpwex  17759  acsmap2d  18505  gsumress  18598  subsubm  18694  frmdsssubm  18739  frmdss2  18741  subsubg  19024  cntzmhm2  19201  cntzcmnf  19708  ablcntzd  19720  gsumzsubmcl  19781  gsumconst  19797  gsumzmhm  19800  subgdmdprd  19899  dprdcntz2  19903  dprd2da  19907  dmdprdsplit2lem  19910  ablfac1eu  19938  pgpfaclem1  19946  pgpfaclem2  19947  issubdrg  20382  subsubrg  20383  subdrgint  20412  lmhmlsp  20653  lspsntri  20701  lspindpi  20738  lidldvgen  20886  gsumfsum  21005  mrccss  21239  frlmsslsp  21343  opsrtoslem2  21609  scmatsgrp1  22016  toponss  22421  ssntr  22554  elcls3  22579  toponmre  22589  neiptoptop  22627  neiptopnei  22628  neitr  22676  ordtbas  22688  ordtopn1  22690  ordtopn2  22691  iscnp3  22740  tgcn  22748  tgcnp  22749  ssidcn  22751  cnclsi  22768  cncls  22770  cncnp  22776  lmcld  22799  tgcmp  22897  cnconn  22918  connima  22921  clsconn  22926  conncompcld  22930  1stccnp  22958  kgentopon  23034  llycmpkgen2  23046  1stckgen  23050  kgencn2  23053  ptopn  23079  txcls  23100  ptpjcn  23107  ptclsg  23111  xkoccn  23115  txcnp  23116  ptcnplem  23117  txcmplem2  23138  xkoptsub  23150  xkopt  23151  xkoco2cn  23154  xkococnlem  23155  xkoinjcn  23183  imasnopn  23186  imasncld  23187  imasncls  23188  qtopkgen  23206  basqtop  23207  tgqtop  23208  qtoprest  23213  kqsat  23227  kqcldsat  23229  kqnrmlem1  23239  kqnrmlem2  23240  hmeontr  23265  reghmph  23289  nrmhmph  23290  fmfnfmlem4  23453  fmfnfm  23454  flimopn  23471  flimclslem  23480  flfnei  23487  lmflf  23501  txflf  23502  fclsopn  23510  fclsfnflim  23523  alexsublem  23540  ptcmplem3  23550  cnextcn  23563  efmndtmd  23597  submtmd  23600  subgtgp  23601  symgtgp  23602  clssubg  23605  clsnsg  23606  tgpconncompeqg  23608  snclseqg  23612  tsmscls  23634  trust  23726  restutop  23734  restutopopn  23735  utop3cls  23748  utopreg  23749  trcfilu  23791  blssec  23933  prdsbl  23992  blssopn  23996  metcnp  24042  cfilucfil  24060  psmetutop  24068  iccntr  24329  icccmplem2  24331  reconnlem1  24334  metnrmlem1a  24366  metnrmlem1  24367  metnrmlem2  24368  metnrmlem3  24369  cnheibor  24463  lebnumlem1  24469  lebnumlem3  24471  lebnumii  24474  clsocv  24759  iscfil2  24775  iscmet3  24802  cmetss  24825  relcmpcmet  24827  bcthlem5  24837  itg1addlem5  25210  perfdvf  25412  dvres3  25422  dvres3a  25423  dvcmul  25453  dvcmulf  25454  dvlip2  25504  lhop1lem  25522  dvcnvrelem1  25526  dvcnvrelem2  25527  dvcnvre  25528  dvcvx  25529  plyco0  25698  plyaddlem1  25719  plymullem1  25720  aalioulem3  25839  ulmdvlem1  25904  precsexlem6  27648  precsexlem7  27649  axcontlem10  28221  eengtrkg  28234  wlkp1lem7  28926  1wlkdlem4  29383  hsupunss  30584  pjpjpre  30660  ssmd2  31553  superpos  31595  atexch  31622  curry2ima  31918  pfxf1  32096  gsumhashmul  32196  symgcom2  32233  pmtrcnelor  32240  cycpmco2lem7  32279  cycpmconjvlem  32288  cycpmconjv  32289  cyc3conja  32304  nsgmgc  32512  nsgqusf1olem3  32515  elrspunidl  32535  mxidlprm  32575  ressply1evl  32636  lssdimle  32681  dimkerim  32701  fedgmullem1  32703  fedgmullem2  32704  fedgmul  32705  madjusmdetlem2  32797  zarclsun  32839  rhmpreimacnlem  32853  ordtconnlem1  32893  measiuns  33204  imambfm  33250  cnmbfm  33251  dya2iocnrect  33269  omsfval  33282  omssubaddlem  33287  omssubadd  33288  totprobd  33414  fzssfzo  33539  signstfvn  33569  bnj999  33958  bnj1408  34036  bnj1442  34049  bnj1450  34050  bnj1501  34067  fnrelpredd  34081  revwlk  34104  cvmsss2  34254  cvmliftmolem1  34261  cvmliftlem3  34267  cvmlift2lem9  34291  cvmlift2lem11  34293  cvmlift3lem6  34304  cvmlift3lem7  34305  ssmclslem  34545  mclsax  34549  mclsppslem  34563  mclspps  34564  dfrdg2  34756  neiin  35206  neibastop2  35235  filnetlem4  35255  rdgssun  36248  lindsdom  36471  poimirlem11  36488  poimirlem12  36489  itg2addnclem2  36529  cnres2  36620  sstotbnd2  36631  sstotbnd  36632  prdstotbnd  36651  heibor1lem  36666  igenval2  36923  lshpnelb  37843  lcvexchlem4  37896  lsatexch  37902  l1cvat  37914  lkrscss  37957  lkrss  38027  lkreqN  38029  paddunN  38787  osumcllem2N  38817  pmapojoinN  38828  pl42lem2N  38840  dibglbN  40026  diblss  40030  dicvaddcl  40050  dicvscacl  40051  diclss  40053  cdlemn5pre  40060  dihord5apre  40122  dihglblem3N  40155  dihglb2  40202  dochsat  40243  dochshpncl  40244  djhspss  40266  dihsumssj  40268  mapdlsm  40524  hdmaprnlem3eN  40718  hdmaplkr  40773  fnwe2lem2  41779  lnmlsslnm  41809  lmhmfgima  41812  hbtlem6  41857  omabs2  42068  tfsconcatrev  42084  naddwordnexlem0  42133  trrelsuperreldg  42405  iunrelexpuztr  42456  clsk1indlem2  42779  grumnudlem  43030  dvsconst  43075  dvsinax  44616  dvbdfbdioolem1  44631  itgsinexplem1  44657  itgperiod  44684  stoweidlem39  44742  dirkeritg  44805  fourierdlem48  44857  fourierdlem49  44858  fourierdlem70  44879  fourierdlem71  44880  fourierdlem81  44890  issalgend  45041  f1oresf1o  45985  subsubmgm  46554  subsubrng  46727  rmsuppss  47000  restcls2lem  47499  iscnrm3rlem7  47533