Theorem sseqtrd 3958

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

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

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 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2728  df-ss 3906

This theorem is referenced by:  sseqtrrd  3959  sseqtrid  3964  3sstr3d  3976  uniintsn  4927  fssdmd  6686  oeeui  8538  nnaword2  8566  oaabs2  8585  naddword2  8628  erssxp  8667  fipwuni  9339  cantnflem3  9612  ficardun2  10124  ackbij1lem12  10152  ackbij1b  10160  fin1a2lem13  10334  winafp  10620  ioodisj  13435  reltrclfv  14979  prodss  15912  mrcssv  17580  mrcsscl  17586  mrcuni  17587  mressmrcd  17593  mreexexlem2d  17611  mreexexlem3d  17612  mreexfidimd  17616  subcss2  17810  resssetc  18059  funcsetcres2  18060  estrres  18105  poslubdg  18378  ipodrsfi  18505  acsmap2d  18521  mrelatlub  18528  mreclatBAD  18529  subsubmgm  18678  subsubm  18784  subsubg  19125  trivsubgd  19128  trivnsgd  19147  oppglsm  19617  subglsm  19648  lsmdisj  19656  gsumval3  19882  dprdres  20005  dprdss  20006  dprd2da  20019  dmdprdsplit2lem  20022  ablfac1b  20047  pgpfac1lem3  20054  subsubrng  20540  subsubrg  20575  rgspnval  20589  issubdrg  20757  islssd  20930  lspun  20982  lspssp  20983  lsslsp  21010  lsmssspx  21083  lspabs2  21118  lspabs3  21119  lspsolvlem  21140  lbsextlem3  21158  qsssubdrg  21406  obselocv  21708  lsslindf  21810  sraassa  21849  mplbas2  22020  gsumply1subr  22197  tgcl  22934  basgen  22953  tgfiss  22956  bastop1  22958  bastop2  22959  clsss2  23037  elcls3  23048  topssnei  23089  neiptopnei  23097  neitr  23145  restcls  23146  restlp  23148  ordtrest2  23169  iscncl  23234  cncls2  23238  cncls  23239  cnntr  23240  lmcls  23267  tgcmp  23366  cmpcld  23367  uncmp  23368  hauscmplem  23371  cmpfi  23373  clsconn  23395  2ndcsb  23414  2ndcctbss  23420  2ndcomap  23423  nllyrest  23451  1stckgenlem  23518  kgencn2  23522  kgen2cn  23524  ptbasfi  23546  txcld  23568  txcls  23569  txbasval  23571  neitx  23572  ptcld  23578  ptclsg  23580  txnlly  23602  hausdiag  23610  txkgen  23617  xkopt  23620  xkopjcn  23621  xkococnlem  23624  cnmpt1res  23641  cnmpt2res  23642  imasnopn  23655  imasncld  23656  imasncls  23657  qtopcld  23678  qtoprest  23682  qtopcmap  23684  kqcldsat  23698  kqreglem2  23707  kqnrmlem2  23709  hmeontr  23734  neifil  23845  fgtr  23855  trnei  23857  uffixfr  23888  uffix2  23889  uffixsn  23890  elflim  23936  flimclslem  23949  fclsopn  23979  fclscmpi  23994  fclscmp  23995  alexsubALTlem3  24014  alexsubALT  24016  ptcmplem3  24019  subgntr  24072  opnsubg  24073  clssubg  24074  clsnsg  24075  cldsubg  24076  tgpconncompeqg  24077  snclseqg  24081  tsmsgsum  24104  tsmsid  24105  tgptsmscld  24116  ustssco  24180  utop2nei  24215  utop3cls  24216  utopreg  24217  cnextucn  24267  ressprdsds  24336  lpbl  24468  met2ndci  24487  prdsxmslem2  24494  metustexhalf  24521  psmetutop  24532  tgioo  24761  metdstri  24817  metdseq0  24820  xlebnum  24932  clsocv  25217  metelcls  25272  metsscmetcld  25282  cmetss  25283  relcmpcmet  25285  cmpcmet  25286  minveclem4a  25397  uniioovol  25546  uniioombllem3  25552  limcres  25853  dvbss  25868  perfdvf  25870  dvreslem  25876  dvres2lem  25877  dvmptresicc  25883  dvcnp2  25887  dvaddbr  25905  dvmulbr  25906  dvcmulf  25912  dvcj  25917  dvnfre  25919  dvmptres2  25929  dvmptcmul  25931  dvmptntr  25938  dvlip2  25962  dvcnvrelem2  25985  ftc1cn  26010  dvntaylp  26336  taylthlem1  26338  ulmdvlem3  26367  pserulm  26387  nodense  27656  mulsproplem13  28120  mulsproplem14  28121  onsbnd  28273  shsub2  31396  spanssoc  31420  shub2  31454  ococin  31479  ssjo  31518  chub2  31579  spanpr  31651  elnlfn  31999  mdslj1i  32390  mdslmd3i  32403  mdexchi  32406  chirredlem1  32461  atcvat3i  32467  mdsymlem1  32474  mdsymlem5  32478  imadifxp  32671  fnpreimac  32743  suppovss  32754  symgcom2  33145  pmtrcnelor  33152  cycpmco2f1  33185  0ringsubrg  33312  erlval  33319  1fldgenq  33383  0ringidl  33481  elrspunidl  33488  0ringprmidl  33509  drngmxidl  33537  drngmxidlr  33538  idlsrgmulrss1  33571  idlsrgmulrss2  33572  1arithidomlem2  33596  ply1dg3rt0irred  33644  resssra  33731  lsssra  33732  drgextlsp  33738  lvecdim0  33751  lbslsat  33760  dimkerim  33771  fedgmullem2  33774  fedgmul  33775  fldgenfldext  33812  fldextrspunlsplem  33817  fldextrspunlsp  33818  fldextrspunlem1  33819  fldextrspunfld  33820  fldextrspundgdvdslem  33824  fldextrspundgdvds  33825  algextdeglem3  33863  algextdeglem4  33864  qtophaus  33980  locfinreflem  33984  rspecbas  34009  zarclssn  34017  zarmxt1  34024  zarcmplem  34025  fsumcvg4  34094  esum2d  34237  omsmon  34442  omssubadd  34444  carsgclctun  34465  sitgclg  34486  eulerpartlemgf  34523  reprpmtf1o  34770  cvmscld  35455  cvmliftmolem1  35463  cvmlift2lem9  35493  cvmlift2lem11  35495  cvmlift3lem6  35506  opnregcld  36512  ivthALT  36517  neibastop2  36543  fnemeet1  36548  fnejoin1  36550  pibt2  37733  poimirlem11  37952  poimirlem12  37953  poimirlem30  37971  ftc1cnnc  38013  sstotbnd  38096  ssbnd  38109  heibor1lem  38130  heiborlem3  38134  heibor  38142  lsmsat  39454  lssats  39458  lcvexchlem3  39482  lsatcvat3  39498  lkrscss  39544  lkrpssN  39609  pmod1i  40294  pclbtwnN  40343  pclunN  40344  pclss2polN  40367  pcl0N  40368  sspmaplubN  40371  paddunN  40373  pnonsingN  40379  pclfinclN  40396  osumcllem4N  40405  dia2dimlem13  41522  dvhopellsm  41563  dvadiaN  41574  dicelval1stN  41634  dicelval2nd  41635  dihssxp  41698  dihvalrel  41725  dochsscl  41814  dihoml4  41823  dochnoncon  41837  dvh3dim3N  41895  lcfrlem2  41989  lcfrlem5  41992  lcfr  42031  lcdlsp  42067  mapdsn  42087  mapdlsm  42110  mapdpglem1  42118  mapdindp0  42165  hlhilocv  42403  primrootscoprbij  42541  rntrclfvOAI  43123  ismrcd1  43130  ismrcd2  43131  coeq0i  43185  hbtlem6  43557  iocinico  43640  omabs2  43760  naddwordnexlem4  43829  trclubNEW  44046  ntrk2imkb  44464  isotone1  44475  k0004ss3  44580  iccdifprioo  45946  limsupequzmptlem  46156  cncfuni  46314  cncfiooicclem1  46321  dvresntr  46346  itgsubsticclem  46403  fourierdlem42  46577  fourierdlem48  46582  fourierdlem49  46583  fourierdlem50  46584  qndenserrn  46727  prsal  46746  intsaluni  46757  sssalgen  46763  dfsalgen2  46769  sge0split  46837  ismeannd  46895  caragensspw  46937  caragendifcl  46942  carageniuncl  46951  caratheodorylem1  46954  hoicvrrex  46984  ovnssle  46989  ovn02  46996  ovnsubadd  47000  hoidmv1le  47022  ovnlecvr2  47038  ovncvr2  47039  isvonmbl  47066  vonmblss  47068  ovolval4lem2  47078  ovnovollem1  47084  ovnovollem2  47085  incsmf  47170  decsmf  47195  uspgropssxp  48620  mreuniss  49375  restcls2lem  49388  restcls2  49389  cnneiima  49392  imassc  49628