Theorem sseqtrd 3974

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

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

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 1943  ax-6 2000  ax-7 2041  ax-9 2156  ax-ext 2737

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

This theorem is used by:  sseqtrrd  3975  sseqtrid  3980  3sstr3d  3992  uniintsn  4952  fssdmd  6728  oeeui  8590  nnaword2  8618  oaabs2  8637  naddword2  8681  erssxp  8720  fipwuni  9389  cantnflem3  9663  ficardun2  10197  ackbij1lem12  10225  ackbij1b  10233  fin1a2lem13  10407  winafp  10693  ioodisj  13520  reltrclfv  15073  prodss  16019  mrcssv  17687  mrcsscl  17693  mrcuni  17694  mressmrcd  17700  mreexexlem2d  17718  mreexexlem3d  17719  mreexfidimd  17723  subcss2  17917  resssetc  18166  funcsetcres2  18167  estrres  18212  poslubdg  18485  ipodrsfi  18612  acsmap2d  18628  mrelatlub  18635  mreclatBAD  18636  subsubmgm  18789  subsubm  18898  subsubg  19239  trivsubgd  19242  trivnsgd  19261  oppglsm  19735  subglsm  19766  lsmdisj  19774  gsumval3  20000  dprdres  20123  dprdss  20124  dprd2da  20137  dmdprdsplit2lem  20140  ablfac1b  20165  pgpfac1lem3  20172  subsubrng  20691  subsubrg  20726  rgspnval  20740  issubdrg  20912  islssd  21085  lspun  21137  lspssp  21138  lsslsp  21165  lsmssspx  21238  lspabs2  21273  lspabs3  21274  lspsolvlem  21295  lbsextlem3  21313  0ringidl  21389  0ringprmidl  21506  qsssubdrg  21605  obselocv  21907  lsslindf  22009  sraassa  22048  mplbas2  22222  gsumply1subr  22422  tgcl  23155  basgen  23174  tgfiss  23177  bastop1  23179  bastop2  23180  clsss2  23258  elcls3  23269  topssnei  23310  neiptopnei  23318  neitr  23366  restcls  23367  restlp  23369  ordtrest2  23390  iscncl  23455  cncls2  23459  cncls  23460  cnntr  23461  lmcls  23488  tgcmp  23587  cmpcld  23588  uncmp  23589  hauscmplem  23592  cmpfi  23594  clsconn  23616  2ndcsb  23635  2ndcctbss  23641  2ndcomap  23644  nllyrest  23672  1stckgenlem  23739  kgencn2  23743  kgen2cn  23745  ptbasfi  23767  txcld  23789  txcls  23790  txbasval  23792  neitx  23793  ptcld  23799  ptclsg  23801  txnlly  23823  hausdiag  23831  txkgen  23838  xkopt  23841  xkopjcn  23842  xkococnlem  23845  cnmpt1res  23862  cnmpt2res  23863  imasnopn  23876  imasncld  23877  imasncls  23878  qtopcld  23899  qtoprest  23903  qtopcmap  23905  kqcldsat  23919  kqreglem2  23928  kqnrmlem2  23930  hmeontr  23955  neifil  24066  fgtr  24076  trnei  24078  uffixfr  24109  uffix2  24110  uffixsn  24111  elflim  24157  flimclslem  24170  fclsopn  24200  fclscmpi  24215  fclscmp  24216  alexsubALTlem3  24235  alexsubALT  24237  ptcmplem3  24240  subgntr  24293  opnsubg  24294  clssubg  24295  clsnsg  24296  cldsubg  24297  tgpconncompeqg  24298  snclseqg  24302  tsmsgsum  24325  tsmsid  24326  tgptsmscld  24337  ustssco  24401  utop2nei  24436  utop3cls  24437  utopreg  24438  cnextucn  24488  ressprdsds  24557  lpbl  24689  met2ndci  24708  prdsxmslem2  24715  metustexhalf  24742  psmetutop  24753  tgioo  24982  metdstri  25038  metdseq0  25041  xlebnum  25153  clsocv  25438  metelcls  25493  metsscmetcld  25503  cmetss  25504  relcmpcmet  25506  cmpcmet  25507  minveclem4a  25618  uniioovol  25767  uniioombllem3  25773  limcres  26074  dvbss  26089  perfdvf  26091  dvreslem  26097  dvres2lem  26098  dvmptresicc  26104  dvcnp2  26108  dvaddbr  26126  dvmulbr  26127  dvcmulf  26133  dvcj  26138  dvnfre  26140  dvmptres2  26150  dvmptcmul  26152  dvmptntr  26159  dvlip2  26183  dvcnvrelem2  26206  ftc1cn  26231  dvntaylp  26563  taylthlem1  26565  ulmdvlem3  26594  pserulm  26614  nodense  27885  mulsproplem13  28350  mulsproplem14  28351  onsbnd  28503  prlnghpg  29225  shsub2  31706  spanssoc  31730  shub2  31764  ococin  31789  ssjo  31828  chub2  31889  spanpr  31961  elnlfn  32309  mdslj1i  32700  mdslmd3i  32713  mdexchi  32716  chirredlem1  32771  atcvat3i  32777  mdsymlem1  32784  mdsymlem5  32788  imadifxp  32975  fnpreimac  33044  suppovss  33055  symgcom2  33427  pmtrcnelor  33434  cycpmco2f1  33467  0ringsubrg  33594  erlval  33601  1fldgenq  33666  elrspunidl  33759  drngmxidl  33782  drngmxidlr  33783  idlsrgmulrss1  33824  idlsrgmulrss2  33825  1arithidomlem2  33849  ply1dg3rt0irred  33897  resssra  34000  lsssra  34001  drgextlsp  34007  lvecdim0  34020  lbslsat  34029  dimkerim  34040  fedgmullem2  34043  fedgmul  34044  fldgenfldext  34081  fldextrspunlsplem  34086  fldextrspunlsp  34087  fldextrspunlem1  34088  fldextrspunfld  34089  fldextrspundgdvdslem  34093  fldextrspundgdvds  34094  algextdeglem3  34132  algextdeglem4  34133  qtophaus  34249  locfinreflem  34253  rspecbas  34278  zarclssn  34286  zarmxt1  34293  zarcmplem  34294  fsumcvg4  34363  esum2d  34506  omsmon  34712  omssubadd  34714  carsgclctun  34735  sitgclg  34756  eulerpartlemgf  34793  reprpmtf1o  35037  cvmscld  35778  cvmliftmolem1  35786  cvmlift2lem9  35816  cvmlift2lem11  35818  cvmlift3lem6  35829  nadddilem4  36728  opnregcld  36874  ivthALT  36879  neibastop2  36905  fnemeet1  36910  fnejoin1  36912  pibt2  38096  poimirlem11  38315  poimirlem12  38316  poimirlem30  38334  ftc1cnnc  38376  sstotbnd  38459  ssbnd  38472  heibor1lem  38493  heiborlem3  38497  heibor  38505  lsmsat  39815  lssats  39819  lcvexchlem3  39843  lsatcvat3  39859  lkrscss  39905  lkrpssN  39970  pmod1i  40655  pclbtwnN  40704  pclunN  40705  pclss2polN  40728  pcl0N  40729  sspmaplubN  40732  paddunN  40734  pnonsingN  40740  pclfinclN  40757  osumcllem4N  40766  dia2dimlem13  41883  dvhopellsm  41924  dvadiaN  41935  dicelval1stN  41995  dicelval2nd  41996  dihssxp  42059  dihvalrel  42086  dochsscl  42175  dihoml4  42184  dochnoncon  42198  dvh3dim3N  42256  lcfrlem2  42350  lcfrlem5  42353  lcfr  42392  lcdlsp  42428  mapdsn  42448  mapdlsm  42471  mapdpglem1  42479  mapdindp0  42526  hlhilocv  42764  primrootscoprbij  42902  rntrclfvOAI  43455  ismrcd1  43462  ismrcd2  43463  coeq0i  43517  hbtlem6  43889  iocinico  43972  omabs2  44092  naddwordnexlem4  44161  trclubNEW  44378  ntrk2imkb  44796  isotone1  44807  k0004ss3  44912  iccdifprioo  46265  limsupequzmptlem  46475  cncfuni  46633  cncfiooicclem1  46640  dvresntr  46665  itgsubsticclem  46722  fourierdlem42  46896  fourierdlem48  46901  fourierdlem49  46902  fourierdlem50  46903  qndenserrn  47046  prsal  47065  intsaluni  47076  sssalgen  47082  dfsalgen2  47088  sge0split  47156  ismeannd  47214  caragensspw  47256  caragendifcl  47261  carageniuncl  47270  caratheodorylem1  47273  hoicvrrex  47303  ovnssle  47308  ovn02  47315  ovnsubadd  47319  hoidmv1le  47341  ovnlecvr2  47357  ovncvr2  47358  isvonmbl  47385  vonmblss  47387  ovolval4lem2  47397  ovnovollem1  47403  ovnovollem2  47404  incsmf  47489  decsmf  47514  uspgropssxp  48942  mreuniss  49711  restcls2lem  49724  restcls2  49725  cnneiima  49728  imassc  49964