Theorem sseqtrd 3641

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

Syntax hints:   → wi 4   = wceq 1483   ⊆ wss 3574

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-in 3581  df-ss 3588

This theorem is referenced by:  sseqtr4d  3642  uniintsn  4514  oeeui  7682  nnaword2  7710  oaabs2  7725  erssxp  7765  fipwuni  8332  ordtypelem7  8429  cantnflem3  8588  cdainf  9014  ficardun2  9025  ackbij1lem12  9053  ackbij1b  9061  fin1a2lem13  9234  winafp  9519  ioodisj  12302  reltrclfv  13758  prodss  14677  vdwlem11  15695  mrcssv  16274  mrcsscl  16280  mrcuni  16281  mressmrcd  16287  mreexexlem2d  16305  mreexexlem3d  16306  mreexfidimd  16311  subcss2  16503  resssetc  16742  funcsetcres2  16743  estrres  16779  poslubdg  17149  ipodrsfi  17163  acsmap2d  17179  mrelatlub  17186  mreclatBAD  17187  subsubm  17357  subsubg  17617  oppglsm  18057  subglsm  18086  lsmdisj  18094  gsumval3  18308  dprdres  18427  dprdss  18428  dprd2da  18441  dmdprdsplit2lem  18444  ablfac1b  18469  pgpfac1lem3  18476  issubdrg  18805  subsubrg  18806  islssd  18936  lspun  18987  lspssp  18988  lsslsp  19015  lsmssspx  19088  lspabs2  19120  lspabs3  19121  lspsolvlem  19142  lbsextlem3  19160  mplbas2  19470  gsumply1subr  19604  qsssubdrg  19805  obselocv  20072  lsslindf  20169  tgcl  20773  basgen  20792  tgfiss  20795  bastop1  20797  bastop2  20798  clsss2  20876  elcls3  20887  topssnei  20928  neiptopnei  20936  neitr  20984  restcls  20985  restlp  20987  ordtrest2  21008  iscncl  21073  cncls2  21077  cncls  21078  cnntr  21079  lmcls  21106  tgcmp  21204  cmpcld  21205  uncmp  21206  hauscmplem  21209  cmpfi  21211  clsconn  21233  2ndcsb  21252  2ndcctbss  21258  2ndcomap  21261  nllyrest  21289  1stckgenlem  21356  kgencn2  21360  kgen2cn  21362  ptbasfi  21384  txcld  21406  txcls  21407  txbasval  21409  neitx  21410  ptcld  21416  ptclsg  21418  txnlly  21440  hausdiag  21448  txkgen  21455  xkopt  21458  xkopjcn  21459  xkococnlem  21462  cnmpt1res  21479  cnmpt2res  21480  imasnopn  21493  imasncld  21494  imasncls  21495  qtopcld  21516  qtoprest  21520  qtopcmap  21522  kqcldsat  21536  kqreglem2  21545  kqnrmlem2  21547  hmeontr  21572  neifil  21684  fgtr  21694  trnei  21696  uffixfr  21727  uffix2  21728  uffixsn  21729  elflim  21775  flimclslem  21788  fclsopn  21818  fclscmpi  21833  fclscmp  21834  alexsubALTlem3  21853  alexsubALT  21855  ptcmplem3  21858  subgntr  21910  opnsubg  21911  clssubg  21912  clsnsg  21913  cldsubg  21914  tgpconncompeqg  21915  snclseqg  21919  tsmsgsum  21942  tsmsid  21943  tgptsmscld  21954  ustssco  22018  utop2nei  22054  utop3cls  22055  utopreg  22056  cnextucn  22107  ressprdsds  22176  lpbl  22308  met2ndci  22327  prdsxmslem2  22334  metustexhalf  22361  psmetutop  22372  tgioo  22599  metdstri  22654  metdseq0  22657  xlebnum  22764  clsocv  23049  metelcls  23103  cmetss  23113  relcmpcmet  23115  cmpcmet  23116  minveclem4a  23201  uniioovol  23347  uniioombllem3  23353  limcres  23650  dvbss  23665  perfdvf  23667  dvreslem  23673  dvres2lem  23674  dvcnp2  23683  dvaddbr  23701  dvmulbr  23702  dvcmulf  23708  dvcj  23713  dvnfre  23715  dvmptres2  23725  dvmptcmul  23727  dvmptntr  23734  dvlip2  23758  dvcnvrelem2  23781  ftc1cn  23806  taylfvallem1  24111  taylply2  24122  taylply  24123  dvtaylp  24124  dvntaylp  24125  dvntaylp0  24126  taylthlem1  24127  taylthlem2  24128  ulmdvlem3  24156  pserulm  24176  shsub2  28184  spanssoc  28208  shub2  28242  ococin  28267  ssjo  28306  chub2  28367  spanpr  28439  elnlfn  28787  mdslj1i  29178  mdslmd3i  29191  mdexchi  29194  chirredlem1  29249  atcvat3i  29255  mdsymlem1  29262  mdsymlem5  29266  imadifxp  29414  qtophaus  29903  locfinreflem  29907  fsumcvg4  29996  esum2d  30155  omsmon  30360  omssubadd  30362  carsggect  30380  carsgclctun  30383  sitgclg  30404  eulerpartlemgf  30441  reprpmtf1o  30704  cvmscld  31255  cvmliftmolem1  31263  cvmlift2lem9  31293  cvmlift2lem11  31295  cvmlift3lem6  31306  nodense  31842  opnregcld  32325  ivthALT  32330  neibastop2  32356  fnemeet1  32361  fnejoin1  32363  poimirlem11  33420  poimirlem12  33421  poimirlem30  33439  ftc1cnnc  33484  sstotbnd  33574  ssbnd  33587  heibor1lem  33608  heiborlem3  33612  heibor  33620  lsmsat  34295  lssats  34299  lcvexchlem3  34323  lsatcvat3  34339  lkrscss  34385  lkrpssN  34450  pmod1i  35134  pclbtwnN  35183  pclunN  35184  pclss2polN  35207  pcl0N  35208  sspmaplubN  35211  paddunN  35213  pnonsingN  35219  pclfinclN  35236  osumcllem4N  35245  dia2dimlem13  36365  dvhopellsm  36406  dvadiaN  36417  dicelval1stN  36477  dicelval2nd  36478  dihssxp  36541  dihvalrel  36568  dochsscl  36657  dihoml4  36666  dochnoncon  36680  dvh3dim3N  36738  lcfrlem2  36832  lcfrlem5  36835  lcfr  36874  lcdlsp  36910  mapdsn  36930  mapdlsm  36953  mapdpglem1  36961  mapdindp0  37008  hlhilocv  37249  rntrclfvOAI  37254  ismrcd1  37261  ismrcd2  37262  coeq0i  37316  hbtlem6  37699  rgspnval  37738  iocinico  37797  trclubNEW  37926  ntrk2imkb  38335  isotone1  38346  k0004ss3  38451  wessf1ornlem  39371  iccdifprioo  39742  limsupequzmptlem  39960  cncfuni  40099  cncfiooicclem1  40106  dvresntr  40132  dvmptresicc  40134  itgsubsticclem  40191  fourierdlem42  40366  fourierdlem48  40371  fourierdlem49  40372  fourierdlem50  40373  qndenserrn  40519  prsal  40538  intsaluni  40547  sssalgen  40553  dfsalgen2  40559  sge0f1o  40599  sge0split  40626  ismeannd  40684  caragensspw  40723  caragendifcl  40728  carageniuncl  40737  caratheodorylem1  40740  hoicvrrex  40770  ovnssle  40775  ovn02  40782  ovnsubadd  40786  hoidmv1le  40808  ovnlecvr2  40824  ovncvr2  40825  isvonmbl  40852  vonmblss  40854  ovolval4lem2  40864  ovnovollem1  40870  ovnovollem2  40871  incsmf  40951  decsmf  40975  uspgropssxp  41752  subsubmgm  41797