Theorem sseqtrd 3934

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

Syntax hints:   → wi 4   = wceq 1538   ⊆ wss 3860

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2729

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-v 3411  df-in 3867  df-ss 3877

This theorem is referenced by:  sseqtrrd  3935  uniintsn  4880  fssdmd  6518  oeeui  8243  nnaword2  8271  oaabs2  8287  erssxp  8327  fipwuni  8928  cantnflem3  9192  ficardun2  9667  ficardun2OLD  9668  ackbij1lem12  9696  ackbij1b  9704  fin1a2lem13  9877  winafp  10162  ioodisj  12919  reltrclfv  14429  prodss  15354  mrcssv  16948  mrcsscl  16954  mrcuni  16955  mressmrcd  16961  mreexexlem2d  16979  mreexexlem3d  16980  mreexfidimd  16984  subcss2  17177  resssetc  17423  funcsetcres2  17424  estrres  17460  poslubdg  17830  ipodrsfi  17844  acsmap2d  17860  mrelatlub  17867  mreclatBAD  17868  subsubm  18052  subsubg  18374  trivsubgd  18377  trivnsgd  18396  oppglsm  18839  subglsm  18871  lsmdisj  18879  gsumval3  19100  dprdres  19223  dprdss  19224  dprd2da  19237  dmdprdsplit2lem  19240  ablfac1b  19265  pgpfac1lem3  19272  issubdrg  19633  subsubrg  19634  islssd  19780  lspun  19832  lspssp  19833  lsslsp  19860  lsmssspx  19933  lspabs2  19965  lspabs3  19966  lspsolvlem  19987  lbsextlem3  20005  qsssubdrg  20230  obselocv  20498  lsslindf  20600  mplbas2  20807  gsumply1subr  20963  tgcl  21674  basgen  21693  tgfiss  21696  bastop1  21698  bastop2  21699  clsss2  21777  elcls3  21788  topssnei  21829  neiptopnei  21837  neitr  21885  restcls  21886  restlp  21888  ordtrest2  21909  iscncl  21974  cncls2  21978  cncls  21979  cnntr  21980  lmcls  22007  tgcmp  22106  cmpcld  22107  uncmp  22108  hauscmplem  22111  cmpfi  22113  clsconn  22135  2ndcsb  22154  2ndcctbss  22160  2ndcomap  22163  nllyrest  22191  1stckgenlem  22258  kgencn2  22262  kgen2cn  22264  ptbasfi  22286  txcld  22308  txcls  22309  txbasval  22311  neitx  22312  ptcld  22318  ptclsg  22320  txnlly  22342  hausdiag  22350  txkgen  22357  xkopt  22360  xkopjcn  22361  xkococnlem  22364  cnmpt1res  22381  cnmpt2res  22382  imasnopn  22395  imasncld  22396  imasncls  22397  qtopcld  22418  qtoprest  22422  qtopcmap  22424  kqcldsat  22438  kqreglem2  22447  kqnrmlem2  22449  hmeontr  22474  neifil  22585  fgtr  22595  trnei  22597  uffixfr  22628  uffix2  22629  uffixsn  22630  elflim  22676  flimclslem  22689  fclsopn  22719  fclscmpi  22734  fclscmp  22735  alexsubALTlem3  22754  alexsubALT  22756  ptcmplem3  22759  subgntr  22812  opnsubg  22813  clssubg  22814  clsnsg  22815  cldsubg  22816  tgpconncompeqg  22817  snclseqg  22821  tsmsgsum  22844  tsmsid  22845  tgptsmscld  22856  ustssco  22920  utop2nei  22956  utop3cls  22957  utopreg  22958  cnextucn  23009  ressprdsds  23078  lpbl  23210  met2ndci  23229  prdsxmslem2  23236  metustexhalf  23263  psmetutop  23274  tgioo  23502  metdstri  23557  metdseq0  23560  xlebnum  23671  clsocv  23955  metelcls  24010  metsscmetcld  24020  cmetss  24021  relcmpcmet  24023  cmpcmet  24024  minveclem4a  24135  uniioovol  24284  uniioombllem3  24290  limcres  24590  dvbss  24605  perfdvf  24607  dvreslem  24613  dvres2lem  24614  dvmptresicc  24620  dvcnp2  24624  dvaddbr  24642  dvmulbr  24643  dvcmulf  24649  dvcj  24654  dvnfre  24656  dvmptres2  24666  dvmptcmul  24668  dvmptntr  24675  dvlip2  24699  dvcnvrelem2  24722  ftc1cn  24747  dvntaylp  25070  taylthlem1  25072  ulmdvlem3  25101  pserulm  25121  shsub2  29212  spanssoc  29236  shub2  29270  ococin  29295  ssjo  29334  chub2  29395  spanpr  29467  elnlfn  29815  mdslj1i  30206  mdslmd3i  30219  mdexchi  30222  chirredlem1  30277  atcvat3i  30283  mdsymlem1  30290  mdsymlem5  30294  imadifxp  30467  fnpreimac  30536  suppovss  30545  symgcom2  30883  pmtrcnelor  30890  cycpmco2f1  30921  0ringidl  31130  elrspunidl  31131  0ringprmidl  31150  idlsrgmulrss1  31181  idlsrgmulrss2  31182  drgextlsp  31206  lvecdim0  31215  lbslsat  31224  dimkerim  31233  fedgmullem2  31236  fedgmul  31237  qtophaus  31311  locfinreflem  31315  rspecbas  31340  zarclssn  31348  zarmxt1  31355  zarcmplem  31356  fsumcvg4  31425  esum2d  31584  omsmon  31788  omssubadd  31790  carsgclctun  31811  sitgclg  31832  eulerpartlemgf  31869  reprpmtf1o  32129  cvmscld  32755  cvmliftmolem1  32763  cvmlift2lem9  32793  cvmlift2lem11  32795  cvmlift3lem6  32806  nodense  33484  opnregcld  34094  ivthALT  34099  neibastop2  34125  fnemeet1  34130  fnejoin1  34132  pibt2  35140  poimirlem11  35374  poimirlem12  35375  poimirlem30  35393  ftc1cnnc  35435  sstotbnd  35519  ssbnd  35532  heibor1lem  35553  heiborlem3  35557  heibor  35565  lsmsat  36610  lssats  36614  lcvexchlem3  36638  lsatcvat3  36654  lkrscss  36700  lkrpssN  36765  pmod1i  37450  pclbtwnN  37499  pclunN  37500  pclss2polN  37523  pcl0N  37524  sspmaplubN  37527  paddunN  37529  pnonsingN  37535  pclfinclN  37552  osumcllem4N  37561  dia2dimlem13  38678  dvhopellsm  38719  dvadiaN  38730  dicelval1stN  38790  dicelval2nd  38791  dihssxp  38854  dihvalrel  38881  dochsscl  38970  dihoml4  38979  dochnoncon  38993  dvh3dim3N  39051  lcfrlem2  39145  lcfrlem5  39148  lcfr  39187  lcdlsp  39223  mapdsn  39243  mapdlsm  39266  mapdpglem1  39274  mapdindp0  39321  hlhilocv  39559  rntrclfvOAI  40033  ismrcd1  40040  ismrcd2  40041  coeq0i  40095  hbtlem6  40474  rgspnval  40513  iocinico  40563  trclubNEW  40720  ntrk2imkb  41141  isotone1  41152  k0004ss3  41257  iccdifprioo  42547  limsupequzmptlem  42764  cncfuni  42922  cncfiooicclem1  42929  dvresntr  42954  itgsubsticclem  43011  fourierdlem42  43185  fourierdlem48  43190  fourierdlem49  43191  fourierdlem50  43192  qndenserrn  43335  prsal  43354  intsaluni  43363  sssalgen  43369  dfsalgen2  43375  sge0split  43442  ismeannd  43500  caragensspw  43542  caragendifcl  43547  carageniuncl  43556  caratheodorylem1  43559  hoicvrrex  43589  ovnssle  43594  ovn02  43601  ovnsubadd  43605  hoidmv1le  43627  ovnlecvr2  43643  ovncvr2  43644  isvonmbl  43671  vonmblss  43673  ovolval4lem2  43683  ovnovollem1  43689  ovnovollem2  43690  incsmf  43770  decsmf  43794  uspgropssxp  44767  subsubmgm  44812  restcls2lem  45624  restcls2  45625  cnneiima  45628