Theorem sseqtrd 3972

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

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

This theorem is referenced by:  sseqtrrd  3973  sseqtrid  3978  3sstr3d  3990  uniintsn  4942  fssdmd  6688  oeeui  8540  nnaword2  8568  oaabs2  8587  naddword2  8630  erssxp  8669  fipwuni  9341  cantnflem3  9612  ficardun2  10124  ackbij1lem12  10152  ackbij1b  10160  fin1a2lem13  10334  winafp  10620  ioodisj  13410  reltrclfv  14952  prodss  15882  mrcssv  17549  mrcsscl  17555  mrcuni  17556  mressmrcd  17562  mreexexlem2d  17580  mreexexlem3d  17581  mreexfidimd  17585  subcss2  17779  resssetc  18028  funcsetcres2  18029  estrres  18074  poslubdg  18347  ipodrsfi  18474  acsmap2d  18490  mrelatlub  18497  mreclatBAD  18498  subsubmgm  18647  subsubm  18753  subsubg  19091  trivsubgd  19094  trivnsgd  19113  oppglsm  19583  subglsm  19614  lsmdisj  19622  gsumval3  19848  dprdres  19971  dprdss  19972  dprd2da  19985  dmdprdsplit2lem  19988  ablfac1b  20013  pgpfac1lem3  20020  subsubrng  20508  subsubrg  20543  rgspnval  20557  issubdrg  20725  islssd  20898  lspun  20950  lspssp  20951  lsslsp  20978  lsslspOLD  20979  lsmssspx  21052  lspabs2  21087  lspabs3  21088  lspsolvlem  21109  lbsextlem3  21127  qsssubdrg  21393  obselocv  21695  lsslindf  21797  sraassa  21836  mplbas2  22009  gsumply1subr  22186  tgcl  22925  basgen  22944  tgfiss  22947  bastop1  22949  bastop2  22950  clsss2  23028  elcls3  23039  topssnei  23080  neiptopnei  23088  neitr  23136  restcls  23137  restlp  23139  ordtrest2  23160  iscncl  23225  cncls2  23229  cncls  23230  cnntr  23231  lmcls  23258  tgcmp  23357  cmpcld  23358  uncmp  23359  hauscmplem  23362  cmpfi  23364  clsconn  23386  2ndcsb  23405  2ndcctbss  23411  2ndcomap  23414  nllyrest  23442  1stckgenlem  23509  kgencn2  23513  kgen2cn  23515  ptbasfi  23537  txcld  23559  txcls  23560  txbasval  23562  neitx  23563  ptcld  23569  ptclsg  23571  txnlly  23593  hausdiag  23601  txkgen  23608  xkopt  23611  xkopjcn  23612  xkococnlem  23615  cnmpt1res  23632  cnmpt2res  23633  imasnopn  23646  imasncld  23647  imasncls  23648  qtopcld  23669  qtoprest  23673  qtopcmap  23675  kqcldsat  23689  kqreglem2  23698  kqnrmlem2  23700  hmeontr  23725  neifil  23836  fgtr  23846  trnei  23848  uffixfr  23879  uffix2  23880  uffixsn  23881  elflim  23927  flimclslem  23940  fclsopn  23970  fclscmpi  23985  fclscmp  23986  alexsubALTlem3  24005  alexsubALT  24007  ptcmplem3  24010  subgntr  24063  opnsubg  24064  clssubg  24065  clsnsg  24066  cldsubg  24067  tgpconncompeqg  24068  snclseqg  24072  tsmsgsum  24095  tsmsid  24096  tgptsmscld  24107  ustssco  24171  utop2nei  24206  utop3cls  24207  utopreg  24208  cnextucn  24258  ressprdsds  24327  lpbl  24459  met2ndci  24478  prdsxmslem2  24485  metustexhalf  24512  psmetutop  24523  tgioo  24752  metdstri  24808  metdseq0  24811  xlebnum  24932  clsocv  25218  metelcls  25273  metsscmetcld  25283  cmetss  25284  relcmpcmet  25286  cmpcmet  25287  minveclem4a  25398  uniioovol  25548  uniioombllem3  25554  limcres  25855  dvbss  25870  perfdvf  25872  dvreslem  25878  dvres2lem  25879  dvmptresicc  25885  dvcnp2  25889  dvcnp2OLD  25890  dvaddbr  25908  dvmulbr  25909  dvmulbrOLD  25910  dvcmulf  25916  dvcj  25922  dvnfre  25924  dvmptres2  25934  dvmptcmul  25936  dvmptntr  25943  dvlip2  25968  dvcnvrelem2  25991  ftc1cn  26018  dvntaylp  26347  taylthlem1  26349  ulmdvlem3  26379  pserulm  26399  nodense  27672  mulsproplem13  28136  mulsproplem14  28137  onsbnd  28289  shsub2  31412  spanssoc  31436  shub2  31470  ococin  31495  ssjo  31534  chub2  31595  spanpr  31667  elnlfn  32015  mdslj1i  32406  mdslmd3i  32419  mdexchi  32422  chirredlem1  32477  atcvat3i  32483  mdsymlem1  32490  mdsymlem5  32494  imadifxp  32687  fnpreimac  32759  suppovss  32770  symgcom2  33177  pmtrcnelor  33184  cycpmco2f1  33217  0ringsubrg  33344  erlval  33351  1fldgenq  33415  0ringidl  33513  elrspunidl  33520  0ringprmidl  33541  drngmxidl  33569  drngmxidlr  33570  idlsrgmulrss1  33603  idlsrgmulrss2  33604  1arithidomlem2  33628  ply1dg3rt0irred  33676  resssra  33763  lsssra  33764  drgextlsp  33770  lvecdim0  33783  lbslsat  33793  dimkerim  33804  fedgmullem2  33807  fedgmul  33808  fldgenfldext  33845  fldextrspunlsplem  33850  fldextrspunlsp  33851  fldextrspunlem1  33852  fldextrspunfld  33853  fldextrspundgdvdslem  33857  fldextrspundgdvds  33858  algextdeglem3  33896  algextdeglem4  33897  qtophaus  34013  locfinreflem  34017  rspecbas  34042  zarclssn  34050  zarmxt1  34057  zarcmplem  34058  fsumcvg4  34127  esum2d  34270  omsmon  34475  omssubadd  34477  carsgclctun  34498  sitgclg  34519  eulerpartlemgf  34556  reprpmtf1o  34803  cvmscld  35486  cvmliftmolem1  35494  cvmlift2lem9  35524  cvmlift2lem11  35526  cvmlift3lem6  35537  opnregcld  36543  ivthALT  36548  neibastop2  36574  fnemeet1  36579  fnejoin1  36581  pibt2  37669  poimirlem11  37879  poimirlem12  37880  poimirlem30  37898  ftc1cnnc  37940  sstotbnd  38023  ssbnd  38036  heibor1lem  38057  heiborlem3  38061  heibor  38069  lsmsat  39381  lssats  39385  lcvexchlem3  39409  lsatcvat3  39425  lkrscss  39471  lkrpssN  39536  pmod1i  40221  pclbtwnN  40270  pclunN  40271  pclss2polN  40294  pcl0N  40295  sspmaplubN  40298  paddunN  40300  pnonsingN  40306  pclfinclN  40323  osumcllem4N  40332  dia2dimlem13  41449  dvhopellsm  41490  dvadiaN  41501  dicelval1stN  41561  dicelval2nd  41562  dihssxp  41625  dihvalrel  41652  dochsscl  41741  dihoml4  41750  dochnoncon  41764  dvh3dim3N  41822  lcfrlem2  41916  lcfrlem5  41919  lcfr  41958  lcdlsp  41994  mapdsn  42014  mapdlsm  42037  mapdpglem1  42045  mapdindp0  42092  hlhilocv  42330  primrootscoprbij  42469  rntrclfvOAI  43045  ismrcd1  43052  ismrcd2  43053  coeq0i  43107  hbtlem6  43483  iocinico  43566  omabs2  43686  naddwordnexlem4  43755  trclubNEW  43972  ntrk2imkb  44390  isotone1  44401  k0004ss3  44506  iccdifprioo  45873  limsupequzmptlem  46083  cncfuni  46241  cncfiooicclem1  46248  dvresntr  46273  itgsubsticclem  46330  fourierdlem42  46504  fourierdlem48  46509  fourierdlem49  46510  fourierdlem50  46511  qndenserrn  46654  prsal  46673  intsaluni  46684  sssalgen  46690  dfsalgen2  46696  sge0split  46764  ismeannd  46822  caragensspw  46864  caragendifcl  46869  carageniuncl  46878  caratheodorylem1  46881  hoicvrrex  46911  ovnssle  46916  ovn02  46923  ovnsubadd  46927  hoidmv1le  46949  ovnlecvr2  46965  ovncvr2  46966  isvonmbl  46993  vonmblss  46995  ovolval4lem2  47005  ovnovollem1  47011  ovnovollem2  47012  incsmf  47097  decsmf  47122  uspgropssxp  48501  mreuniss  49256  restcls2lem  49269  restcls2  49270  cnneiima  49273  imassc  49509