Theorem sseqtrd 3944

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ⊆ wss 3895

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2752  df-ss 3896

This theorem is used by:  sseqtrrd  3945  sseqtrid  3950  3sstr3d  3962  uniintsn  4944  fssdmd  6729  oeeui  8615  nnaword2  8643  oaabs2  8662  naddword2  8706  erssxp  8745  fipwuni  9422  cantnflem3  9696  ficardun2  10284  ackbij1lem12  10312  ackbij1b  10320  fin1a2lem13  10494  winafp  10786  ioodisj  13617  reltrclfv  15176  prodss  16120  mrcssv  17794  mrcsscl  17800  mrcuni  17801  mressmrcd  17807  mreexexlem2d  17825  mreexexlem3d  17826  mreexfidimd  17830  subcss2  18024  resssetc  18273  funcsetcres2  18274  estrres  18319  poslubdg  18592  ipodrsfi  18719  acsmap2d  18735  mrelatlub  18742  mreclatBAD  18743  subsubmgm  18905  subsubm  19018  subsubg  19366  trivsubgd  19369  trivnsgd  19388  oppglsm  19862  subglsm  19893  lsmdisj  19901  gsumval3  20127  dprdres  20250  dprdss  20251  dprd2da  20264  dmdprdsplit2lem  20267  ablfac1b  20292  pgpfac1lem3  20299  subsubrng  20821  subsubrg  20856  rgspnval  20870  issubdrg  21043  islssd  21216  lspun  21268  lspssp  21269  lsslsp  21296  lsmssspx  21369  lspabs2  21404  lspabs3  21405  lspsolvlem  21426  lbsextlem3  21444  0ringidl  21520  0ringprmidl  21639  qsssubdrg  21738  obselocv  22040  lsslindf  22142  sraassa  22183  mplbas2  22357  gsumply1subr  22557  tgcl  23293  basgen  23312  tgfiss  23315  bastop1  23317  bastop2  23318  clsss2  23396  elcls3  23407  topssnei  23448  neiptopnei  23456  neitr  23504  restcls  23505  restlp  23507  ordtrest2  23528  iscncl  23593  cncls2  23597  cncls  23598  cnntr  23599  lmcls  23626  tgcmp  23725  cmpcld  23726  uncmp  23727  hauscmplem  23730  cmpfi  23732  clsconn  23754  2ndcsb  23773  2ndcctbss  23780  2ndcomap  23783  nllyrest  23811  1stckgenlem  23878  kgencn2  23882  kgen2cn  23884  ptbasfi  23906  txcld  23928  txcls  23929  txbasval  23931  neitx  23932  ptcld  23938  ptclsg  23940  txnlly  23962  hausdiag  23970  txkgen  23977  xkopt  23980  xkopjcn  23981  xkococnlem  23984  cnmpt1res  24001  cnmpt2res  24002  imasnopn  24015  imasncld  24016  imasncls  24017  qtopcld  24038  qtoprest  24042  qtopcmap  24044  kqcldsat  24058  kqreglem2  24067  kqnrmlem2  24069  hmeontr  24094  neifil  24205  fgtr  24215  trnei  24217  uffixfr  24248  uffix2  24249  uffixsn  24250  elflim  24296  flimclslem  24309  fclsopn  24339  fclscmpi  24354  fclscmp  24355  alexsubALTlem3  24374  alexsubALT  24376  ptcmplem3  24379  subgntr  24432  opnsubg  24433  clssubg  24434  clsnsg  24435  cldsubg  24436  tgpconncompeqg  24437  snclseqg  24441  tsmsgsum  24464  tsmsid  24465  tgptsmscld  24476  ustssco  24540  utop2nei  24575  utop3cls  24576  utopreg  24577  cnextucn  24627  ressprdsds  24696  lpbl  24828  met2ndci  24847  prdsxmslem2  24854  metustexhalf  24881  psmetutop  24892  tgioo  25121  metdstri  25177  metdseq0  25180  xlebnum  25292  clsocv  25577  metelcls  25632  metsscmetcld  25642  cmetss  25643  relcmpcmet  25645  cmpcmet  25646  minveclem4a  25757  uniioovol  25906  uniioombllem3  25912  limcres  26212  dvbss  26227  perfdvf  26229  dvreslem  26235  dvres2lem  26236  dvmptresicc  26242  dvcnp2  26246  dvaddbr  26264  dvmulbr  26265  dvcmulf  26271  dvcj  26276  dvnfre  26278  dvmptres2  26288  dvmptcmul  26290  dvmptntr  26297  dvlip2  26321  dvcnvrelem2  26344  ftc1cn  26369  dvntaylp  26704  taylthlem1  26706  ulmdvlem3  26735  pserulm  26755  nodense  28055  mulsproplem13  28520  mulsproplem14  28521  onsbnd  28673  prlnghpg  29430  shsub2  31933  spanssoc  31957  shub2  31991  ococin  32016  ssjo  32055  chub2  32116  spanpr  32188  elnlfn  32536  mdslj1i  32927  mdslmd3i  32940  mdexchi  32943  chirredlem1  32998  atcvat3i  33004  mdsymlem1  33011  mdsymlem5  33015  imadifxp  33243  fnpreimac  33312  suppovss  33322  symgcom2  33692  pmtrcnelor  33699  cycpmco2f1  33732  0ringsubrg  33859  erlval  33866  1fldgenq  33931  elrspunidl  34025  drngmxidl  34048  drngmxidlr  34049  idlsrgmulrss1  34090  idlsrgmulrss2  34091  1arithidomlem2  34115  ply1dg3rt0irred  34163  resssra  34266  lsssra  34267  drgextlsp  34273  lvecdim0  34286  lbslsat  34295  dimkerim  34306  fedgmullem2  34309  fedgmul  34310  fldgenfldext  34347  fldextrspunlsplem  34352  fldextrspunlsp  34353  fldextrspunlem1  34354  fldextrspunfld  34355  fldextrspundgdvdslem  34359  fldextrspundgdvds  34360  algextdeglem3  34398  algextdeglem4  34399  qtophaus  34515  locfinreflem  34519  rspecbas  34544  zarclssn  34552  zarmxt1  34559  zarcmplem  34560  fsumcvg4  34629  esum2d  34772  omsmon  34977  omssubadd  34979  carsgclctun  35000  sitgclg  35021  eulerpartlemgf  35058  reprpmtf1o  35302  maxssj0  35946  cvmscld  36125  cvmliftmolem1  36133  cvmlift2lem9  36163  cvmlift2lem11  36165  cvmlift3lem6  36176  nadddilem4  37065  opnregcld  37211  ivthALT  37216  neibastop2  37242  fnemeet1  37247  fnejoin1  37249  pibt2  38434  poimirlem11  38643  poimirlem12  38644  poimirlem30  38662  ftc1cnnc  38704  sstotbnd  38803  ssbnd  38816  heibor1lem  38837  heiborlem3  38841  heibor  38849  lsmsat  40159  lssats  40163  lcvexchlem3  40187  lsatcvat3  40203  lkrscss  40249  lkrpssN  40314  pmod1i  40999  pclbtwnN  41048  pclunN  41049  pclss2polN  41072  pcl0N  41073  sspmaplubN  41076  paddunN  41078  pnonsingN  41084  pclfinclN  41101  osumcllem4N  41110  dia2dimlem13  42227  dvhopellsm  42268  dvadiaN  42279  dicelval1stN  42339  dicelval2nd  42340  dihssxp  42403  dihvalrel  42430  dochsscl  42519  dihoml4  42528  dochnoncon  42542  dvh3dim3N  42600  lcfrlem2  42694  lcfrlem5  42697  lcfr  42736  lcdlsp  42772  mapdsn  42792  mapdlsm  42815  mapdpglem1  42823  mapdindp0  42870  hlhilocv  43108  primrootscoprbij  43246  rntrclfvOAI  43796  ismrcd1  43803  ismrcd2  43804  coeq0i  43858  hbtlem6  44225  iocinico  44308  omabs2  44428  naddwordnexlem4  44497  trclubNEW  44713  ntrk2imkb  45131  isotone1  45142  k0004ss3  45247  iccdifprioo  46622  limsupequzmptlem  46832  cncfuni  46990  cncfiooicclem1  46997  dvresntr  47022  itgsubsticclem  47079  fourierdlem42  47253  fourierdlem48  47258  fourierdlem49  47259  fourierdlem50  47260  qndenserrn  47403  prsal  47422  intsaluni  47433  sssalgen  47439  dfsalgen2  47445  sge0split  47513  ismeannd  47571  caragensspw  47613  caragendifcl  47618  carageniuncl  47627  caratheodorylem1  47630  hoicvrrex  47660  ovnssle  47665  ovn02  47672  ovnsubadd  47676  hoidmv1le  47698  ovnlecvr2  47714  ovncvr2  47715  isvonmbl  47742  vonmblss  47744  ovolval4lem2  47754  ovnovollem1  47760  ovnovollem2  47761  incsmf  47846  decsmf  47871  uspgropssxp  49336  mreuniss  50108  restcls2lem  50121  restcls2  50122  cnneiima  50125  imassc  50363