Theorem sseqtrrd 4008

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

Syntax hints:   → wi 4   = wceq 1537   ⊆ wss 3936

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-in 3943  df-ss 3952

This theorem is referenced by:  sseqtrrid  4020  funfvima2d  6994  fnfvima  6995  wfrlem17  7971  oaordi  8172  omordi  8192  omlimcl  8204  oen0  8212  domunsncan  8617  f1opwfi  8828  cantnfle  9134  cantnflt  9135  cantnflem1d  9151  r1pwss  9213  rankxplim3  9310  acndom2  9480  fodomfi2  9486  cflm  9672  cflim2  9685  isf34lem5  9800  isf34lem7  9801  isf34lem6  9802  axdc2lem  9870  ttukeylem5  9935  wunex2  10160  ssfzunsn  12954  ccatass  13942  swrdval2  14008  splfv2a  14118  revccat  14128  cshimadifsn  14191  cshimadifsn0  14192  rtrclreclem1  14417  rtrclreclem2  14418  sumrblem  15068  prodrblem  15283  dfphi2  16111  vdwlem1  16317  basprssdmsets  16549  imasaddfnlem  16801  imasaddvallem  16802  imasvscafn  16810  imasvscaval  16811  mreexexlem4d  16918  mreexfidimd  16921  sscpwex  17085  acsmap2d  17789  gsumress  17892  subsubm  17981  frmdsssubm  18026  frmdss2  18028  subsubg  18302  cntzmhm2  18470  cntzcmnf  18965  ablcntzd  18977  gsumzsubmcl  19038  gsumconst  19054  gsumzmhm  19057  subgdmdprd  19156  dprdcntz2  19160  dprd2da  19164  dmdprdsplit2lem  19167  ablfac1eu  19195  pgpfaclem1  19203  pgpfaclem2  19204  issubdrg  19560  subsubrg  19561  subdrgint  19582  lmhmlsp  19821  lspsntri  19869  lspindpi  19904  lidldvgen  20028  opsrtoslem2  20265  gsumfsum  20612  mrccss  20838  frlmsslsp  20940  scmatsgrp1  21131  toponss  21535  ssntr  21666  elcls3  21691  toponmre  21701  neiptoptop  21739  neiptopnei  21740  neitr  21788  ordtbas  21800  ordtopn1  21802  ordtopn2  21803  iscnp3  21852  tgcn  21860  tgcnp  21861  ssidcn  21863  cnclsi  21880  cncls  21882  cncnp  21888  lmcld  21911  tgcmp  22009  cnconn  22030  connima  22033  clsconn  22038  conncompcld  22042  1stccnp  22070  kgentopon  22146  llycmpkgen2  22158  1stckgen  22162  kgencn2  22165  ptopn  22191  txcls  22212  ptpjcn  22219  ptclsg  22223  xkoccn  22227  txcnp  22228  ptcnplem  22229  txcmplem2  22250  xkoptsub  22262  xkopt  22263  xkoco2cn  22266  xkococnlem  22267  xkoinjcn  22295  imasnopn  22298  imasncld  22299  imasncls  22300  qtopkgen  22318  basqtop  22319  tgqtop  22320  qtoprest  22325  kqsat  22339  kqcldsat  22341  kqnrmlem1  22351  kqnrmlem2  22352  hmeontr  22377  reghmph  22401  nrmhmph  22402  fmfnfmlem4  22565  fmfnfm  22566  flimopn  22583  flimclslem  22592  flfnei  22599  lmflf  22613  txflf  22614  fclsopn  22622  fclsfnflim  22635  alexsublem  22652  ptcmplem3  22662  cnextcn  22675  efmndtmd  22709  submtmd  22712  subgtgp  22713  symgtgp  22714  clssubg  22717  clsnsg  22718  tgpconncompeqg  22720  snclseqg  22724  tsmscls  22746  trust  22838  restutop  22846  restutopopn  22847  utop3cls  22860  utopreg  22861  trcfilu  22903  blssec  23045  prdsbl  23101  blssopn  23105  metcnp  23151  cfilucfil  23169  psmetutop  23177  iccntr  23429  icccmplem2  23431  reconnlem1  23434  metnrmlem1a  23466  metnrmlem1  23467  metnrmlem2  23468  metnrmlem3  23469  cnheibor  23559  lebnumlem1  23565  lebnumlem3  23567  lebnumii  23570  clsocv  23853  iscfil2  23869  iscmet3  23896  cmetss  23919  relcmpcmet  23921  bcthlem5  23931  itg1addlem5  24301  perfdvf  24501  dvres3  24511  dvres3a  24512  dvcmul  24541  dvcmulf  24542  dvlip2  24592  lhop1lem  24610  dvcnvrelem1  24614  dvcnvrelem2  24615  dvcnvre  24616  dvcvx  24617  plyco0  24782  plyaddlem1  24803  plymullem1  24804  aalioulem3  24923  ulmdvlem1  24988  axcontlem10  26759  eengtrkg  26772  wlkp1lem7  27461  1wlkdlem4  27919  hsupunss  29120  pjpjpre  29196  ssmd2  30089  superpos  30131  atexch  30158  curry2ima  30444  pfxf1  30618  symgcom2  30728  pmtrcnelor  30735  cycpmco2lem7  30774  cycpmconjvlem  30783  cycpmconjv  30784  cyc3conja  30799  mxidlprm  30977  lssdimle  31006  dimkerim  31023  fedgmullem1  31025  fedgmullem2  31026  fedgmul  31027  madjusmdetlem2  31093  ordtconnlem1  31167  measiuns  31476  imambfm  31520  cnmbfm  31521  dya2iocnrect  31539  omsfval  31552  omssubaddlem  31557  omssubadd  31558  totprobd  31684  fzssfzo  31809  signstfvn  31839  bnj999  32230  bnj1408  32308  bnj1442  32321  bnj1450  32322  bnj1501  32339  revwlk  32371  cvmsss2  32521  cvmliftmolem1  32528  cvmliftlem3  32534  cvmlift2lem9  32558  cvmlift2lem11  32560  cvmlift3lem6  32571  cvmlift3lem7  32572  ssmclslem  32812  mclsax  32816  mclsppslem  32830  mclspps  32831  dfrdg2  33040  trpredtr  33069  frrlem8  33130  frrlem10  33132  neiin  33680  neibastop2  33709  filnetlem4  33729  rdgssun  34662  lindsdom  34901  poimirlem11  34918  poimirlem12  34919  itg2addnclem2  34959  cnres2  35056  sstotbnd2  35067  sstotbnd  35068  prdstotbnd  35087  heibor1lem  35102  igenval2  35359  lshpnelb  36135  lcvexchlem4  36188  lsatexch  36194  l1cvat  36206  lkrscss  36249  lkrss  36319  lkreqN  36321  paddunN  37078  osumcllem2N  37108  pmapojoinN  37119  pl42lem2N  37131  dibglbN  38317  diblss  38321  dicvaddcl  38341  dicvscacl  38342  diclss  38344  cdlemn5pre  38351  dihord5apre  38413  dihglblem3N  38446  dihglb2  38493  dochsat  38534  dochshpncl  38535  djhspss  38557  dihsumssj  38559  mapdlsm  38815  hdmaprnlem3eN  39009  hdmaplkr  39064  fnwe2lem2  39700  lnmlsslnm  39730  lmhmfgima  39733  hbtlem6  39778  trrelsuperreldg  40062  iunrelexpuztr  40113  clsk1indlem2  40441  grumnudlem  40670  dvsconst  40711  dvsinax  42246  dvbdfbdioolem1  42262  itgsinexplem1  42288  itgperiod  42315  stoweidlem39  42373  dirkeritg  42436  fourierdlem48  42488  fourierdlem49  42489  fourierdlem70  42510  fourierdlem71  42511  fourierdlem81  42521  issalgend  42670  f1oresf1o  43538  subsubmgm  44113  rmsuppss  44467