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 ⊢ (𝜑 → 𝐴 ⊆ 𝐶)

Syntax hints:   → wi 4   = wceq 1570   ⊆ wss 3906

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755  df-ss 3923

This theorem is referenced by:  sseqtrrd  3975  sseqtrid  3980  3sstr3d  3992  uniintsn  4951  fssdmd  6726  oeeui  8589  nnaword2  8617  oaabs2  8636  naddword2  8680  erssxp  8719  fipwuni  9387  cantnflem3  9661  ficardun2  10186  ackbij1lem12  10214  ackbij1b  10222  fin1a2lem13  10397  winafp  10683  ioodisj  13510  reltrclfv  15056  prodss  16003  mrcssv  17671  mrcsscl  17677  mrcuni  17678  mressmrcd  17684  mreexexlem2d  17702  mreexexlem3d  17703  mreexfidimd  17707  subcss2  17901  resssetc  18150  funcsetcres2  18151  estrres  18196  poslubdg  18469  ipodrsfi  18596  acsmap2d  18612  mrelatlub  18619  mreclatBAD  18620  subsubmgm  18769  subsubm  18876  subsubg  19217  trivsubgd  19220  trivnsgd  19239  oppglsm  19713  subglsm  19744  lsmdisj  19752  gsumval3  19978  dprdres  20101  dprdss  20102  dprd2da  20115  dmdprdsplit2lem  20118  ablfac1b  20143  pgpfac1lem3  20150  subsubrng  20649  subsubrg  20684  rgspnval  20698  issubdrg  20864  islssd  21037  lspun  21089  lspssp  21090  lsslsp  21117  lsmssspx  21190  lspabs2  21225  lspabs3  21226  lspsolvlem  21247  lbsextlem3  21265  0ringidl  21341  0ringprmidl  21458  qsssubdrg  21557  obselocv  21859  lsslindf  21961  sraassa  22000  mplbas2  22174  gsumply1subr  22374  tgcl  23107  basgen  23126  tgfiss  23129  bastop1  23131  bastop2  23132  clsss2  23210  elcls3  23221  topssnei  23262  neiptopnei  23270  neitr  23318  restcls  23319  restlp  23321  ordtrest2  23342  iscncl  23407  cncls2  23411  cncls  23412  cnntr  23413  lmcls  23440  tgcmp  23539  cmpcld  23540  uncmp  23541  hauscmplem  23544  cmpfi  23546  clsconn  23568  2ndcsb  23587  2ndcctbss  23593  2ndcomap  23596  nllyrest  23624  1stckgenlem  23691  kgencn2  23695  kgen2cn  23697  ptbasfi  23719  txcld  23741  txcls  23742  txbasval  23744  neitx  23745  ptcld  23751  ptclsg  23753  txnlly  23775  hausdiag  23783  txkgen  23790  xkopt  23793  xkopjcn  23794  xkococnlem  23797  cnmpt1res  23814  cnmpt2res  23815  imasnopn  23828  imasncld  23829  imasncls  23830  qtopcld  23851  qtoprest  23855  qtopcmap  23857  kqcldsat  23871  kqreglem2  23880  kqnrmlem2  23882  hmeontr  23907  neifil  24018  fgtr  24028  trnei  24030  uffixfr  24061  uffix2  24062  uffixsn  24063  elflim  24109  flimclslem  24122  fclsopn  24152  fclscmpi  24167  fclscmp  24168  alexsubALTlem3  24187  alexsubALT  24189  ptcmplem3  24192  subgntr  24245  opnsubg  24246  clssubg  24247  clsnsg  24248  cldsubg  24249  tgpconncompeqg  24250  snclseqg  24254  tsmsgsum  24277  tsmsid  24278  tgptsmscld  24289  ustssco  24353  utop2nei  24388  utop3cls  24389  utopreg  24390  cnextucn  24440  ressprdsds  24509  lpbl  24641  met2ndci  24660  prdsxmslem2  24667  metustexhalf  24694  psmetutop  24705  tgioo  24934  metdstri  24990  metdseq0  24993  xlebnum  25105  clsocv  25390  metelcls  25445  metsscmetcld  25455  cmetss  25456  relcmpcmet  25458  cmpcmet  25459  minveclem4a  25570  uniioovol  25719  uniioombllem3  25725  limcres  26026  dvbss  26041  perfdvf  26043  dvreslem  26049  dvres2lem  26050  dvmptresicc  26056  dvcnp2  26060  dvaddbr  26078  dvmulbr  26079  dvcmulf  26085  dvcj  26090  dvnfre  26092  dvmptres2  26102  dvmptcmul  26104  dvmptntr  26111  dvlip2  26135  dvcnvrelem2  26158  ftc1cn  26183  dvntaylp  26515  taylthlem1  26517  ulmdvlem3  26546  pserulm  26566  nodense  27837  mulsproplem13  28302  mulsproplem14  28303  onsbnd  28455  prlnghpg  29177  shsub2  31658  spanssoc  31682  shub2  31716  ococin  31741  ssjo  31780  chub2  31841  spanpr  31913  elnlfn  32261  mdslj1i  32652  mdslmd3i  32665  mdexchi  32668  chirredlem1  32723  atcvat3i  32729  mdsymlem1  32736  mdsymlem5  32740  imadifxp  32927  fnpreimac  32996  suppovss  33007  symgcom2  33385  pmtrcnelor  33392  cycpmco2f1  33425  0ringsubrg  33552  erlval  33559  1fldgenq  33624  elrspunidl  33717  drngmxidl  33740  drngmxidlr  33741  idlsrgmulrss1  33782  idlsrgmulrss2  33783  1arithidomlem2  33807  ply1dg3rt0irred  33855  resssra  33958  lsssra  33959  drgextlsp  33965  lvecdim0  33978  lbslsat  33987  dimkerim  33998  fedgmullem2  34001  fedgmul  34002  fldgenfldext  34039  fldextrspunlsplem  34044  fldextrspunlsp  34045  fldextrspunlem1  34046  fldextrspunfld  34047  fldextrspundgdvdslem  34051  fldextrspundgdvds  34052  algextdeglem3  34090  algextdeglem4  34091  qtophaus  34207  locfinreflem  34211  rspecbas  34236  zarclssn  34244  zarmxt1  34251  zarcmplem  34252  fsumcvg4  34321  esum2d  34464  omsmon  34669  omssubadd  34671  carsgclctun  34692  sitgclg  34713  eulerpartlemgf  34750  reprpmtf1o  34994  cvmscld  35746  cvmliftmolem1  35754  cvmlift2lem9  35784  cvmlift2lem11  35786  cvmlift3lem6  35797  opnregcld  36822  ivthALT  36827  neibastop2  36853  fnemeet1  36858  fnejoin1  36860  pibt2  38044  poimirlem11  38263  poimirlem12  38264  poimirlem30  38282  ftc1cnnc  38324  sstotbnd  38407  ssbnd  38420  heibor1lem  38441  heiborlem3  38445  heibor  38453  lsmsat  39763  lssats  39767  lcvexchlem3  39791  lsatcvat3  39807  lkrscss  39853  lkrpssN  39918  pmod1i  40603  pclbtwnN  40652  pclunN  40653  pclss2polN  40676  pcl0N  40677  sspmaplubN  40680  paddunN  40682  pnonsingN  40688  pclfinclN  40705  osumcllem4N  40714  dia2dimlem13  41831  dvhopellsm  41872  dvadiaN  41883  dicelval1stN  41943  dicelval2nd  41944  dihssxp  42007  dihvalrel  42034  dochsscl  42123  dihoml4  42132  dochnoncon  42146  dvh3dim3N  42204  lcfrlem2  42298  lcfrlem5  42301  lcfr  42340  lcdlsp  42376  mapdsn  42396  mapdlsm  42419  mapdpglem1  42427  mapdindp0  42474  hlhilocv  42712  primrootscoprbij  42850  rntrclfvOAI  43405  ismrcd1  43412  ismrcd2  43413  coeq0i  43467  hbtlem6  43839  iocinico  43922  omabs2  44042  naddwordnexlem4  44111  trclubNEW  44328  ntrk2imkb  44746  isotone1  44757  k0004ss3  44862  iccdifprioo  46215  limsupequzmptlem  46425  cncfuni  46583  cncfiooicclem1  46590  dvresntr  46615  itgsubsticclem  46672  fourierdlem42  46846  fourierdlem48  46851  fourierdlem49  46852  fourierdlem50  46853  qndenserrn  46996  prsal  47015  intsaluni  47026  sssalgen  47032  dfsalgen2  47038  sge0split  47106  ismeannd  47164  caragensspw  47206  caragendifcl  47211  carageniuncl  47220  caratheodorylem1  47223  hoicvrrex  47253  ovnssle  47258  ovn02  47265  ovnsubadd  47269  hoidmv1le  47291  ovnlecvr2  47307  ovncvr2  47308  isvonmbl  47335  vonmblss  47337  ovolval4lem2  47347  ovnovollem1  47353  ovnovollem2  47354  incsmf  47439  decsmf  47464  uspgropssxp  48892  mreuniss  49661  restcls2lem  49674  restcls2  49675  cnneiima  49678  imassc  49914