Theorem sseqtrd 4023

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3956  df-ss 3966

This theorem is referenced by:  sseqtrrd  4024  sseqtrid  4035  uniintsn  4992  fssdmd  6737  oeeui  8602  nnaword2  8630  oaabs2  8648  naddword2  8691  erssxp  8726  fipwuni  9421  cantnflem3  9686  ficardun2  10197  ficardun2OLD  10198  ackbij1lem12  10226  ackbij1b  10234  fin1a2lem13  10407  winafp  10692  ioodisj  13459  reltrclfv  14964  prodss  15891  mrcssv  17558  mrcsscl  17564  mrcuni  17565  mressmrcd  17571  mreexexlem2d  17589  mreexexlem3d  17590  mreexfidimd  17594  subcss2  17793  resssetc  18042  funcsetcres2  18043  estrres  18091  poslubdg  18367  ipodrsfi  18492  acsmap2d  18508  mrelatlub  18515  mreclatBAD  18516  subsubm  18697  subsubg  19029  trivsubgd  19033  trivnsgd  19052  oppglsm  19510  subglsm  19541  lsmdisj  19549  gsumval3  19775  dprdres  19898  dprdss  19899  dprd2da  19912  dmdprdsplit2lem  19915  ablfac1b  19940  pgpfac1lem3  19947  subsubrg  20345  issubdrg  20401  islssd  20546  lspun  20598  lspssp  20599  lsslsp  20626  lsmssspx  20699  lspabs2  20733  lspabs3  20734  lspsolvlem  20755  lbsextlem3  20773  qsssubdrg  21004  obselocv  21283  lsslindf  21385  sraassa  21423  mplbas2  21597  gsumply1subr  21756  tgcl  22472  basgen  22491  tgfiss  22494  bastop1  22496  bastop2  22497  clsss2  22576  elcls3  22587  topssnei  22628  neiptopnei  22636  neitr  22684  restcls  22685  restlp  22687  ordtrest2  22708  iscncl  22773  cncls2  22777  cncls  22778  cnntr  22779  lmcls  22806  tgcmp  22905  cmpcld  22906  uncmp  22907  hauscmplem  22910  cmpfi  22912  clsconn  22934  2ndcsb  22953  2ndcctbss  22959  2ndcomap  22962  nllyrest  22990  1stckgenlem  23057  kgencn2  23061  kgen2cn  23063  ptbasfi  23085  txcld  23107  txcls  23108  txbasval  23110  neitx  23111  ptcld  23117  ptclsg  23119  txnlly  23141  hausdiag  23149  txkgen  23156  xkopt  23159  xkopjcn  23160  xkococnlem  23163  cnmpt1res  23180  cnmpt2res  23181  imasnopn  23194  imasncld  23195  imasncls  23196  qtopcld  23217  qtoprest  23221  qtopcmap  23223  kqcldsat  23237  kqreglem2  23246  kqnrmlem2  23248  hmeontr  23273  neifil  23384  fgtr  23394  trnei  23396  uffixfr  23427  uffix2  23428  uffixsn  23429  elflim  23475  flimclslem  23488  fclsopn  23518  fclscmpi  23533  fclscmp  23534  alexsubALTlem3  23553  alexsubALT  23555  ptcmplem3  23558  subgntr  23611  opnsubg  23612  clssubg  23613  clsnsg  23614  cldsubg  23615  tgpconncompeqg  23616  snclseqg  23620  tsmsgsum  23643  tsmsid  23644  tgptsmscld  23655  ustssco  23719  utop2nei  23755  utop3cls  23756  utopreg  23757  cnextucn  23808  ressprdsds  23877  lpbl  24012  met2ndci  24031  prdsxmslem2  24038  metustexhalf  24065  psmetutop  24076  tgioo  24312  metdstri  24367  metdseq0  24370  xlebnum  24481  clsocv  24767  metelcls  24822  metsscmetcld  24832  cmetss  24833  relcmpcmet  24835  cmpcmet  24836  minveclem4a  24947  uniioovol  25096  uniioombllem3  25102  limcres  25403  dvbss  25418  perfdvf  25420  dvreslem  25426  dvres2lem  25427  dvmptresicc  25433  dvcnp2  25437  dvaddbr  25455  dvmulbr  25456  dvcmulf  25462  dvcj  25467  dvnfre  25469  dvmptres2  25479  dvmptcmul  25481  dvmptntr  25488  dvlip2  25512  dvcnvrelem2  25535  ftc1cn  25560  dvntaylp  25883  taylthlem1  25885  ulmdvlem3  25914  pserulm  25934  nodense  27195  mulsproplem13  27587  mulsproplem14  27588  shsub2  30609  spanssoc  30633  shub2  30667  ococin  30692  ssjo  30731  chub2  30792  spanpr  30864  elnlfn  31212  mdslj1i  31603  mdslmd3i  31616  mdexchi  31619  chirredlem1  31674  atcvat3i  31680  mdsymlem1  31687  mdsymlem5  31691  imadifxp  31863  fnpreimac  31927  suppovss  31937  symgcom2  32276  pmtrcnelor  32283  cycpmco2f1  32314  0ringsubrg  32410  1fldgenq  32443  0ringidl  32570  elrspunidl  32577  0ringprmidl  32599  drngmxidl  32624  idlsrgmulrss1  32656  idlsrgmulrss2  32657  drgextlsp  32712  lvecdim0  32722  lbslsat  32732  dimkerim  32743  fedgmullem2  32746  fedgmul  32747  algextdeglem1  32803  qtophaus  32847  locfinreflem  32851  rspecbas  32876  zarclssn  32884  zarmxt1  32891  zarcmplem  32892  fsumcvg4  32961  esum2d  33122  omsmon  33328  omssubadd  33330  carsgclctun  33351  sitgclg  33372  eulerpartlemgf  33409  reprpmtf1o  33669  cvmscld  34295  cvmliftmolem1  34303  cvmlift2lem9  34333  cvmlift2lem11  34335  cvmlift3lem6  34346  gg-dvcnp2  35205  gg-dvmulbr  35206  opnregcld  35263  ivthALT  35268  neibastop2  35294  fnemeet1  35299  fnejoin1  35301  pibt2  36346  poimirlem11  36547  poimirlem12  36548  poimirlem30  36566  ftc1cnnc  36608  sstotbnd  36691  ssbnd  36704  heibor1lem  36725  heiborlem3  36729  heibor  36737  lsmsat  37926  lssats  37930  lcvexchlem3  37954  lsatcvat3  37970  lkrscss  38016  lkrpssN  38081  pmod1i  38767  pclbtwnN  38816  pclunN  38817  pclss2polN  38840  pcl0N  38841  sspmaplubN  38844  paddunN  38846  pnonsingN  38852  pclfinclN  38869  osumcllem4N  38878  dia2dimlem13  39995  dvhopellsm  40036  dvadiaN  40047  dicelval1stN  40107  dicelval2nd  40108  dihssxp  40171  dihvalrel  40198  dochsscl  40287  dihoml4  40296  dochnoncon  40310  dvh3dim3N  40368  lcfrlem2  40462  lcfrlem5  40465  lcfr  40504  lcdlsp  40540  mapdsn  40560  mapdlsm  40583  mapdpglem1  40591  mapdindp0  40638  hlhilocv  40880  rntrclfvOAI  41477  ismrcd1  41484  ismrcd2  41485  coeq0i  41539  hbtlem6  41919  rgspnval  41958  iocinico  42009  omabs2  42130  naddwordnexlem4  42200  trclubNEW  42418  ntrk2imkb  42836  isotone1  42847  k0004ss3  42952  iccdifprioo  44277  limsupequzmptlem  44492  cncfuni  44650  cncfiooicclem1  44657  dvresntr  44682  itgsubsticclem  44739  fourierdlem42  44913  fourierdlem48  44918  fourierdlem49  44919  fourierdlem50  44920  qndenserrn  45063  prsal  45082  intsaluni  45093  sssalgen  45099  dfsalgen2  45105  sge0split  45173  ismeannd  45231  caragensspw  45273  caragendifcl  45278  carageniuncl  45287  caratheodorylem1  45290  hoicvrrex  45320  ovnssle  45325  ovn02  45332  ovnsubadd  45336  hoidmv1le  45358  ovnlecvr2  45374  ovncvr2  45375  isvonmbl  45402  vonmblss  45404  ovolval4lem2  45414  ovnovollem1  45420  ovnovollem2  45421  incsmf  45506  decsmf  45531  uspgropssxp  46570  subsubmgm  46615  subsubrng  46790  mreuniss  47580  restcls2lem  47593  restcls2  47594  cnneiima  47597