Theorem sseqtrd 3987

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

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

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3448  df-in 3920  df-ss 3930

This theorem is referenced by:  sseqtrrd  3988  sseqtrid  3999  uniintsn  4953  fssdmd  6692  oeeui  8554  nnaword2  8582  oaabs2  8600  naddword2  8643  erssxp  8678  fipwuni  9371  cantnflem3  9636  ficardun2  10147  ficardun2OLD  10148  ackbij1lem12  10176  ackbij1b  10184  fin1a2lem13  10357  winafp  10642  ioodisj  13409  reltrclfv  14914  prodss  15841  mrcssv  17508  mrcsscl  17514  mrcuni  17515  mressmrcd  17521  mreexexlem2d  17539  mreexexlem3d  17540  mreexfidimd  17544  subcss2  17743  resssetc  17992  funcsetcres2  17993  estrres  18041  poslubdg  18317  ipodrsfi  18442  acsmap2d  18458  mrelatlub  18465  mreclatBAD  18466  subsubm  18641  subsubg  18965  trivsubgd  18969  trivnsgd  18988  oppglsm  19438  subglsm  19469  lsmdisj  19477  gsumval3  19698  dprdres  19821  dprdss  19822  dprd2da  19835  dmdprdsplit2lem  19838  ablfac1b  19863  pgpfac1lem3  19870  issubdrg  20296  subsubrg  20297  islssd  20453  lspun  20505  lspssp  20506  lsslsp  20533  lsmssspx  20606  lspabs2  20640  lspabs3  20641  lspsolvlem  20662  lbsextlem3  20680  qsssubdrg  20893  obselocv  21171  lsslindf  21273  mplbas2  21480  gsumply1subr  21642  tgcl  22356  basgen  22375  tgfiss  22378  bastop1  22380  bastop2  22381  clsss2  22460  elcls3  22471  topssnei  22512  neiptopnei  22520  neitr  22568  restcls  22569  restlp  22571  ordtrest2  22592  iscncl  22657  cncls2  22661  cncls  22662  cnntr  22663  lmcls  22690  tgcmp  22789  cmpcld  22790  uncmp  22791  hauscmplem  22794  cmpfi  22796  clsconn  22818  2ndcsb  22837  2ndcctbss  22843  2ndcomap  22846  nllyrest  22874  1stckgenlem  22941  kgencn2  22945  kgen2cn  22947  ptbasfi  22969  txcld  22991  txcls  22992  txbasval  22994  neitx  22995  ptcld  23001  ptclsg  23003  txnlly  23025  hausdiag  23033  txkgen  23040  xkopt  23043  xkopjcn  23044  xkococnlem  23047  cnmpt1res  23064  cnmpt2res  23065  imasnopn  23078  imasncld  23079  imasncls  23080  qtopcld  23101  qtoprest  23105  qtopcmap  23107  kqcldsat  23121  kqreglem2  23130  kqnrmlem2  23132  hmeontr  23157  neifil  23268  fgtr  23278  trnei  23280  uffixfr  23311  uffix2  23312  uffixsn  23313  elflim  23359  flimclslem  23372  fclsopn  23402  fclscmpi  23417  fclscmp  23418  alexsubALTlem3  23437  alexsubALT  23439  ptcmplem3  23442  subgntr  23495  opnsubg  23496  clssubg  23497  clsnsg  23498  cldsubg  23499  tgpconncompeqg  23500  snclseqg  23504  tsmsgsum  23527  tsmsid  23528  tgptsmscld  23539  ustssco  23603  utop2nei  23639  utop3cls  23640  utopreg  23641  cnextucn  23692  ressprdsds  23761  lpbl  23896  met2ndci  23915  prdsxmslem2  23922  metustexhalf  23949  psmetutop  23960  tgioo  24196  metdstri  24251  metdseq0  24254  xlebnum  24365  clsocv  24651  metelcls  24706  metsscmetcld  24716  cmetss  24717  relcmpcmet  24719  cmpcmet  24720  minveclem4a  24831  uniioovol  24980  uniioombllem3  24986  limcres  25287  dvbss  25302  perfdvf  25304  dvreslem  25310  dvres2lem  25311  dvmptresicc  25317  dvcnp2  25321  dvaddbr  25339  dvmulbr  25340  dvcmulf  25346  dvcj  25351  dvnfre  25353  dvmptres2  25363  dvmptcmul  25365  dvmptntr  25372  dvlip2  25396  dvcnvrelem2  25419  ftc1cn  25444  dvntaylp  25767  taylthlem1  25769  ulmdvlem3  25798  pserulm  25818  nodense  27077  shsub2  30330  spanssoc  30354  shub2  30388  ococin  30413  ssjo  30452  chub2  30513  spanpr  30585  elnlfn  30933  mdslj1i  31324  mdslmd3i  31337  mdexchi  31340  chirredlem1  31395  atcvat3i  31401  mdsymlem1  31408  mdsymlem5  31412  imadifxp  31586  fnpreimac  31654  suppovss  31665  symgcom2  32005  pmtrcnelor  32012  cycpmco2f1  32043  0ringsubrg  32134  1fldgenq  32160  0ringidl  32277  elrspunidl  32279  0ringprmidl  32298  idlsrgmulrss1  32329  idlsrgmulrss2  32330  drgextlsp  32379  lvecdim0  32389  lbslsat  32398  dimkerim  32409  fedgmullem2  32412  fedgmul  32413  qtophaus  32506  locfinreflem  32510  rspecbas  32535  zarclssn  32543  zarmxt1  32550  zarcmplem  32551  fsumcvg4  32620  esum2d  32781  omsmon  32987  omssubadd  32989  carsgclctun  33010  sitgclg  33031  eulerpartlemgf  33068  reprpmtf1o  33328  cvmscld  33954  cvmliftmolem1  33962  cvmlift2lem9  33992  cvmlift2lem11  33994  cvmlift3lem6  34005  opnregcld  34878  ivthALT  34883  neibastop2  34909  fnemeet1  34914  fnejoin1  34916  pibt2  35961  poimirlem11  36162  poimirlem12  36163  poimirlem30  36181  ftc1cnnc  36223  sstotbnd  36307  ssbnd  36320  heibor1lem  36341  heiborlem3  36345  heibor  36353  lsmsat  37543  lssats  37547  lcvexchlem3  37571  lsatcvat3  37587  lkrscss  37633  lkrpssN  37698  pmod1i  38384  pclbtwnN  38433  pclunN  38434  pclss2polN  38457  pcl0N  38458  sspmaplubN  38461  paddunN  38463  pnonsingN  38469  pclfinclN  38486  osumcllem4N  38495  dia2dimlem13  39612  dvhopellsm  39653  dvadiaN  39664  dicelval1stN  39724  dicelval2nd  39725  dihssxp  39788  dihvalrel  39815  dochsscl  39904  dihoml4  39913  dochnoncon  39927  dvh3dim3N  39985  lcfrlem2  40079  lcfrlem5  40082  lcfr  40121  lcdlsp  40157  mapdsn  40177  mapdlsm  40200  mapdpglem1  40208  mapdindp0  40255  hlhilocv  40497  rntrclfvOAI  41072  ismrcd1  41079  ismrcd2  41080  coeq0i  41134  hbtlem6  41514  rgspnval  41553  iocinico  41604  omabs2  41725  naddwordnexlem4  41795  trclubNEW  42013  ntrk2imkb  42431  isotone1  42442  k0004ss3  42547  iccdifprioo  43874  limsupequzmptlem  44089  cncfuni  44247  cncfiooicclem1  44254  dvresntr  44279  itgsubsticclem  44336  fourierdlem42  44510  fourierdlem48  44515  fourierdlem49  44516  fourierdlem50  44517  qndenserrn  44660  prsal  44679  intsaluni  44690  sssalgen  44696  dfsalgen2  44702  sge0split  44770  ismeannd  44828  caragensspw  44870  caragendifcl  44875  carageniuncl  44884  caratheodorylem1  44887  hoicvrrex  44917  ovnssle  44922  ovn02  44929  ovnsubadd  44933  hoidmv1le  44955  ovnlecvr2  44971  ovncvr2  44972  isvonmbl  44999  vonmblss  45001  ovolval4lem2  45011  ovnovollem1  45017  ovnovollem2  45018  incsmf  45103  decsmf  45128  uspgropssxp  46166  subsubmgm  46211  mreuniss  47052  restcls2lem  47065  restcls2  47066  cnneiima  47069