Theorem sseqtrd 4022

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

Hypotheses

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

Assertion

Ref	Expression
sseqtrd	⊢ (𝜑 → 𝐴 ⊆ 𝐶)

Proof of Theorem sseqtrd

Step	Hyp	Ref	Expression
1		sseqtrd.1	. 2 ⊢ (𝜑 → 𝐴 ⊆ 𝐵)
2		sseqtrd.2	. . 3 ⊢ (𝜑 → 𝐵 = 𝐶)
3	2	sseq2d 4014	. 2 ⊢ (𝜑 → (𝐴 ⊆ 𝐵 ↔ 𝐴 ⊆ 𝐶))
4	1, 3	mpbid 231	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:  sseqtrrd  4023  sseqtrid  4034  uniintsn  4994  fssdmd  6746  oeeui  8629  nnaword2  8657  oaabs2  8676  naddword2  8719  erssxp  8754  fipwuni  9457  cantnflem3  9722  ficardun2  10233  ficardun2OLD  10234  ackbij1lem12  10262  ackbij1b  10270  fin1a2lem13  10443  winafp  10728  ioodisj  13499  reltrclfv  15004  prodss  15931  mrcssv  17601  mrcsscl  17607  mrcuni  17608  mressmrcd  17614  mreexexlem2d  17632  mreexexlem3d  17633  mreexfidimd  17637  subcss2  17836  resssetc  18088  funcsetcres2  18089  estrres  18137  poslubdg  18413  ipodrsfi  18538  acsmap2d  18554  mrelatlub  18561  mreclatBAD  18562  subsubmgm  18677  subsubm  18775  subsubg  19111  trivsubgd  19115  trivnsgd  19134  oppglsm  19604  subglsm  19635  lsmdisj  19643  gsumval3  19869  dprdres  19992  dprdss  19993  dprd2da  20006  dmdprdsplit2lem  20009  ablfac1b  20034  pgpfac1lem3  20041  subsubrng  20507  subsubrg  20544  issubdrg  20675  islssd  20826  lspun  20878  lspssp  20879  lsslsp  20906  lsslspOLD  20907  lsmssspx  20980  lspabs2  21015  lspabs3  21016  lspsolvlem  21037  lbsextlem3  21055  qsssubdrg  21366  obselocv  21669  lsslindf  21771  sraassa  21809  mplbas2  21987  gsumply1subr  22159  tgcl  22892  basgen  22911  tgfiss  22914  bastop1  22916  bastop2  22917  clsss2  22996  elcls3  23007  topssnei  23048  neiptopnei  23056  neitr  23104  restcls  23105  restlp  23107  ordtrest2  23128  iscncl  23193  cncls2  23197  cncls  23198  cnntr  23199  lmcls  23226  tgcmp  23325  cmpcld  23326  uncmp  23327  hauscmplem  23330  cmpfi  23332  clsconn  23354  2ndcsb  23373  2ndcctbss  23379  2ndcomap  23382  nllyrest  23410  1stckgenlem  23477  kgencn2  23481  kgen2cn  23483  ptbasfi  23505  txcld  23527  txcls  23528  txbasval  23530  neitx  23531  ptcld  23537  ptclsg  23539  txnlly  23561  hausdiag  23569  txkgen  23576  xkopt  23579  xkopjcn  23580  xkococnlem  23583  cnmpt1res  23600  cnmpt2res  23601  imasnopn  23614  imasncld  23615  imasncls  23616  qtopcld  23637  qtoprest  23641  qtopcmap  23643  kqcldsat  23657  kqreglem2  23666  kqnrmlem2  23668  hmeontr  23693  neifil  23804  fgtr  23814  trnei  23816  uffixfr  23847  uffix2  23848  uffixsn  23849  elflim  23895  flimclslem  23908  fclsopn  23938  fclscmpi  23953  fclscmp  23954  alexsubALTlem3  23973  alexsubALT  23975  ptcmplem3  23978  subgntr  24031  opnsubg  24032  clssubg  24033  clsnsg  24034  cldsubg  24035  tgpconncompeqg  24036  snclseqg  24040  tsmsgsum  24063  tsmsid  24064  tgptsmscld  24075  ustssco  24139  utop2nei  24175  utop3cls  24176  utopreg  24177  cnextucn  24228  ressprdsds  24297  lpbl  24432  met2ndci  24451  prdsxmslem2  24458  metustexhalf  24485  psmetutop  24496  tgioo  24732  metdstri  24787  metdseq0  24790  xlebnum  24911  clsocv  25198  metelcls  25253  metsscmetcld  25263  cmetss  25264  relcmpcmet  25266  cmpcmet  25267  minveclem4a  25378  uniioovol  25528  uniioombllem3  25534  limcres  25835  dvbss  25850  perfdvf  25852  dvreslem  25858  dvres2lem  25859  dvmptresicc  25865  dvcnp2  25869  dvcnp2OLD  25870  dvaddbr  25888  dvmulbr  25889  dvmulbrOLD  25890  dvcmulf  25896  dvcj  25902  dvnfre  25904  dvmptres2  25914  dvmptcmul  25916  dvmptntr  25923  dvlip2  25948  dvcnvrelem2  25971  ftc1cn  25998  dvntaylp  26326  taylthlem1  26328  ulmdvlem3  26358  pserulm  26378  nodense  27645  mulsproplem13  28048  mulsproplem14  28049  shsub2  31155  spanssoc  31179  shub2  31213  ococin  31238  ssjo  31277  chub2  31338  spanpr  31410  elnlfn  31758  mdslj1i  32149  mdslmd3i  32162  mdexchi  32165  chirredlem1  32220  atcvat3i  32226  mdsymlem1  32233  mdsymlem5  32237  imadifxp  32412  fnpreimac  32478  suppovss  32486  symgcom2  32828  pmtrcnelor  32835  cycpmco2f1  32866  0ringsubrg  32969  erlval  32997  1fldgenq  33033  0ringidl  33161  elrspunidl  33169  0ringprmidl  33190  drngmxidl  33215  idlsrgmulrss1  33247  idlsrgmulrss2  33248  0ringufd  33257  resssra  33320  lsssra  33321  drgextlsp  33326  lvecdim0  33337  lbslsat  33347  dimkerim  33358  fedgmullem2  33361  fedgmul  33362  algextdeglem3  33420  algextdeglem4  33421  qtophaus  33470  locfinreflem  33474  rspecbas  33499  zarclssn  33507  zarmxt1  33514  zarcmplem  33515  fsumcvg4  33584  esum2d  33745  omsmon  33951  omssubadd  33953  carsgclctun  33974  sitgclg  33995  eulerpartlemgf  34032  reprpmtf1o  34291  cvmscld  34916  cvmliftmolem1  34924  cvmlift2lem9  34954  cvmlift2lem11  34956  cvmlift3lem6  34967  opnregcld  35847  ivthALT  35852  neibastop2  35878  fnemeet1  35883  fnejoin1  35885  pibt2  36929  poimirlem11  37137  poimirlem12  37138  poimirlem30  37156  ftc1cnnc  37198  sstotbnd  37281  ssbnd  37294  heibor1lem  37315  heiborlem3  37319  heibor  37327  lsmsat  38512  lssats  38516  lcvexchlem3  38540  lsatcvat3  38556  lkrscss  38602  lkrpssN  38667  pmod1i  39353  pclbtwnN  39402  pclunN  39403  pclss2polN  39426  pcl0N  39427  sspmaplubN  39430  paddunN  39432  pnonsingN  39438  pclfinclN  39455  osumcllem4N  39464  dia2dimlem13  40581  dvhopellsm  40622  dvadiaN  40633  dicelval1stN  40693  dicelval2nd  40694  dihssxp  40757  dihvalrel  40784  dochsscl  40873  dihoml4  40882  dochnoncon  40896  dvh3dim3N  40954  lcfrlem2  41048  lcfrlem5  41051  lcfr  41090  lcdlsp  41126  mapdsn  41146  mapdlsm  41169  mapdpglem1  41177  mapdindp0  41224  hlhilocv  41466  primrootscoprbij  41605  rntrclfvOAI  42142  ismrcd1  42149  ismrcd2  42150  coeq0i  42204  hbtlem6  42584  rgspnval  42623  iocinico  42671  omabs2  42792  naddwordnexlem4  42862  trclubNEW  43080  ntrk2imkb  43498  isotone1  43509  k0004ss3  43614  iccdifprioo  44930  limsupequzmptlem  45145  cncfuni  45303  cncfiooicclem1  45310  dvresntr  45335  itgsubsticclem  45392  fourierdlem42  45566  fourierdlem48  45571  fourierdlem49  45572  fourierdlem50  45573  qndenserrn  45716  prsal  45735  intsaluni  45746  sssalgen  45752  dfsalgen2  45758  sge0split  45826  ismeannd  45884  caragensspw  45926  caragendifcl  45931  carageniuncl  45940  caratheodorylem1  45943  hoicvrrex  45973  ovnssle  45978  ovn02  45985  ovnsubadd  45989  hoidmv1le  46011  ovnlecvr2  46027  ovncvr2  46028  isvonmbl  46055  vonmblss  46057  ovolval4lem2  46067  ovnovollem1  46073  ovnovollem2  46074  incsmf  46159  decsmf  46184  uspgropssxp  47284  mreuniss  47996  restcls2lem  48009  restcls2  48010  cnneiima  48013