Theorem sseqtrd 3604

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

Syntax hints:   → wi 4   = wceq 1475   ⊆ wss 3540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-in 3547  df-ss 3554

This theorem is referenced by:  sseqtr4d  3605  uniintsn  4449  oeeui  7569  nnaword2  7597  oaabs2  7612  erssxp  7652  fipwuni  8215  ordtypelem7  8312  cantnflem3  8471  cdainf  8897  ficardun2  8908  ackbij1lem12  8936  ackbij1b  8944  fin1a2lem13  9117  winafp  9398  ioodisj  12173  reltrclfv  13606  prodss  14516  vdwlem11  15533  mrcssv  16097  mrcsscl  16103  mrcuni  16104  mressmrcd  16110  mreexexlem2d  16128  mreexexlem3d  16129  mreexfidimd  16134  subcss2  16326  resssetc  16565  funcsetcres2  16566  estrres  16602  poslubdg  16972  ipodrsfi  16986  acsmap2d  17002  mrelatlub  17009  mreclatBAD  17010  subsubm  17180  subsubg  17440  oppglsm  17880  subglsm  17909  lsmdisj  17917  gsumval3  18131  dprdres  18250  dprdss  18251  dprd2da  18264  dmdprdsplit2lem  18267  ablfac1b  18292  pgpfac1lem3  18299  issubdrg  18628  subsubrg  18629  islssd  18757  lspun  18808  lspssp  18809  lsslsp  18836  lsmssspx  18909  lspabs2  18941  lspabs3  18942  lspsolvlem  18963  lbsextlem3  18981  mplbas2  19291  gsumply1subr  19425  qsssubdrg  19624  obselocv  19891  lsslindf  19988  tgcl  20584  basgen  20603  tgfiss  20606  bastop1  20608  bastop2  20609  clsss2  20686  elcls3  20697  topssnei  20738  neiptopnei  20746  neitr  20794  restcls  20795  restlp  20797  ordtrest2  20818  iscncl  20883  cncls2  20887  cncls  20888  cnntr  20889  lmcls  20916  tgcmp  21014  cmpcld  21015  uncmp  21016  hauscmplem  21019  cmpfi  21021  clscon  21043  2ndcsb  21062  2ndcctbss  21068  2ndcomap  21071  nllyrest  21099  1stckgenlem  21166  kgencn2  21170  kgen2cn  21172  ptbasfi  21194  txcld  21216  txcls  21217  txbasval  21219  neitx  21220  ptcld  21226  ptclsg  21228  txnlly  21250  hausdiag  21258  txkgen  21265  xkopt  21268  xkopjcn  21269  xkococnlem  21272  cnmpt1res  21289  cnmpt2res  21290  imasnopn  21303  imasncld  21304  imasncls  21305  qtopcld  21326  qtoprest  21330  qtopcmap  21332  kqcldsat  21346  kqreglem2  21355  kqnrmlem2  21357  hmeontr  21382  neifil  21494  fgtr  21504  trnei  21506  uffixfr  21537  uffix2  21538  uffixsn  21539  elflim  21585  flimclslem  21598  fclsopn  21628  fclscmpi  21643  fclscmp  21644  alexsubALTlem3  21663  alexsubALT  21665  ptcmplem3  21668  subgntr  21720  opnsubg  21721  clssubg  21722  clsnsg  21723  cldsubg  21724  tgpconcompeqg  21725  snclseqg  21729  tsmsgsum  21752  tsmsid  21753  tgptsmscld  21764  ustssco  21828  utop2nei  21864  utop3cls  21865  utopreg  21866  cnextucn  21917  ressprdsds  21986  lpbl  22118  met2ndci  22137  prdsxmslem2  22144  metustexhalf  22171  psmetutop  22182  tgioo  22407  metdstri  22462  metdseq0  22465  xlebnum  22572  clsocv  22857  metelcls  22911  cmetss  22921  relcmpcmet  22923  cmpcmet  22924  minveclem4a  23009  uniioovol  23153  uniioombllem3  23159  limcres  23456  dvbss  23471  perfdvf  23473  dvreslem  23479  dvres2lem  23480  dvcnp2  23489  dvaddbr  23507  dvmulbr  23508  dvcmulf  23514  dvcj  23519  dvnfre  23521  dvmptres2  23531  dvmptcmul  23533  dvmptntr  23540  dvlip2  23562  dvcnvrelem2  23585  ftc1cn  23610  taylfvallem1  23915  taylply2  23926  taylply  23927  dvtaylp  23928  dvntaylp  23929  dvntaylp0  23930  taylthlem1  23931  taylthlem2  23932  ulmdvlem3  23960  pserulm  23980  shsub2  27568  spanssoc  27592  shub2  27626  ococin  27651  ssjo  27690  chub2  27751  spanpr  27823  elnlfn  28171  mdslj1i  28562  mdslmd3i  28575  mdexchi  28578  chirredlem1  28633  atcvat3i  28639  mdsymlem1  28646  mdsymlem5  28650  imadifxp  28796  qtophaus  29231  locfinreflem  29235  fsumcvg4  29324  esum2d  29482  omsmon  29687  omssubadd  29689  carsggect  29707  carsgclctun  29710  sitgclg  29731  eulerpartlemgf  29768  cvmscld  30509  cvmliftmolem1  30517  cvmlift2lem9  30547  cvmlift2lem11  30549  cvmlift3lem6  30560  nodense  31088  opnregcld  31495  ivthALT  31500  neibastop2  31526  fnemeet1  31531  fnejoin1  31533  poimirlem11  32590  poimirlem12  32591  poimirlem30  32609  ftc1cnnc  32654  sstotbnd  32744  ssbnd  32757  heibor1lem  32778  heiborlem3  32782  heibor  32790  lsmsat  33313  lssats  33317  lcvexchlem3  33341  lsatcvat3  33357  lkrscss  33403  lkrpssN  33468  pmod1i  34152  pclbtwnN  34201  pclunN  34202  pclss2polN  34225  pcl0N  34226  sspmaplubN  34229  paddunN  34231  pnonsingN  34237  pclfinclN  34254  osumcllem4N  34263  dia2dimlem13  35383  dvhopellsm  35424  dvadiaN  35435  dicelval1stN  35495  dicelval2nd  35496  dihssxp  35559  dihvalrel  35586  dochsscl  35675  dihoml4  35684  dochnoncon  35698  dvh3dim3N  35756  lcfrlem2  35850  lcfrlem5  35853  lcfr  35892  lcdlsp  35928  mapdsn  35948  mapdlsm  35971  mapdpglem1  35979  mapdindp0  36026  hlhilocv  36267  rntrclfvOAI  36272  ismrcd1  36279  ismrcd2  36280  coeq0i  36334  hbtlem6  36718  rgspnval  36757  iocinico  36816  trclubNEW  36945  ntrk2imkb  37355  isotone1  37366  k0004ss3  37471  wessf1ornlem  38366  iccdifprioo  38589  cncfuni  38772  cncfiooicclem1  38779  dvresntr  38806  dvmptresicc  38809  itgsubsticclem  38867  fourierdlem42  39042  fourierdlem48  39047  fourierdlem49  39048  fourierdlem50  39049  qndenserrn  39195  prsal  39214  intsaluni  39223  sssalgen  39229  dfsalgen2  39235  sge0f1o  39275  sge0split  39302  ismeannd  39360  caragensspw  39399  caragendifcl  39404  carageniuncl  39413  caratheodorylem1  39416  hoicvrrex  39446  ovnssle  39451  ovn02  39458  ovnsubadd  39462  hoidmv1le  39484  ovnlecvr2  39500  ovncvr2  39501  isvonmbl  39528  vonmblss  39530  ovolval4lem2  39540  ovnovollem1  39546  ovnovollem2  39547  incsmf  39629  decsmf  39653  subsubmgm  41587