Theorem sseqtrd 3975

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

Syntax hints:   → wi 4   = wceq 1563   ⊆ wss 3907

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-cleq 2757  df-ss 3924

This theorem is referenced by:  sseqtrrd  3976  sseqtrid  3981  3sstr3d  3993  uniintsn  4945  fssdmd  6714  oeeui  8576  nnaword2  8604  oaabs2  8623  naddword2  8667  erssxp  8706  fipwuni  9374  cantnflem3  9648  ficardun2  10173  ackbij1lem12  10201  ackbij1b  10209  fin1a2lem13  10384  winafp  10670  ioodisj  13497  reltrclfv  15042  prodss  15989  mrcssv  17658  mrcsscl  17664  mrcuni  17665  mressmrcd  17671  mreexexlem2d  17689  mreexexlem3d  17690  mreexfidimd  17694  subcss2  17888  resssetc  18137  funcsetcres2  18138  estrres  18183  poslubdg  18456  ipodrsfi  18583  acsmap2d  18599  mrelatlub  18606  mreclatBAD  18607  subsubmgm  18756  subsubm  18863  subsubg  19204  trivsubgd  19207  trivnsgd  19226  oppglsm  19700  subglsm  19731  lsmdisj  19739  gsumval3  19965  dprdres  20088  dprdss  20089  dprd2da  20102  dmdprdsplit2lem  20105  ablfac1b  20130  pgpfac1lem3  20137  subsubrng  20636  subsubrg  20671  rgspnval  20685  issubdrg  20849  islssd  21022  lspun  21074  lspssp  21075  lsslsp  21102  lsmssspx  21175  lspabs2  21210  lspabs3  21211  lspsolvlem  21232  lbsextlem3  21250  0ringidl  21326  0ringprmidl  21434  qsssubdrg  21533  obselocv  21835  lsslindf  21937  sraassa  21976  mplbas2  22150  gsumply1subr  22350  tgcl  23083  basgen  23102  tgfiss  23105  bastop1  23107  bastop2  23108  clsss2  23186  elcls3  23197  topssnei  23238  neiptopnei  23246  neitr  23294  restcls  23295  restlp  23297  ordtrest2  23318  iscncl  23383  cncls2  23387  cncls  23388  cnntr  23389  lmcls  23416  tgcmp  23515  cmpcld  23516  uncmp  23517  hauscmplem  23520  cmpfi  23522  clsconn  23544  2ndcsb  23563  2ndcctbss  23569  2ndcomap  23572  nllyrest  23600  1stckgenlem  23667  kgencn2  23671  kgen2cn  23673  ptbasfi  23695  txcld  23717  txcls  23718  txbasval  23720  neitx  23721  ptcld  23727  ptclsg  23729  txnlly  23751  hausdiag  23759  txkgen  23766  xkopt  23769  xkopjcn  23770  xkococnlem  23773  cnmpt1res  23790  cnmpt2res  23791  imasnopn  23804  imasncld  23805  imasncls  23806  qtopcld  23827  qtoprest  23831  qtopcmap  23833  kqcldsat  23847  kqreglem2  23856  kqnrmlem2  23858  hmeontr  23883  neifil  23994  fgtr  24004  trnei  24006  uffixfr  24037  uffix2  24038  uffixsn  24039  elflim  24085  flimclslem  24098  fclsopn  24128  fclscmpi  24143  fclscmp  24144  alexsubALTlem3  24163  alexsubALT  24165  ptcmplem3  24168  subgntr  24221  opnsubg  24222  clssubg  24223  clsnsg  24224  cldsubg  24225  tgpconncompeqg  24226  snclseqg  24230  tsmsgsum  24253  tsmsid  24254  tgptsmscld  24265  ustssco  24329  utop2nei  24364  utop3cls  24365  utopreg  24366  cnextucn  24416  ressprdsds  24485  lpbl  24617  met2ndci  24636  prdsxmslem2  24643  metustexhalf  24670  psmetutop  24681  tgioo  24910  metdstri  24966  metdseq0  24969  xlebnum  25081  clsocv  25366  metelcls  25421  metsscmetcld  25431  cmetss  25432  relcmpcmet  25434  cmpcmet  25435  minveclem4a  25546  uniioovol  25695  uniioombllem3  25701  limcres  26002  dvbss  26017  perfdvf  26019  dvreslem  26025  dvres2lem  26026  dvmptresicc  26032  dvcnp2  26036  dvaddbr  26054  dvmulbr  26055  dvcmulf  26061  dvcj  26066  dvnfre  26068  dvmptres2  26078  dvmptcmul  26080  dvmptntr  26087  dvlip2  26111  dvcnvrelem2  26134  ftc1cn  26159  dvntaylp  26488  taylthlem1  26490  ulmdvlem3  26519  pserulm  26539  nodense  27810  mulsproplem13  28275  mulsproplem14  28276  onsbnd  28428  shsub2  31582  spanssoc  31606  shub2  31640  ococin  31665  ssjo  31704  chub2  31765  spanpr  31837  elnlfn  32185  mdslj1i  32576  mdslmd3i  32589  mdexchi  32592  chirredlem1  32647  atcvat3i  32653  mdsymlem1  32660  mdsymlem5  32664  imadifxp  32852  fnpreimac  32923  suppovss  32934  symgcom2  33312  pmtrcnelor  33319  cycpmco2f1  33352  0ringsubrg  33479  erlval  33486  1fldgenq  33553  elrspunidl  33647  drngmxidl  33671  drngmxidlr  33672  idlsrgmulrss1  33713  idlsrgmulrss2  33714  1arithidomlem2  33738  ply1dg3rt0irred  33786  resssra  33889  lsssra  33890  drgextlsp  33896  lvecdim0  33909  lbslsat  33918  dimkerim  33929  fedgmullem2  33932  fedgmul  33933  fldgenfldext  33970  fldextrspunlsplem  33975  fldextrspunlsp  33976  fldextrspunlem1  33977  fldextrspunfld  33978  fldextrspundgdvdslem  33982  fldextrspundgdvds  33983  algextdeglem3  34021  algextdeglem4  34022  qtophaus  34138  locfinreflem  34142  rspecbas  34167  zarclssn  34175  zarmxt1  34182  zarcmplem  34183  fsumcvg4  34252  esum2d  34395  omsmon  34600  omssubadd  34602  carsgclctun  34623  sitgclg  34644  eulerpartlemgf  34681  reprpmtf1o  34925  cvmscld  35631  cvmliftmolem1  35639  cvmlift2lem9  35669  cvmlift2lem11  35671  cvmlift3lem6  35682  opnregcld  36698  ivthALT  36703  neibastop2  36729  fnemeet1  36734  fnejoin1  36736  pibt2  37918  poimirlem11  38137  poimirlem12  38138  poimirlem30  38156  ftc1cnnc  38198  sstotbnd  38281  ssbnd  38294  heibor1lem  38315  heiborlem3  38319  heibor  38327  lsmsat  39639  lssats  39643  lcvexchlem3  39667  lsatcvat3  39683  lkrscss  39729  lkrpssN  39794  pmod1i  40479  pclbtwnN  40528  pclunN  40529  pclss2polN  40552  pcl0N  40553  sspmaplubN  40556  paddunN  40558  pnonsingN  40564  pclfinclN  40581  osumcllem4N  40590  dia2dimlem13  41707  dvhopellsm  41748  dvadiaN  41759  dicelval1stN  41819  dicelval2nd  41820  dihssxp  41883  dihvalrel  41910  dochsscl  41999  dihoml4  42008  dochnoncon  42022  dvh3dim3N  42080  lcfrlem2  42174  lcfrlem5  42177  lcfr  42216  lcdlsp  42252  mapdsn  42272  mapdlsm  42295  mapdpglem1  42303  mapdindp0  42350  hlhilocv  42588  primrootscoprbij  42726  rntrclfvOAI  43279  ismrcd1  43286  ismrcd2  43287  coeq0i  43341  hbtlem6  43713  iocinico  43796  omabs2  43916  naddwordnexlem4  43985  trclubNEW  44202  ntrk2imkb  44620  isotone1  44631  k0004ss3  44736  iccdifprioo  46091  limsupequzmptlem  46301  cncfuni  46459  cncfiooicclem1  46466  dvresntr  46491  itgsubsticclem  46548  fourierdlem42  46722  fourierdlem48  46727  fourierdlem49  46728  fourierdlem50  46729  qndenserrn  46872  prsal  46891  intsaluni  46902  sssalgen  46908  dfsalgen2  46914  sge0split  46982  ismeannd  47040  caragensspw  47082  caragendifcl  47087  carageniuncl  47096  caratheodorylem1  47099  hoicvrrex  47129  ovnssle  47134  ovn02  47141  ovnsubadd  47145  hoidmv1le  47167  ovnlecvr2  47183  ovncvr2  47184  isvonmbl  47211  vonmblss  47213  ovolval4lem2  47223  ovnovollem1  47229  ovnovollem2  47230  incsmf  47315  decsmf  47340  uspgropssxp  48765  mreuniss  49530  restcls2lem  49543  restcls2  49544  cnneiima  49547  imassc  49783