Theorem sseqtrd 3955

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

Syntax hints:   → wi 4   = wceq 1538   ⊆ wss 3881

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-in 3888  df-ss 3898

This theorem is referenced by:  sseqtrrd  3956  uniintsn  4875  fssdmd  6503  oeeui  8211  nnaword2  8239  oaabs2  8255  erssxp  8295  fipwuni  8874  cantnflem3  9138  ficardun2  9613  ficardun2OLD  9614  ackbij1lem12  9642  ackbij1b  9650  fin1a2lem13  9823  winafp  10108  ioodisj  12860  reltrclfv  14368  prodss  15293  mrcssv  16877  mrcsscl  16883  mrcuni  16884  mressmrcd  16890  mreexexlem2d  16908  mreexexlem3d  16909  mreexfidimd  16913  subcss2  17105  resssetc  17344  funcsetcres2  17345  estrres  17381  poslubdg  17751  ipodrsfi  17765  acsmap2d  17781  mrelatlub  17788  mreclatBAD  17789  subsubm  17973  subsubg  18294  trivsubgd  18297  trivnsgd  18316  oppglsm  18759  subglsm  18791  lsmdisj  18799  gsumval3  19020  dprdres  19143  dprdss  19144  dprd2da  19157  dmdprdsplit2lem  19160  ablfac1b  19185  pgpfac1lem3  19192  issubdrg  19553  subsubrg  19554  islssd  19700  lspun  19752  lspssp  19753  lsslsp  19780  lsmssspx  19853  lspabs2  19885  lspabs3  19886  lspsolvlem  19907  lbsextlem3  19925  qsssubdrg  20150  obselocv  20417  lsslindf  20519  mplbas2  20710  gsumply1subr  20863  tgcl  21574  basgen  21593  tgfiss  21596  bastop1  21598  bastop2  21599  clsss2  21677  elcls3  21688  topssnei  21729  neiptopnei  21737  neitr  21785  restcls  21786  restlp  21788  ordtrest2  21809  iscncl  21874  cncls2  21878  cncls  21879  cnntr  21880  lmcls  21907  tgcmp  22006  cmpcld  22007  uncmp  22008  hauscmplem  22011  cmpfi  22013  clsconn  22035  2ndcsb  22054  2ndcctbss  22060  2ndcomap  22063  nllyrest  22091  1stckgenlem  22158  kgencn2  22162  kgen2cn  22164  ptbasfi  22186  txcld  22208  txcls  22209  txbasval  22211  neitx  22212  ptcld  22218  ptclsg  22220  txnlly  22242  hausdiag  22250  txkgen  22257  xkopt  22260  xkopjcn  22261  xkococnlem  22264  cnmpt1res  22281  cnmpt2res  22282  imasnopn  22295  imasncld  22296  imasncls  22297  qtopcld  22318  qtoprest  22322  qtopcmap  22324  kqcldsat  22338  kqreglem2  22347  kqnrmlem2  22349  hmeontr  22374  neifil  22485  fgtr  22495  trnei  22497  uffixfr  22528  uffix2  22529  uffixsn  22530  elflim  22576  flimclslem  22589  fclsopn  22619  fclscmpi  22634  fclscmp  22635  alexsubALTlem3  22654  alexsubALT  22656  ptcmplem3  22659  subgntr  22712  opnsubg  22713  clssubg  22714  clsnsg  22715  cldsubg  22716  tgpconncompeqg  22717  snclseqg  22721  tsmsgsum  22744  tsmsid  22745  tgptsmscld  22756  ustssco  22820  utop2nei  22856  utop3cls  22857  utopreg  22858  cnextucn  22909  ressprdsds  22978  lpbl  23110  met2ndci  23129  prdsxmslem2  23136  metustexhalf  23163  psmetutop  23174  tgioo  23401  metdstri  23456  metdseq0  23459  xlebnum  23570  clsocv  23854  metelcls  23909  metsscmetcld  23919  cmetss  23920  relcmpcmet  23922  cmpcmet  23923  minveclem4a  24034  uniioovol  24183  uniioombllem3  24189  limcres  24489  dvbss  24504  perfdvf  24506  dvreslem  24512  dvres2lem  24513  dvmptresicc  24519  dvcnp2  24523  dvaddbr  24541  dvmulbr  24542  dvcmulf  24548  dvcj  24553  dvnfre  24555  dvmptres2  24565  dvmptcmul  24567  dvmptntr  24574  dvlip2  24598  dvcnvrelem2  24621  ftc1cn  24646  dvntaylp  24966  taylthlem1  24968  ulmdvlem3  24997  pserulm  25017  shsub2  29108  spanssoc  29132  shub2  29166  ococin  29191  ssjo  29230  chub2  29291  spanpr  29363  elnlfn  29711  mdslj1i  30102  mdslmd3i  30115  mdexchi  30118  chirredlem1  30173  atcvat3i  30179  mdsymlem1  30186  mdsymlem5  30190  imadifxp  30364  fnpreimac  30434  suppovss  30443  symgcom2  30778  pmtrcnelor  30785  cycpmco2f1  30816  0ringidl  31013  elrspunidl  31014  0ringprmidl  31033  idlsrgmulrss1  31064  idlsrgmulrss2  31065  drgextlsp  31084  lvecdim0  31093  lbslsat  31102  dimkerim  31111  fedgmullem2  31114  fedgmul  31115  qtophaus  31189  locfinreflem  31193  rspecbas  31218  zarclssn  31226  zarmxt1  31233  zarcmplem  31234  fsumcvg4  31303  esum2d  31462  omsmon  31666  omssubadd  31668  carsgclctun  31689  sitgclg  31710  eulerpartlemgf  31747  reprpmtf1o  32007  cvmscld  32633  cvmliftmolem1  32641  cvmlift2lem9  32671  cvmlift2lem11  32673  cvmlift3lem6  32684  nodense  33309  opnregcld  33791  ivthALT  33796  neibastop2  33822  fnemeet1  33827  fnejoin1  33829  pibt2  34834  poimirlem11  35068  poimirlem12  35069  poimirlem30  35087  ftc1cnnc  35129  sstotbnd  35213  ssbnd  35226  heibor1lem  35247  heiborlem3  35251  heibor  35259  lsmsat  36304  lssats  36308  lcvexchlem3  36332  lsatcvat3  36348  lkrscss  36394  lkrpssN  36459  pmod1i  37144  pclbtwnN  37193  pclunN  37194  pclss2polN  37217  pcl0N  37218  sspmaplubN  37221  paddunN  37223  pnonsingN  37229  pclfinclN  37246  osumcllem4N  37255  dia2dimlem13  38372  dvhopellsm  38413  dvadiaN  38424  dicelval1stN  38484  dicelval2nd  38485  dihssxp  38548  dihvalrel  38575  dochsscl  38664  dihoml4  38673  dochnoncon  38687  dvh3dim3N  38745  lcfrlem2  38839  lcfrlem5  38842  lcfr  38881  lcdlsp  38917  mapdsn  38937  mapdlsm  38960  mapdpglem1  38968  mapdindp0  39015  hlhilocv  39253  rntrclfvOAI  39632  ismrcd1  39639  ismrcd2  39640  coeq0i  39694  hbtlem6  40073  rgspnval  40112  iocinico  40162  trclubNEW  40319  ntrk2imkb  40740  isotone1  40751  k0004ss3  40856  iccdifprioo  42153  limsupequzmptlem  42370  cncfuni  42528  cncfiooicclem1  42535  dvresntr  42560  itgsubsticclem  42617  fourierdlem42  42791  fourierdlem48  42796  fourierdlem49  42797  fourierdlem50  42798  qndenserrn  42941  prsal  42960  intsaluni  42969  sssalgen  42975  dfsalgen2  42981  sge0split  43048  ismeannd  43106  caragensspw  43148  caragendifcl  43153  carageniuncl  43162  caratheodorylem1  43165  hoicvrrex  43195  ovnssle  43200  ovn02  43207  ovnsubadd  43211  hoidmv1le  43233  ovnlecvr2  43249  ovncvr2  43250  isvonmbl  43277  vonmblss  43279  ovolval4lem2  43289  ovnovollem1  43295  ovnovollem2  43296  incsmf  43376  decsmf  43400  uspgropssxp  44372  subsubmgm  44417