Theorem sseqtrd 4006

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

Syntax hints:   → wi 4   = wceq 1533   ⊆ wss 3935

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-in 3942  df-ss 3951

This theorem is referenced by:  sseqtrrd  4007  uniintsn  4905  fssdmd  6523  oeeui  8222  nnaword2  8250  oaabs2  8266  erssxp  8306  fipwuni  8884  cantnflem3  9148  ficardun2  9619  ackbij1lem12  9647  ackbij1b  9655  fin1a2lem13  9828  winafp  10113  ioodisj  12862  reltrclfv  14371  prodss  15295  mrcssv  16879  mrcsscl  16885  mrcuni  16886  mressmrcd  16892  mreexexlem2d  16910  mreexexlem3d  16911  mreexfidimd  16915  subcss2  17107  resssetc  17346  funcsetcres2  17347  estrres  17383  poslubdg  17753  ipodrsfi  17767  acsmap2d  17783  mrelatlub  17790  mreclatBAD  17791  subsubm  17975  subsubg  18296  trivsubgd  18299  trivnsgd  18318  oppglsm  18761  subglsm  18793  lsmdisj  18801  gsumval3  19021  dprdres  19144  dprdss  19145  dprd2da  19158  dmdprdsplit2lem  19161  ablfac1b  19186  pgpfac1lem3  19193  issubdrg  19554  subsubrg  19555  islssd  19701  lspun  19753  lspssp  19754  lsslsp  19781  lsmssspx  19854  lspabs2  19886  lspabs3  19887  lspsolvlem  19908  lbsextlem3  19926  mplbas2  20245  gsumply1subr  20396  qsssubdrg  20598  obselocv  20866  lsslindf  20968  tgcl  21571  basgen  21590  tgfiss  21593  bastop1  21595  bastop2  21596  clsss2  21674  elcls3  21685  topssnei  21726  neiptopnei  21734  neitr  21782  restcls  21783  restlp  21785  ordtrest2  21806  iscncl  21871  cncls2  21875  cncls  21876  cnntr  21877  lmcls  21904  tgcmp  22003  cmpcld  22004  uncmp  22005  hauscmplem  22008  cmpfi  22010  clsconn  22032  2ndcsb  22051  2ndcctbss  22057  2ndcomap  22060  nllyrest  22088  1stckgenlem  22155  kgencn2  22159  kgen2cn  22161  ptbasfi  22183  txcld  22205  txcls  22206  txbasval  22208  neitx  22209  ptcld  22215  ptclsg  22217  txnlly  22239  hausdiag  22247  txkgen  22254  xkopt  22257  xkopjcn  22258  xkococnlem  22261  cnmpt1res  22278  cnmpt2res  22279  imasnopn  22292  imasncld  22293  imasncls  22294  qtopcld  22315  qtoprest  22319  qtopcmap  22321  kqcldsat  22335  kqreglem2  22344  kqnrmlem2  22346  hmeontr  22371  neifil  22482  fgtr  22492  trnei  22494  uffixfr  22525  uffix2  22526  uffixsn  22527  elflim  22573  flimclslem  22586  fclsopn  22616  fclscmpi  22631  fclscmp  22632  alexsubALTlem3  22651  alexsubALT  22653  ptcmplem3  22656  subgntr  22709  opnsubg  22710  clssubg  22711  clsnsg  22712  cldsubg  22713  tgpconncompeqg  22714  snclseqg  22718  tsmsgsum  22741  tsmsid  22742  tgptsmscld  22753  ustssco  22817  utop2nei  22853  utop3cls  22854  utopreg  22855  cnextucn  22906  ressprdsds  22975  lpbl  23107  met2ndci  23126  prdsxmslem2  23133  metustexhalf  23160  psmetutop  23171  tgioo  23398  metdstri  23453  metdseq0  23456  xlebnum  23563  clsocv  23847  metelcls  23902  metsscmetcld  23912  cmetss  23913  relcmpcmet  23915  cmpcmet  23916  minveclem4a  24027  uniioovol  24174  uniioombllem3  24180  limcres  24478  dvbss  24493  perfdvf  24495  dvreslem  24501  dvres2lem  24502  dvcnp2  24511  dvaddbr  24529  dvmulbr  24530  dvcmulf  24536  dvcj  24541  dvnfre  24543  dvmptres2  24553  dvmptcmul  24555  dvmptntr  24562  dvlip2  24586  dvcnvrelem2  24609  ftc1cn  24634  dvntaylp  24953  taylthlem1  24955  ulmdvlem3  24984  pserulm  25004  shsub2  29096  spanssoc  29120  shub2  29154  ococin  29179  ssjo  29218  chub2  29279  spanpr  29351  elnlfn  29699  mdslj1i  30090  mdslmd3i  30103  mdexchi  30106  chirredlem1  30161  atcvat3i  30167  mdsymlem1  30174  mdsymlem5  30178  imadifxp  30345  fnpreimac  30410  suppovss  30420  symgcom2  30723  pmtrcnelor  30730  cycpmco2f1  30761  drgextlsp  30991  lvecdim0  31000  lbslsat  31009  dimkerim  31018  fedgmullem2  31021  fedgmul  31022  qtophaus  31095  locfinreflem  31099  fsumcvg4  31188  esum2d  31347  omsmon  31551  omssubadd  31553  carsgclctun  31574  sitgclg  31595  eulerpartlemgf  31632  reprpmtf1o  31892  cvmscld  32515  cvmliftmolem1  32523  cvmlift2lem9  32553  cvmlift2lem11  32555  cvmlift3lem6  32566  nodense  33191  opnregcld  33673  ivthALT  33678  neibastop2  33704  fnemeet1  33709  fnejoin1  33711  pibt2  34692  poimirlem11  34897  poimirlem12  34898  poimirlem30  34916  ftc1cnnc  34960  sstotbnd  35047  ssbnd  35060  heibor1lem  35081  heiborlem3  35085  heibor  35093  lsmsat  36138  lssats  36142  lcvexchlem3  36166  lsatcvat3  36182  lkrscss  36228  lkrpssN  36293  pmod1i  36978  pclbtwnN  37027  pclunN  37028  pclss2polN  37051  pcl0N  37052  sspmaplubN  37055  paddunN  37057  pnonsingN  37063  pclfinclN  37080  osumcllem4N  37089  dia2dimlem13  38206  dvhopellsm  38247  dvadiaN  38258  dicelval1stN  38318  dicelval2nd  38319  dihssxp  38382  dihvalrel  38409  dochsscl  38498  dihoml4  38507  dochnoncon  38521  dvh3dim3N  38579  lcfrlem2  38673  lcfrlem5  38676  lcfr  38715  lcdlsp  38751  mapdsn  38771  mapdlsm  38794  mapdpglem1  38802  mapdindp0  38849  hlhilocv  39087  rntrclfvOAI  39281  ismrcd1  39288  ismrcd2  39289  coeq0i  39343  hbtlem6  39722  rgspnval  39761  iocinico  39811  trclubNEW  39972  ntrk2imkb  40380  isotone1  40391  k0004ss3  40496  iccdifprioo  41785  limsupequzmptlem  42002  cncfuni  42162  cncfiooicclem1  42169  dvresntr  42195  dvmptresicc  42197  itgsubsticclem  42253  fourierdlem42  42428  fourierdlem48  42433  fourierdlem49  42434  fourierdlem50  42435  qndenserrn  42578  prsal  42597  intsaluni  42606  sssalgen  42612  dfsalgen2  42618  sge0split  42685  ismeannd  42743  caragensspw  42785  caragendifcl  42790  carageniuncl  42799  caratheodorylem1  42802  hoicvrrex  42832  ovnssle  42837  ovn02  42844  ovnsubadd  42848  hoidmv1le  42870  ovnlecvr2  42886  ovncvr2  42887  isvonmbl  42914  vonmblss  42916  ovolval4lem2  42926  ovnovollem1  42932  ovnovollem2  42933  incsmf  43013  decsmf  43037  uspgropssxp  44013  subsubmgm  44058