Theorem sseqtrd 3959

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

Syntax hints:   → wi 4   = wceq 1542   ⊆ wss 3890

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 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-ss 3907

This theorem is referenced by:  sseqtrrd  3960  sseqtrid  3965  3sstr3d  3977  uniintsn  4928  fssdmd  6680  oeeui  8531  nnaword2  8559  oaabs2  8578  naddword2  8621  erssxp  8660  fipwuni  9332  cantnflem3  9603  ficardun2  10115  ackbij1lem12  10143  ackbij1b  10151  fin1a2lem13  10325  winafp  10611  ioodisj  13426  reltrclfv  14970  prodss  15903  mrcssv  17571  mrcsscl  17577  mrcuni  17578  mressmrcd  17584  mreexexlem2d  17602  mreexexlem3d  17603  mreexfidimd  17607  subcss2  17801  resssetc  18050  funcsetcres2  18051  estrres  18096  poslubdg  18369  ipodrsfi  18496  acsmap2d  18512  mrelatlub  18519  mreclatBAD  18520  subsubmgm  18669  subsubm  18775  subsubg  19116  trivsubgd  19119  trivnsgd  19138  oppglsm  19608  subglsm  19639  lsmdisj  19647  gsumval3  19873  dprdres  19996  dprdss  19997  dprd2da  20010  dmdprdsplit2lem  20013  ablfac1b  20038  pgpfac1lem3  20045  subsubrng  20531  subsubrg  20566  rgspnval  20580  issubdrg  20748  islssd  20921  lspun  20973  lspssp  20974  lsslsp  21001  lsslspOLD  21002  lsmssspx  21075  lspabs2  21110  lspabs3  21111  lspsolvlem  21132  lbsextlem3  21150  qsssubdrg  21416  obselocv  21718  lsslindf  21820  sraassa  21859  mplbas2  22030  gsumply1subr  22207  tgcl  22944  basgen  22963  tgfiss  22966  bastop1  22968  bastop2  22969  clsss2  23047  elcls3  23058  topssnei  23099  neiptopnei  23107  neitr  23155  restcls  23156  restlp  23158  ordtrest2  23179  iscncl  23244  cncls2  23248  cncls  23249  cnntr  23250  lmcls  23277  tgcmp  23376  cmpcld  23377  uncmp  23378  hauscmplem  23381  cmpfi  23383  clsconn  23405  2ndcsb  23424  2ndcctbss  23430  2ndcomap  23433  nllyrest  23461  1stckgenlem  23528  kgencn2  23532  kgen2cn  23534  ptbasfi  23556  txcld  23578  txcls  23579  txbasval  23581  neitx  23582  ptcld  23588  ptclsg  23590  txnlly  23612  hausdiag  23620  txkgen  23627  xkopt  23630  xkopjcn  23631  xkococnlem  23634  cnmpt1res  23651  cnmpt2res  23652  imasnopn  23665  imasncld  23666  imasncls  23667  qtopcld  23688  qtoprest  23692  qtopcmap  23694  kqcldsat  23708  kqreglem2  23717  kqnrmlem2  23719  hmeontr  23744  neifil  23855  fgtr  23865  trnei  23867  uffixfr  23898  uffix2  23899  uffixsn  23900  elflim  23946  flimclslem  23959  fclsopn  23989  fclscmpi  24004  fclscmp  24005  alexsubALTlem3  24024  alexsubALT  24026  ptcmplem3  24029  subgntr  24082  opnsubg  24083  clssubg  24084  clsnsg  24085  cldsubg  24086  tgpconncompeqg  24087  snclseqg  24091  tsmsgsum  24114  tsmsid  24115  tgptsmscld  24126  ustssco  24190  utop2nei  24225  utop3cls  24226  utopreg  24227  cnextucn  24277  ressprdsds  24346  lpbl  24478  met2ndci  24497  prdsxmslem2  24504  metustexhalf  24531  psmetutop  24542  tgioo  24771  metdstri  24827  metdseq0  24830  xlebnum  24942  clsocv  25227  metelcls  25282  metsscmetcld  25292  cmetss  25293  relcmpcmet  25295  cmpcmet  25296  minveclem4a  25407  uniioovol  25556  uniioombllem3  25562  limcres  25863  dvbss  25878  perfdvf  25880  dvreslem  25886  dvres2lem  25887  dvmptresicc  25893  dvcnp2  25897  dvaddbr  25915  dvmulbr  25916  dvcmulf  25922  dvcj  25927  dvnfre  25929  dvmptres2  25939  dvmptcmul  25941  dvmptntr  25948  dvlip2  25972  dvcnvrelem2  25995  ftc1cn  26020  dvntaylp  26348  taylthlem1  26350  ulmdvlem3  26380  pserulm  26400  nodense  27670  mulsproplem13  28134  mulsproplem14  28135  onsbnd  28287  shsub2  31411  spanssoc  31435  shub2  31469  ococin  31494  ssjo  31533  chub2  31594  spanpr  31666  elnlfn  32014  mdslj1i  32405  mdslmd3i  32418  mdexchi  32421  chirredlem1  32476  atcvat3i  32482  mdsymlem1  32489  mdsymlem5  32493  imadifxp  32686  fnpreimac  32758  suppovss  32769  symgcom2  33160  pmtrcnelor  33167  cycpmco2f1  33200  0ringsubrg  33327  erlval  33334  1fldgenq  33398  0ringidl  33496  elrspunidl  33503  0ringprmidl  33524  drngmxidl  33552  drngmxidlr  33553  idlsrgmulrss1  33586  idlsrgmulrss2  33587  1arithidomlem2  33611  ply1dg3rt0irred  33659  resssra  33746  lsssra  33747  drgextlsp  33753  lvecdim0  33766  lbslsat  33776  dimkerim  33787  fedgmullem2  33790  fedgmul  33791  fldgenfldext  33828  fldextrspunlsplem  33833  fldextrspunlsp  33834  fldextrspunlem1  33835  fldextrspunfld  33836  fldextrspundgdvdslem  33840  fldextrspundgdvds  33841  algextdeglem3  33879  algextdeglem4  33880  qtophaus  33996  locfinreflem  34000  rspecbas  34025  zarclssn  34033  zarmxt1  34040  zarcmplem  34041  fsumcvg4  34110  esum2d  34253  omsmon  34458  omssubadd  34460  carsgclctun  34481  sitgclg  34502  eulerpartlemgf  34539  reprpmtf1o  34786  cvmscld  35471  cvmliftmolem1  35479  cvmlift2lem9  35509  cvmlift2lem11  35511  cvmlift3lem6  35522  opnregcld  36528  ivthALT  36533  neibastop2  36559  fnemeet1  36564  fnejoin1  36566  pibt2  37747  poimirlem11  37966  poimirlem12  37967  poimirlem30  37985  ftc1cnnc  38027  sstotbnd  38110  ssbnd  38123  heibor1lem  38144  heiborlem3  38148  heibor  38156  lsmsat  39468  lssats  39472  lcvexchlem3  39496  lsatcvat3  39512  lkrscss  39558  lkrpssN  39623  pmod1i  40308  pclbtwnN  40357  pclunN  40358  pclss2polN  40381  pcl0N  40382  sspmaplubN  40385  paddunN  40387  pnonsingN  40393  pclfinclN  40410  osumcllem4N  40419  dia2dimlem13  41536  dvhopellsm  41577  dvadiaN  41588  dicelval1stN  41648  dicelval2nd  41649  dihssxp  41712  dihvalrel  41739  dochsscl  41828  dihoml4  41837  dochnoncon  41851  dvh3dim3N  41909  lcfrlem2  42003  lcfrlem5  42006  lcfr  42045  lcdlsp  42081  mapdsn  42101  mapdlsm  42124  mapdpglem1  42132  mapdindp0  42179  hlhilocv  42417  primrootscoprbij  42555  rntrclfvOAI  43137  ismrcd1  43144  ismrcd2  43145  coeq0i  43199  hbtlem6  43575  iocinico  43658  omabs2  43778  naddwordnexlem4  43847  trclubNEW  44064  ntrk2imkb  44482  isotone1  44493  k0004ss3  44598  iccdifprioo  45964  limsupequzmptlem  46174  cncfuni  46332  cncfiooicclem1  46339  dvresntr  46364  itgsubsticclem  46421  fourierdlem42  46595  fourierdlem48  46600  fourierdlem49  46601  fourierdlem50  46602  qndenserrn  46745  prsal  46764  intsaluni  46775  sssalgen  46781  dfsalgen2  46787  sge0split  46855  ismeannd  46913  caragensspw  46955  caragendifcl  46960  carageniuncl  46969  caratheodorylem1  46972  hoicvrrex  47002  ovnssle  47007  ovn02  47014  ovnsubadd  47018  hoidmv1le  47040  ovnlecvr2  47056  ovncvr2  47057  isvonmbl  47084  vonmblss  47086  ovolval4lem2  47096  ovnovollem1  47102  ovnovollem2  47103  incsmf  47188  decsmf  47213  uspgropssxp  48632  mreuniss  49387  restcls2lem  49400  restcls2  49401  cnneiima  49404  imassc  49640