Theorem sseqtrd 3970

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

Syntax hints:   → wi 4   = wceq 1541   ⊆ wss 3901

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 1968  ax-7 2009  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2728  df-ss 3918

This theorem is referenced by:  sseqtrrd  3971  sseqtrid  3976  3sstr3d  3988  uniintsn  4940  fssdmd  6680  oeeui  8530  nnaword2  8558  oaabs2  8577  naddword2  8620  erssxp  8658  fipwuni  9329  cantnflem3  9600  ficardun2  10112  ackbij1lem12  10140  ackbij1b  10148  fin1a2lem13  10322  winafp  10608  ioodisj  13398  reltrclfv  14940  prodss  15870  mrcssv  17537  mrcsscl  17543  mrcuni  17544  mressmrcd  17550  mreexexlem2d  17568  mreexexlem3d  17569  mreexfidimd  17573  subcss2  17767  resssetc  18016  funcsetcres2  18017  estrres  18062  poslubdg  18335  ipodrsfi  18462  acsmap2d  18478  mrelatlub  18485  mreclatBAD  18486  subsubmgm  18635  subsubm  18741  subsubg  19079  trivsubgd  19082  trivnsgd  19101  oppglsm  19571  subglsm  19602  lsmdisj  19610  gsumval3  19836  dprdres  19959  dprdss  19960  dprd2da  19973  dmdprdsplit2lem  19976  ablfac1b  20001  pgpfac1lem3  20008  subsubrng  20496  subsubrg  20531  rgspnval  20545  issubdrg  20713  islssd  20886  lspun  20938  lspssp  20939  lsslsp  20966  lsslspOLD  20967  lsmssspx  21040  lspabs2  21075  lspabs3  21076  lspsolvlem  21097  lbsextlem3  21115  qsssubdrg  21381  obselocv  21683  lsslindf  21785  sraassa  21824  mplbas2  21997  gsumply1subr  22174  tgcl  22913  basgen  22932  tgfiss  22935  bastop1  22937  bastop2  22938  clsss2  23016  elcls3  23027  topssnei  23068  neiptopnei  23076  neitr  23124  restcls  23125  restlp  23127  ordtrest2  23148  iscncl  23213  cncls2  23217  cncls  23218  cnntr  23219  lmcls  23246  tgcmp  23345  cmpcld  23346  uncmp  23347  hauscmplem  23350  cmpfi  23352  clsconn  23374  2ndcsb  23393  2ndcctbss  23399  2ndcomap  23402  nllyrest  23430  1stckgenlem  23497  kgencn2  23501  kgen2cn  23503  ptbasfi  23525  txcld  23547  txcls  23548  txbasval  23550  neitx  23551  ptcld  23557  ptclsg  23559  txnlly  23581  hausdiag  23589  txkgen  23596  xkopt  23599  xkopjcn  23600  xkococnlem  23603  cnmpt1res  23620  cnmpt2res  23621  imasnopn  23634  imasncld  23635  imasncls  23636  qtopcld  23657  qtoprest  23661  qtopcmap  23663  kqcldsat  23677  kqreglem2  23686  kqnrmlem2  23688  hmeontr  23713  neifil  23824  fgtr  23834  trnei  23836  uffixfr  23867  uffix2  23868  uffixsn  23869  elflim  23915  flimclslem  23928  fclsopn  23958  fclscmpi  23973  fclscmp  23974  alexsubALTlem3  23993  alexsubALT  23995  ptcmplem3  23998  subgntr  24051  opnsubg  24052  clssubg  24053  clsnsg  24054  cldsubg  24055  tgpconncompeqg  24056  snclseqg  24060  tsmsgsum  24083  tsmsid  24084  tgptsmscld  24095  ustssco  24159  utop2nei  24194  utop3cls  24195  utopreg  24196  cnextucn  24246  ressprdsds  24315  lpbl  24447  met2ndci  24466  prdsxmslem2  24473  metustexhalf  24500  psmetutop  24511  tgioo  24740  metdstri  24796  metdseq0  24799  xlebnum  24920  clsocv  25206  metelcls  25261  metsscmetcld  25271  cmetss  25272  relcmpcmet  25274  cmpcmet  25275  minveclem4a  25386  uniioovol  25536  uniioombllem3  25542  limcres  25843  dvbss  25858  perfdvf  25860  dvreslem  25866  dvres2lem  25867  dvmptresicc  25873  dvcnp2  25877  dvcnp2OLD  25878  dvaddbr  25896  dvmulbr  25897  dvmulbrOLD  25898  dvcmulf  25904  dvcj  25910  dvnfre  25912  dvmptres2  25922  dvmptcmul  25924  dvmptntr  25931  dvlip2  25956  dvcnvrelem2  25979  ftc1cn  26006  dvntaylp  26335  taylthlem1  26337  ulmdvlem3  26367  pserulm  26387  nodense  27660  mulsproplem13  28124  mulsproplem14  28125  onsbnd  28277  shsub2  31400  spanssoc  31424  shub2  31458  ococin  31483  ssjo  31522  chub2  31583  spanpr  31655  elnlfn  32003  mdslj1i  32394  mdslmd3i  32407  mdexchi  32410  chirredlem1  32465  atcvat3i  32471  mdsymlem1  32478  mdsymlem5  32482  imadifxp  32676  fnpreimac  32749  suppovss  32760  symgcom2  33166  pmtrcnelor  33173  cycpmco2f1  33206  0ringsubrg  33333  erlval  33340  1fldgenq  33404  0ringidl  33502  elrspunidl  33509  0ringprmidl  33530  drngmxidl  33558  drngmxidlr  33559  idlsrgmulrss1  33592  idlsrgmulrss2  33593  1arithidomlem2  33617  ply1dg3rt0irred  33665  resssra  33743  lsssra  33744  drgextlsp  33750  lvecdim0  33763  lbslsat  33773  dimkerim  33784  fedgmullem2  33787  fedgmul  33788  fldgenfldext  33825  fldextrspunlsplem  33830  fldextrspunlsp  33831  fldextrspunlem1  33832  fldextrspunfld  33833  fldextrspundgdvdslem  33837  fldextrspundgdvds  33838  algextdeglem3  33876  algextdeglem4  33877  qtophaus  33993  locfinreflem  33997  rspecbas  34022  zarclssn  34030  zarmxt1  34037  zarcmplem  34038  fsumcvg4  34107  esum2d  34250  omsmon  34455  omssubadd  34457  carsgclctun  34478  sitgclg  34499  eulerpartlemgf  34536  reprpmtf1o  34783  cvmscld  35467  cvmliftmolem1  35475  cvmlift2lem9  35505  cvmlift2lem11  35507  cvmlift3lem6  35518  opnregcld  36524  ivthALT  36529  neibastop2  36555  fnemeet1  36560  fnejoin1  36562  pibt2  37622  poimirlem11  37832  poimirlem12  37833  poimirlem30  37851  ftc1cnnc  37893  sstotbnd  37976  ssbnd  37989  heibor1lem  38010  heiborlem3  38014  heibor  38022  lsmsat  39268  lssats  39272  lcvexchlem3  39296  lsatcvat3  39312  lkrscss  39358  lkrpssN  39423  pmod1i  40108  pclbtwnN  40157  pclunN  40158  pclss2polN  40181  pcl0N  40182  sspmaplubN  40185  paddunN  40187  pnonsingN  40193  pclfinclN  40210  osumcllem4N  40219  dia2dimlem13  41336  dvhopellsm  41377  dvadiaN  41388  dicelval1stN  41448  dicelval2nd  41449  dihssxp  41512  dihvalrel  41539  dochsscl  41628  dihoml4  41637  dochnoncon  41651  dvh3dim3N  41709  lcfrlem2  41803  lcfrlem5  41806  lcfr  41845  lcdlsp  41881  mapdsn  41901  mapdlsm  41924  mapdpglem1  41932  mapdindp0  41979  hlhilocv  42217  primrootscoprbij  42356  rntrclfvOAI  42933  ismrcd1  42940  ismrcd2  42941  coeq0i  42995  hbtlem6  43371  iocinico  43454  omabs2  43574  naddwordnexlem4  43643  trclubNEW  43860  ntrk2imkb  44278  isotone1  44289  k0004ss3  44394  iccdifprioo  45762  limsupequzmptlem  45972  cncfuni  46130  cncfiooicclem1  46137  dvresntr  46162  itgsubsticclem  46219  fourierdlem42  46393  fourierdlem48  46398  fourierdlem49  46399  fourierdlem50  46400  qndenserrn  46543  prsal  46562  intsaluni  46573  sssalgen  46579  dfsalgen2  46585  sge0split  46653  ismeannd  46711  caragensspw  46753  caragendifcl  46758  carageniuncl  46767  caratheodorylem1  46770  hoicvrrex  46800  ovnssle  46805  ovn02  46812  ovnsubadd  46816  hoidmv1le  46838  ovnlecvr2  46854  ovncvr2  46855  isvonmbl  46882  vonmblss  46884  ovolval4lem2  46894  ovnovollem1  46900  ovnovollem2  46901  incsmf  46986  decsmf  47011  uspgropssxp  48390  mreuniss  49145  restcls2lem  49158  restcls2  49159  cnneiima  49162  imassc  49398