Theorem sseqtrd 3967

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

Syntax hints:   → wi 4   = wceq 1541   ⊆ wss 3898

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2725  df-ss 3915

This theorem is referenced by:  sseqtrrd  3968  sseqtrid  3973  3sstr3d  3985  uniintsn  4937  fssdmd  6676  oeeui  8525  nnaword2  8553  oaabs2  8572  naddword2  8615  erssxp  8653  fipwuni  9319  cantnflem3  9590  ficardun2  10102  ackbij1lem12  10130  ackbij1b  10138  fin1a2lem13  10312  winafp  10597  ioodisj  13386  reltrclfv  14928  prodss  15858  mrcssv  17524  mrcsscl  17530  mrcuni  17531  mressmrcd  17537  mreexexlem2d  17555  mreexexlem3d  17556  mreexfidimd  17560  subcss2  17754  resssetc  18003  funcsetcres2  18004  estrres  18049  poslubdg  18322  ipodrsfi  18449  acsmap2d  18465  mrelatlub  18472  mreclatBAD  18473  subsubmgm  18622  subsubm  18728  subsubg  19066  trivsubgd  19069  trivnsgd  19088  oppglsm  19558  subglsm  19589  lsmdisj  19597  gsumval3  19823  dprdres  19946  dprdss  19947  dprd2da  19960  dmdprdsplit2lem  19963  ablfac1b  19988  pgpfac1lem3  19995  subsubrng  20482  subsubrg  20517  rgspnval  20531  issubdrg  20699  islssd  20872  lspun  20924  lspssp  20925  lsslsp  20952  lsslspOLD  20953  lsmssspx  21026  lspabs2  21061  lspabs3  21062  lspsolvlem  21083  lbsextlem3  21101  qsssubdrg  21367  obselocv  21669  lsslindf  21771  sraassa  21810  mplbas2  21980  gsumply1subr  22149  tgcl  22887  basgen  22906  tgfiss  22909  bastop1  22911  bastop2  22912  clsss2  22990  elcls3  23001  topssnei  23042  neiptopnei  23050  neitr  23098  restcls  23099  restlp  23101  ordtrest2  23122  iscncl  23187  cncls2  23191  cncls  23192  cnntr  23193  lmcls  23220  tgcmp  23319  cmpcld  23320  uncmp  23321  hauscmplem  23324  cmpfi  23326  clsconn  23348  2ndcsb  23367  2ndcctbss  23373  2ndcomap  23376  nllyrest  23404  1stckgenlem  23471  kgencn2  23475  kgen2cn  23477  ptbasfi  23499  txcld  23521  txcls  23522  txbasval  23524  neitx  23525  ptcld  23531  ptclsg  23533  txnlly  23555  hausdiag  23563  txkgen  23570  xkopt  23573  xkopjcn  23574  xkococnlem  23577  cnmpt1res  23594  cnmpt2res  23595  imasnopn  23608  imasncld  23609  imasncls  23610  qtopcld  23631  qtoprest  23635  qtopcmap  23637  kqcldsat  23651  kqreglem2  23660  kqnrmlem2  23662  hmeontr  23687  neifil  23798  fgtr  23808  trnei  23810  uffixfr  23841  uffix2  23842  uffixsn  23843  elflim  23889  flimclslem  23902  fclsopn  23932  fclscmpi  23947  fclscmp  23948  alexsubALTlem3  23967  alexsubALT  23969  ptcmplem3  23972  subgntr  24025  opnsubg  24026  clssubg  24027  clsnsg  24028  cldsubg  24029  tgpconncompeqg  24030  snclseqg  24034  tsmsgsum  24057  tsmsid  24058  tgptsmscld  24069  ustssco  24133  utop2nei  24168  utop3cls  24169  utopreg  24170  cnextucn  24220  ressprdsds  24289  lpbl  24421  met2ndci  24440  prdsxmslem2  24447  metustexhalf  24474  psmetutop  24485  tgioo  24714  metdstri  24770  metdseq0  24773  xlebnum  24894  clsocv  25180  metelcls  25235  metsscmetcld  25245  cmetss  25246  relcmpcmet  25248  cmpcmet  25249  minveclem4a  25360  uniioovol  25510  uniioombllem3  25516  limcres  25817  dvbss  25832  perfdvf  25834  dvreslem  25840  dvres2lem  25841  dvmptresicc  25847  dvcnp2  25851  dvcnp2OLD  25852  dvaddbr  25870  dvmulbr  25871  dvmulbrOLD  25872  dvcmulf  25878  dvcj  25884  dvnfre  25886  dvmptres2  25896  dvmptcmul  25898  dvmptntr  25905  dvlip2  25930  dvcnvrelem2  25953  ftc1cn  25980  dvntaylp  26309  taylthlem1  26311  ulmdvlem3  26341  pserulm  26361  nodense  27634  mulsproplem13  28070  mulsproplem14  28071  shsub2  31309  spanssoc  31333  shub2  31367  ococin  31392  ssjo  31431  chub2  31492  spanpr  31564  elnlfn  31912  mdslj1i  32303  mdslmd3i  32316  mdexchi  32319  chirredlem1  32374  atcvat3i  32380  mdsymlem1  32387  mdsymlem5  32391  imadifxp  32585  fnpreimac  32657  suppovss  32668  symgcom2  33062  pmtrcnelor  33069  cycpmco2f1  33102  0ringsubrg  33227  erlval  33234  1fldgenq  33297  0ringidl  33395  elrspunidl  33402  0ringprmidl  33423  drngmxidl  33451  drngmxidlr  33452  idlsrgmulrss1  33485  idlsrgmulrss2  33486  1arithidomlem2  33510  ply1dg3rt0irred  33555  resssra  33622  lsssra  33623  drgextlsp  33629  lvecdim0  33642  lbslsat  33652  dimkerim  33663  fedgmullem2  33666  fedgmul  33667  fldgenfldext  33704  fldextrspunlsplem  33709  fldextrspunlsp  33710  fldextrspunlem1  33711  fldextrspunfld  33712  fldextrspundgdvdslem  33716  fldextrspundgdvds  33717  algextdeglem3  33755  algextdeglem4  33756  qtophaus  33872  locfinreflem  33876  rspecbas  33901  zarclssn  33909  zarmxt1  33916  zarcmplem  33917  fsumcvg4  33986  esum2d  34129  omsmon  34334  omssubadd  34336  carsgclctun  34357  sitgclg  34378  eulerpartlemgf  34415  reprpmtf1o  34662  cvmscld  35340  cvmliftmolem1  35348  cvmlift2lem9  35378  cvmlift2lem11  35380  cvmlift3lem6  35391  opnregcld  36397  ivthALT  36402  neibastop2  36428  fnemeet1  36433  fnejoin1  36435  pibt2  37484  poimirlem11  37694  poimirlem12  37695  poimirlem30  37713  ftc1cnnc  37755  sstotbnd  37838  ssbnd  37851  heibor1lem  37872  heiborlem3  37876  heibor  37884  lsmsat  39130  lssats  39134  lcvexchlem3  39158  lsatcvat3  39174  lkrscss  39220  lkrpssN  39285  pmod1i  39970  pclbtwnN  40019  pclunN  40020  pclss2polN  40043  pcl0N  40044  sspmaplubN  40047  paddunN  40049  pnonsingN  40055  pclfinclN  40072  osumcllem4N  40081  dia2dimlem13  41198  dvhopellsm  41239  dvadiaN  41250  dicelval1stN  41310  dicelval2nd  41311  dihssxp  41374  dihvalrel  41401  dochsscl  41490  dihoml4  41499  dochnoncon  41513  dvh3dim3N  41571  lcfrlem2  41665  lcfrlem5  41668  lcfr  41707  lcdlsp  41743  mapdsn  41763  mapdlsm  41786  mapdpglem1  41794  mapdindp0  41841  hlhilocv  42079  primrootscoprbij  42218  rntrclfvOAI  42811  ismrcd1  42818  ismrcd2  42819  coeq0i  42873  hbtlem6  43249  iocinico  43332  omabs2  43452  naddwordnexlem4  43521  trclubNEW  43739  ntrk2imkb  44157  isotone1  44168  k0004ss3  44273  iccdifprioo  45643  limsupequzmptlem  45853  cncfuni  46011  cncfiooicclem1  46018  dvresntr  46043  itgsubsticclem  46100  fourierdlem42  46274  fourierdlem48  46279  fourierdlem49  46280  fourierdlem50  46281  qndenserrn  46424  prsal  46443  intsaluni  46454  sssalgen  46460  dfsalgen2  46466  sge0split  46534  ismeannd  46592  caragensspw  46634  caragendifcl  46639  carageniuncl  46648  caratheodorylem1  46651  hoicvrrex  46681  ovnssle  46686  ovn02  46693  ovnsubadd  46697  hoidmv1le  46719  ovnlecvr2  46735  ovncvr2  46736  isvonmbl  46763  vonmblss  46765  ovolval4lem2  46775  ovnovollem1  46781  ovnovollem2  46782  incsmf  46867  decsmf  46892  uspgropssxp  48271  mreuniss  49027  restcls2lem  49040  restcls2  49041  cnneiima  49044  imassc  49281