Theorem sseqtrd 3957

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

Syntax hints:   → wi 4   = wceq 1539   ⊆ wss 3883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890  df-ss 3900

This theorem is referenced by:  sseqtrrd  3958  uniintsn  4915  fssdmd  6603  oeeui  8395  nnaword2  8423  oaabs2  8439  erssxp  8479  fipwuni  9115  cantnflem3  9379  ficardun2  9889  ficardun2OLD  9890  ackbij1lem12  9918  ackbij1b  9926  fin1a2lem13  10099  winafp  10384  ioodisj  13143  reltrclfv  14656  prodss  15585  mrcssv  17240  mrcsscl  17246  mrcuni  17247  mressmrcd  17253  mreexexlem2d  17271  mreexexlem3d  17272  mreexfidimd  17276  subcss2  17474  resssetc  17723  funcsetcres2  17724  estrres  17772  poslubdg  18047  ipodrsfi  18172  acsmap2d  18188  mrelatlub  18195  mreclatBAD  18196  subsubm  18370  subsubg  18693  trivsubgd  18696  trivnsgd  18715  oppglsm  19162  subglsm  19194  lsmdisj  19202  gsumval3  19423  dprdres  19546  dprdss  19547  dprd2da  19560  dmdprdsplit2lem  19563  ablfac1b  19588  pgpfac1lem3  19595  issubdrg  19964  subsubrg  19965  islssd  20112  lspun  20164  lspssp  20165  lsslsp  20192  lsmssspx  20265  lspabs2  20297  lspabs3  20298  lspsolvlem  20319  lbsextlem3  20337  qsssubdrg  20569  obselocv  20845  lsslindf  20947  mplbas2  21153  gsumply1subr  21315  tgcl  22027  basgen  22046  tgfiss  22049  bastop1  22051  bastop2  22052  clsss2  22131  elcls3  22142  topssnei  22183  neiptopnei  22191  neitr  22239  restcls  22240  restlp  22242  ordtrest2  22263  iscncl  22328  cncls2  22332  cncls  22333  cnntr  22334  lmcls  22361  tgcmp  22460  cmpcld  22461  uncmp  22462  hauscmplem  22465  cmpfi  22467  clsconn  22489  2ndcsb  22508  2ndcctbss  22514  2ndcomap  22517  nllyrest  22545  1stckgenlem  22612  kgencn2  22616  kgen2cn  22618  ptbasfi  22640  txcld  22662  txcls  22663  txbasval  22665  neitx  22666  ptcld  22672  ptclsg  22674  txnlly  22696  hausdiag  22704  txkgen  22711  xkopt  22714  xkopjcn  22715  xkococnlem  22718  cnmpt1res  22735  cnmpt2res  22736  imasnopn  22749  imasncld  22750  imasncls  22751  qtopcld  22772  qtoprest  22776  qtopcmap  22778  kqcldsat  22792  kqreglem2  22801  kqnrmlem2  22803  hmeontr  22828  neifil  22939  fgtr  22949  trnei  22951  uffixfr  22982  uffix2  22983  uffixsn  22984  elflim  23030  flimclslem  23043  fclsopn  23073  fclscmpi  23088  fclscmp  23089  alexsubALTlem3  23108  alexsubALT  23110  ptcmplem3  23113  subgntr  23166  opnsubg  23167  clssubg  23168  clsnsg  23169  cldsubg  23170  tgpconncompeqg  23171  snclseqg  23175  tsmsgsum  23198  tsmsid  23199  tgptsmscld  23210  ustssco  23274  utop2nei  23310  utop3cls  23311  utopreg  23312  cnextucn  23363  ressprdsds  23432  lpbl  23565  met2ndci  23584  prdsxmslem2  23591  metustexhalf  23618  psmetutop  23629  tgioo  23865  metdstri  23920  metdseq0  23923  xlebnum  24034  clsocv  24319  metelcls  24374  metsscmetcld  24384  cmetss  24385  relcmpcmet  24387  cmpcmet  24388  minveclem4a  24499  uniioovol  24648  uniioombllem3  24654  limcres  24955  dvbss  24970  perfdvf  24972  dvreslem  24978  dvres2lem  24979  dvmptresicc  24985  dvcnp2  24989  dvaddbr  25007  dvmulbr  25008  dvcmulf  25014  dvcj  25019  dvnfre  25021  dvmptres2  25031  dvmptcmul  25033  dvmptntr  25040  dvlip2  25064  dvcnvrelem2  25087  ftc1cn  25112  dvntaylp  25435  taylthlem1  25437  ulmdvlem3  25466  pserulm  25486  shsub2  29588  spanssoc  29612  shub2  29646  ococin  29671  ssjo  29710  chub2  29771  spanpr  29843  elnlfn  30191  mdslj1i  30582  mdslmd3i  30595  mdexchi  30598  chirredlem1  30653  atcvat3i  30659  mdsymlem1  30666  mdsymlem5  30670  imadifxp  30841  fnpreimac  30910  suppovss  30919  symgcom2  31255  pmtrcnelor  31262  cycpmco2f1  31293  0ringidl  31507  elrspunidl  31508  0ringprmidl  31527  idlsrgmulrss1  31558  idlsrgmulrss2  31559  drgextlsp  31583  lvecdim0  31592  lbslsat  31601  dimkerim  31610  fedgmullem2  31613  fedgmul  31614  qtophaus  31688  locfinreflem  31692  rspecbas  31717  zarclssn  31725  zarmxt1  31732  zarcmplem  31733  fsumcvg4  31802  esum2d  31961  omsmon  32165  omssubadd  32167  carsgclctun  32188  sitgclg  32209  eulerpartlemgf  32246  reprpmtf1o  32506  cvmscld  33135  cvmliftmolem1  33143  cvmlift2lem9  33173  cvmlift2lem11  33175  cvmlift3lem6  33186  nodense  33822  opnregcld  34446  ivthALT  34451  neibastop2  34477  fnemeet1  34482  fnejoin1  34484  pibt2  35515  poimirlem11  35715  poimirlem12  35716  poimirlem30  35734  ftc1cnnc  35776  sstotbnd  35860  ssbnd  35873  heibor1lem  35894  heiborlem3  35898  heibor  35906  lsmsat  36949  lssats  36953  lcvexchlem3  36977  lsatcvat3  36993  lkrscss  37039  lkrpssN  37104  pmod1i  37789  pclbtwnN  37838  pclunN  37839  pclss2polN  37862  pcl0N  37863  sspmaplubN  37866  paddunN  37868  pnonsingN  37874  pclfinclN  37891  osumcllem4N  37900  dia2dimlem13  39017  dvhopellsm  39058  dvadiaN  39069  dicelval1stN  39129  dicelval2nd  39130  dihssxp  39193  dihvalrel  39220  dochsscl  39309  dihoml4  39318  dochnoncon  39332  dvh3dim3N  39390  lcfrlem2  39484  lcfrlem5  39487  lcfr  39526  lcdlsp  39562  mapdsn  39582  mapdlsm  39605  mapdpglem1  39613  mapdindp0  39660  hlhilocv  39902  rntrclfvOAI  40429  ismrcd1  40436  ismrcd2  40437  coeq0i  40491  hbtlem6  40870  rgspnval  40909  iocinico  40959  trclubNEW  41116  ntrk2imkb  41536  isotone1  41547  k0004ss3  41652  iccdifprioo  42944  limsupequzmptlem  43159  cncfuni  43317  cncfiooicclem1  43324  dvresntr  43349  itgsubsticclem  43406  fourierdlem42  43580  fourierdlem48  43585  fourierdlem49  43586  fourierdlem50  43587  qndenserrn  43730  prsal  43749  intsaluni  43758  sssalgen  43764  dfsalgen2  43770  sge0split  43837  ismeannd  43895  caragensspw  43937  caragendifcl  43942  carageniuncl  43951  caratheodorylem1  43954  hoicvrrex  43984  ovnssle  43989  ovn02  43996  ovnsubadd  44000  hoidmv1le  44022  ovnlecvr2  44038  ovncvr2  44039  isvonmbl  44066  vonmblss  44068  ovolval4lem2  44078  ovnovollem1  44084  ovnovollem2  44085  incsmf  44165  decsmf  44189  uspgropssxp  45194  subsubmgm  45239  mreuniss  46081  restcls2lem  46094  restcls2  46095  cnneiima  46098