Theorem sseqtrd 3949

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ⊆ wss 3900

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2755  df-ss 3901

This theorem is used by:  sseqtrrd  3950  sseqtrid  3955  3sstr3d  3967  uniintsn  4950  fssdmd  6758  oeeui  8649  nnaword2  8677  oaabs2  8696  naddword2  8740  erssxp  8779  fipwuni  9455  cantnflem3  9729  ficardun2  10319  ackbij1lem12  10347  ackbij1b  10355  fin1a2lem13  10529  winafp  10821  ioodisj  13653  reltrclfv  15213  prodss  16158  mrcssv  17838  mrcsscl  17844  mrcuni  17845  mressmrcd  17851  mreexexlem2d  17869  mreexexlem3d  17870  mreexfidimd  17874  subcss2  18068  resssetc  18317  funcsetcres2  18318  estrres  18363  poslubdg  18636  ipodrsfi  18763  acsmap2d  18779  mrelatlub  18786  mreclatBAD  18787  subsubmgm  18949  subsubm  19062  subsubg  19410  trivsubgd  19413  trivnsgd  19432  oppglsm  19907  subglsm  19938  lsmdisj  19946  gsumval3  20172  dprdres  20295  dprdss  20296  dprd2da  20309  dmdprdsplit2lem  20312  ablfac1b  20337  pgpfac1lem3  20344  subsubrng  20866  subsubrg  20901  rgspnval  20915  issubdrg  21088  islssd  21261  lspun  21313  lspssp  21314  lsslsp  21341  lsmssspx  21414  lspabs2  21449  lspabs3  21450  lspsolvlem  21471  lbsextlem3  21489  0ringidl  21565  0ringprmidl  21684  qsssubdrg  21786  obselocv  22089  lsslindf  22191  sraassa  22232  mplbas2  22406  gsumply1subr  22606  tgcl  23342  basgen  23361  tgfiss  23364  bastop1  23366  bastop2  23367  clsss2  23445  elcls3  23456  topssnei  23497  neiptopnei  23505  neitr  23553  restcls  23554  restlp  23556  ordtrest2  23577  iscncl  23642  cncls2  23646  cncls  23647  cnntr  23648  lmcls  23675  tgcmp  23774  cmpcld  23775  uncmp  23776  hauscmplem  23779  cmpfi  23781  clsconn  23803  2ndcsb  23822  2ndcctbss  23829  2ndcomap  23832  nllyrest  23860  1stckgenlem  23927  kgencn2  23931  kgen2cn  23933  ptbasfi  23955  txcld  23977  txcls  23978  txbasval  23980  neitx  23981  ptcld  23987  ptclsg  23989  txnlly  24011  hausdiag  24019  txkgen  24026  xkopt  24029  xkopjcn  24030  xkococnlem  24033  cnmpt1res  24050  cnmpt2res  24051  imasnopn  24064  imasncld  24065  imasncls  24066  qtopcld  24087  qtoprest  24091  qtopcmap  24093  kqcldsat  24107  kqreglem2  24116  kqnrmlem2  24118  hmeontr  24143  neifil  24254  fgtr  24264  trnei  24266  uffixfr  24297  uffix2  24298  uffixsn  24299  elflim  24345  flimclslem  24358  fclsopn  24388  fclscmpi  24403  fclscmp  24404  alexsubALTlem3  24423  alexsubALT  24425  ptcmplem3  24428  subgntr  24481  opnsubg  24482  clssubg  24483  clsnsg  24484  cldsubg  24485  tgpconncompeqg  24486  snclseqg  24490  tsmsgsum  24513  tsmsid  24514  tgptsmscld  24525  ustssco  24589  utop2nei  24624  utop3cls  24625  utopreg  24626  cnextucn  24676  ressprdsds  24745  lpbl  24877  met2ndci  24896  prdsxmslem2  24903  metustexhalf  24930  psmetutop  24941  tgioo  25170  metdstri  25226  metdseq0  25229  xlebnum  25341  clsocv  25626  metelcls  25681  metsscmetcld  25691  cmetss  25692  relcmpcmet  25694  cmpcmet  25695  minveclem4a  25806  uniioovol  25955  uniioombllem3  25961  limcres  26261  dvbss  26276  perfdvf  26278  dvreslem  26284  dvres2lem  26285  dvmptresicc  26291  dvcnp2  26295  dvaddbr  26313  dvmulbr  26314  dvcmulf  26320  dvcj  26325  dvnfre  26327  dvmptres2  26337  dvmptcmul  26339  dvmptntr  26346  dvlip2  26370  dvcnvrelem2  26393  ftc1cn  26418  dvntaylp  26755  taylthlem1  26757  ulmdvlem3  26786  pserulm  26806  nodense  28106  mulsproplem13  28571  mulsproplem14  28572  onsbnd  28724  prlnghpg  29481  shsub2  31984  spanssoc  32008  shub2  32042  ococin  32067  ssjo  32106  chub2  32167  spanpr  32239  elnlfn  32587  mdslj1i  32978  mdslmd3i  32991  mdexchi  32994  chirredlem1  33049  atcvat3i  33055  mdsymlem1  33062  mdsymlem5  33066  imadifxp  33293  fnpreimac  33362  suppovss  33371  symgcom2  33744  pmtrcnelor  33751  cycpmco2f1  33784  0ringsubrg  33911  erlval  33918  1fldgenq  33988  elrspunidl  34082  drngmxidl  34105  drngmxidlr  34106  idlsrgmulrss1  34147  idlsrgmulrss2  34148  1arithidomlem2  34172  ply1dg3rt0irred  34219  resssra  34330  lsssra  34331  drgextlsp  34337  lvecdim0  34350  lbslsat  34359  dimkerim  34370  fedgmullem2  34373  fedgmul  34374  fldgenfldext  34411  fldextrspunlsplem  34416  fldextrspunlsp  34417  fldextrspunlem1  34418  fldextrspunfld  34419  fldextrspundgdvdslem  34423  fldextrspundgdvds  34424  algextdeglem3  34462  algextdeglem4  34463  qtophaus  34579  locfinreflem  34583  rspecbas  34608  zarclssn  34616  zarmxt1  34623  zarcmplem  34624  fsumcvg4  34693  esum2d  34836  omsmon  35041  omssubadd  35043  carsgclctun  35064  sitgclg  35085  eulerpartlemgf  35122  reprpmtf1o  35366  maxssj0  36047  cvmscld  36246  cvmliftmolem1  36254  cvmlift2lem9  36284  cvmlift2lem11  36286  cvmlift3lem6  36297  nadddilem4  37187  opnregcld  37333  ivthALT  37338  neibastop2  37364  fnemeet1  37369  fnejoin1  37371  pibt2  38608  poimirlem11  38817  poimirlem12  38818  poimirlem30  38836  ftc1cnnc  38878  sstotbnd  38975  ssbnd  38988  heibor1lem  39009  heiborlem3  39013  heibor  39021  lsmsat  40331  lssats  40335  lcvexchlem3  40359  lsatcvat3  40375  lkrscss  40421  lkrpssN  40486  pmod1i  41171  pclbtwnN  41220  pclunN  41221  pclss2polN  41244  pcl0N  41245  sspmaplubN  41248  paddunN  41250  pnonsingN  41256  pclfinclN  41273  osumcllem4N  41282  dia2dimlem13  42399  dvhopellsm  42440  dvadiaN  42451  dicelval1stN  42511  dicelval2nd  42512  dihssxp  42575  dihvalrel  42602  dochsscl  42691  dihoml4  42700  dochnoncon  42714  dvh3dim3N  42772  lcfrlem2  42866  lcfrlem5  42869  lcfr  42908  lcdlsp  42944  mapdsn  42964  mapdlsm  42987  mapdpglem1  42995  mapdindp0  43042  hlhilocv  43280  primrootscoprbij  43418  rntrclfvOAI  43968  ismrcd1  43975  ismrcd2  43976  coeq0i  44030  hbtlem6  44396  iocinico  44475  omabs2  44595  naddwordnexlem4  44664  trclubNEW  44880  ntrk2imkb  45298  isotone1  45309  k0004ss3  45414  iccdifprioo  46801  limsupequzmptlem  47011  cncfuni  47169  cncfiooicclem1  47176  dvresntr  47201  itgsubsticclem  47258  fourierdlem42  47432  fourierdlem48  47437  fourierdlem49  47438  fourierdlem50  47439  qndenserrn  47582  prsal  47601  intsaluni  47612  sssalgen  47618  dfsalgen2  47624  sge0split  47692  ismeannd  47750  caragensspw  47792  caragendifcl  47797  carageniuncl  47806  caratheodorylem1  47809  hoicvrrex  47839  ovnssle  47844  ovn02  47851  ovnsubadd  47855  hoidmv1le  47877  ovnlecvr2  47893  ovncvr2  47894  isvonmbl  47921  vonmblss  47923  ovolval4lem2  47933  ovnovollem1  47939  ovnovollem2  47940  incsmf  48025  decsmf  48050  uspgropssxp  49515  mreuniss  50345  restcls2lem  50358  restcls2  50359  cnneiima  50362  imassc  50600