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  27584  mulsproplem14  27585  shsub2  30578  spanssoc  30602  shub2  30636  ococin  30661  ssjo  30700  chub2  30761  spanpr  30833  elnlfn  31181  mdslj1i  31572  mdslmd3i  31585  mdexchi  31588  chirredlem1  31643  atcvat3i  31649  mdsymlem1  31656  mdsymlem5  31660  imadifxp  31832  fnpreimac  31896  suppovss  31906  symgcom2  32245  pmtrcnelor  32252  cycpmco2f1  32283  0ringsubrg  32379  1fldgenq  32412  0ringidl  32539  elrspunidl  32546  0ringprmidl  32568  drngmxidl  32593  idlsrgmulrss1  32625  idlsrgmulrss2  32626  drgextlsp  32681  lvecdim0  32691  lbslsat  32701  dimkerim  32712  fedgmullem2  32715  fedgmul  32716  algextdeglem1  32772  qtophaus  32816  locfinreflem  32820  rspecbas  32845  zarclssn  32853  zarmxt1  32860  zarcmplem  32861  fsumcvg4  32930  esum2d  33091  omsmon  33297  omssubadd  33299  carsgclctun  33320  sitgclg  33341  eulerpartlemgf  33378  reprpmtf1o  33638  cvmscld  34264  cvmliftmolem1  34272  cvmlift2lem9  34302  cvmlift2lem11  34304  cvmlift3lem6  34315  gg-dvcnp2  35174  gg-dvmulbr  35175  opnregcld  35215  ivthALT  35220  neibastop2  35246  fnemeet1  35251  fnejoin1  35253  pibt2  36298  poimirlem11  36499  poimirlem12  36500  poimirlem30  36518  ftc1cnnc  36560  sstotbnd  36643  ssbnd  36656  heibor1lem  36677  heiborlem3  36681  heibor  36689  lsmsat  37878  lssats  37882  lcvexchlem3  37906  lsatcvat3  37922  lkrscss  37968  lkrpssN  38033  pmod1i  38719  pclbtwnN  38768  pclunN  38769  pclss2polN  38792  pcl0N  38793  sspmaplubN  38796  paddunN  38798  pnonsingN  38804  pclfinclN  38821  osumcllem4N  38830  dia2dimlem13  39947  dvhopellsm  39988  dvadiaN  39999  dicelval1stN  40059  dicelval2nd  40060  dihssxp  40123  dihvalrel  40150  dochsscl  40239  dihoml4  40248  dochnoncon  40262  dvh3dim3N  40320  lcfrlem2  40414  lcfrlem5  40417  lcfr  40456  lcdlsp  40492  mapdsn  40512  mapdlsm  40535  mapdpglem1  40543  mapdindp0  40590  hlhilocv  40832  rntrclfvOAI  41429  ismrcd1  41436  ismrcd2  41437  coeq0i  41491  hbtlem6  41871  rgspnval  41910  iocinico  41961  omabs2  42082  naddwordnexlem4  42152  trclubNEW  42370  ntrk2imkb  42788  isotone1  42799  k0004ss3  42904  iccdifprioo  44229  limsupequzmptlem  44444  cncfuni  44602  cncfiooicclem1  44609  dvresntr  44634  itgsubsticclem  44691  fourierdlem42  44865  fourierdlem48  44870  fourierdlem49  44871  fourierdlem50  44872  qndenserrn  45015  prsal  45034  intsaluni  45045  sssalgen  45051  dfsalgen2  45057  sge0split  45125  ismeannd  45183  caragensspw  45225  caragendifcl  45230  carageniuncl  45239  caratheodorylem1  45242  hoicvrrex  45272  ovnssle  45277  ovn02  45284  ovnsubadd  45288  hoidmv1le  45310  ovnlecvr2  45326  ovncvr2  45327  isvonmbl  45354  vonmblss  45356  ovolval4lem2  45366  ovnovollem1  45372  ovnovollem2  45373  incsmf  45458  decsmf  45483  uspgropssxp  46522  subsubmgm  46567  subsubrng  46742  mreuniss  47532  restcls2lem  47545  restcls2  47546  cnneiima  47549