Theorem sseqtrd 4020

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 4016	. 2 ⊢ (𝜑 → (𝐴 ⊆ 𝐵 ↔ 𝐴 ⊆ 𝐶))
4	1, 3	mpbid 232	1 ⊢ (𝜑 → 𝐴 ⊆ 𝐶)

Syntax hints:   → wi 4   = wceq 1540   ⊆ wss 3951

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2729  df-ss 3968

This theorem is referenced by:  sseqtrrd  4021  sseqtrid  4026  3sstr3d  4038  uniintsn  4985  fssdmd  6754  oeeui  8640  nnaword2  8668  oaabs2  8687  naddword2  8730  erssxp  8768  fipwuni  9466  cantnflem3  9731  ficardun2  10242  ackbij1lem12  10270  ackbij1b  10278  fin1a2lem13  10452  winafp  10737  ioodisj  13522  reltrclfv  15056  prodss  15983  mrcssv  17657  mrcsscl  17663  mrcuni  17664  mressmrcd  17670  mreexexlem2d  17688  mreexexlem3d  17689  mreexfidimd  17693  subcss2  17888  resssetc  18137  funcsetcres2  18138  estrres  18184  poslubdg  18459  ipodrsfi  18584  acsmap2d  18600  mrelatlub  18607  mreclatBAD  18608  subsubmgm  18723  subsubm  18829  subsubg  19167  trivsubgd  19171  trivnsgd  19190  oppglsm  19660  subglsm  19691  lsmdisj  19699  gsumval3  19925  dprdres  20048  dprdss  20049  dprd2da  20062  dmdprdsplit2lem  20065  ablfac1b  20090  pgpfac1lem3  20097  subsubrng  20563  subsubrg  20598  rgspnval  20612  issubdrg  20781  islssd  20933  lspun  20985  lspssp  20986  lsslsp  21013  lsslspOLD  21014  lsmssspx  21087  lspabs2  21122  lspabs3  21123  lspsolvlem  21144  lbsextlem3  21162  qsssubdrg  21444  obselocv  21748  lsslindf  21850  sraassa  21889  mplbas2  22060  gsumply1subr  22235  tgcl  22976  basgen  22995  tgfiss  22998  bastop1  23000  bastop2  23001  clsss2  23080  elcls3  23091  topssnei  23132  neiptopnei  23140  neitr  23188  restcls  23189  restlp  23191  ordtrest2  23212  iscncl  23277  cncls2  23281  cncls  23282  cnntr  23283  lmcls  23310  tgcmp  23409  cmpcld  23410  uncmp  23411  hauscmplem  23414  cmpfi  23416  clsconn  23438  2ndcsb  23457  2ndcctbss  23463  2ndcomap  23466  nllyrest  23494  1stckgenlem  23561  kgencn2  23565  kgen2cn  23567  ptbasfi  23589  txcld  23611  txcls  23612  txbasval  23614  neitx  23615  ptcld  23621  ptclsg  23623  txnlly  23645  hausdiag  23653  txkgen  23660  xkopt  23663  xkopjcn  23664  xkococnlem  23667  cnmpt1res  23684  cnmpt2res  23685  imasnopn  23698  imasncld  23699  imasncls  23700  qtopcld  23721  qtoprest  23725  qtopcmap  23727  kqcldsat  23741  kqreglem2  23750  kqnrmlem2  23752  hmeontr  23777  neifil  23888  fgtr  23898  trnei  23900  uffixfr  23931  uffix2  23932  uffixsn  23933  elflim  23979  flimclslem  23992  fclsopn  24022  fclscmpi  24037  fclscmp  24038  alexsubALTlem3  24057  alexsubALT  24059  ptcmplem3  24062  subgntr  24115  opnsubg  24116  clssubg  24117  clsnsg  24118  cldsubg  24119  tgpconncompeqg  24120  snclseqg  24124  tsmsgsum  24147  tsmsid  24148  tgptsmscld  24159  ustssco  24223  utop2nei  24259  utop3cls  24260  utopreg  24261  cnextucn  24312  ressprdsds  24381  lpbl  24516  met2ndci  24535  prdsxmslem2  24542  metustexhalf  24569  psmetutop  24580  tgioo  24817  metdstri  24873  metdseq0  24876  xlebnum  24997  clsocv  25284  metelcls  25339  metsscmetcld  25349  cmetss  25350  relcmpcmet  25352  cmpcmet  25353  minveclem4a  25464  uniioovol  25614  uniioombllem3  25620  limcres  25921  dvbss  25936  perfdvf  25938  dvreslem  25944  dvres2lem  25945  dvmptresicc  25951  dvcnp2  25955  dvcnp2OLD  25956  dvaddbr  25974  dvmulbr  25975  dvmulbrOLD  25976  dvcmulf  25982  dvcj  25988  dvnfre  25990  dvmptres2  26000  dvmptcmul  26002  dvmptntr  26009  dvlip2  26034  dvcnvrelem2  26057  ftc1cn  26084  dvntaylp  26413  taylthlem1  26415  ulmdvlem3  26445  pserulm  26465  nodense  27737  mulsproplem13  28154  mulsproplem14  28155  shsub2  31344  spanssoc  31368  shub2  31402  ococin  31427  ssjo  31466  chub2  31527  spanpr  31599  elnlfn  31947  mdslj1i  32338  mdslmd3i  32351  mdexchi  32354  chirredlem1  32409  atcvat3i  32415  mdsymlem1  32422  mdsymlem5  32426  imadifxp  32614  fnpreimac  32681  suppovss  32690  symgcom2  33104  pmtrcnelor  33111  cycpmco2f1  33144  0ringsubrg  33255  erlval  33262  1fldgenq  33324  0ringidl  33449  elrspunidl  33456  0ringprmidl  33477  drngmxidl  33505  drngmxidlr  33506  idlsrgmulrss1  33539  idlsrgmulrss2  33540  1arithidomlem2  33564  ply1dg3rt0irred  33607  resssra  33638  lsssra  33639  drgextlsp  33644  lvecdim0  33657  lbslsat  33667  dimkerim  33678  fedgmullem2  33681  fedgmul  33682  fldgenfldext  33718  fldextrspunlsplem  33723  fldextrspunlsp  33724  fldextrspunlem1  33725  fldextrspunfld  33726  fldextrspundgdvdslem  33730  fldextrspundgdvds  33731  algextdeglem3  33760  algextdeglem4  33761  qtophaus  33835  locfinreflem  33839  rspecbas  33864  zarclssn  33872  zarmxt1  33879  zarcmplem  33880  fsumcvg4  33949  esum2d  34094  omsmon  34300  omssubadd  34302  carsgclctun  34323  sitgclg  34344  eulerpartlemgf  34381  reprpmtf1o  34641  cvmscld  35278  cvmliftmolem1  35286  cvmlift2lem9  35316  cvmlift2lem11  35318  cvmlift3lem6  35329  opnregcld  36331  ivthALT  36336  neibastop2  36362  fnemeet1  36367  fnejoin1  36369  pibt2  37418  poimirlem11  37638  poimirlem12  37639  poimirlem30  37657  ftc1cnnc  37699  sstotbnd  37782  ssbnd  37795  heibor1lem  37816  heiborlem3  37820  heibor  37828  lsmsat  39009  lssats  39013  lcvexchlem3  39037  lsatcvat3  39053  lkrscss  39099  lkrpssN  39164  pmod1i  39850  pclbtwnN  39899  pclunN  39900  pclss2polN  39923  pcl0N  39924  sspmaplubN  39927  paddunN  39929  pnonsingN  39935  pclfinclN  39952  osumcllem4N  39961  dia2dimlem13  41078  dvhopellsm  41119  dvadiaN  41130  dicelval1stN  41190  dicelval2nd  41191  dihssxp  41254  dihvalrel  41281  dochsscl  41370  dihoml4  41379  dochnoncon  41393  dvh3dim3N  41451  lcfrlem2  41545  lcfrlem5  41548  lcfr  41587  lcdlsp  41623  mapdsn  41643  mapdlsm  41666  mapdpglem1  41674  mapdindp0  41721  hlhilocv  41963  primrootscoprbij  42103  rntrclfvOAI  42702  ismrcd1  42709  ismrcd2  42710  coeq0i  42764  hbtlem6  43141  iocinico  43224  omabs2  43345  naddwordnexlem4  43414  trclubNEW  43632  ntrk2imkb  44050  isotone1  44061  k0004ss3  44166  iccdifprioo  45529  limsupequzmptlem  45743  cncfuni  45901  cncfiooicclem1  45908  dvresntr  45933  itgsubsticclem  45990  fourierdlem42  46164  fourierdlem48  46169  fourierdlem49  46170  fourierdlem50  46171  qndenserrn  46314  prsal  46333  intsaluni  46344  sssalgen  46350  dfsalgen2  46356  sge0split  46424  ismeannd  46482  caragensspw  46524  caragendifcl  46529  carageniuncl  46538  caratheodorylem1  46541  hoicvrrex  46571  ovnssle  46576  ovn02  46583  ovnsubadd  46587  hoidmv1le  46609  ovnlecvr2  46625  ovncvr2  46626  isvonmbl  46653  vonmblss  46655  ovolval4lem2  46665  ovnovollem1  46671  ovnovollem2  46672  incsmf  46757  decsmf  46782  uspgropssxp  48060  mreuniss  48797  restcls2lem  48810  restcls2  48811  cnneiima  48814