Theorem sseqtrd 3967

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ⊆ wss 3899

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2732

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

This theorem is used by:  sseqtrrd  3968  sseqtrid  3973  3sstr3d  3985  uniintsn  4945  fssdmd  6721  oeeui  8590  nnaword2  8618  oaabs2  8637  naddword2  8681  erssxp  8720  fipwuni  9396  cantnflem3  9670  ficardun2  10204  ackbij1lem12  10232  ackbij1b  10240  fin1a2lem13  10414  winafp  10706  ioodisj  13535  reltrclfv  15090  prodss  16034  mrcssv  17702  mrcsscl  17708  mrcuni  17709  mressmrcd  17715  mreexexlem2d  17733  mreexexlem3d  17734  mreexfidimd  17738  subcss2  17932  resssetc  18181  funcsetcres2  18182  estrres  18227  poslubdg  18500  ipodrsfi  18627  acsmap2d  18643  mrelatlub  18650  mreclatBAD  18651  subsubmgm  18812  subsubm  18925  subsubg  19273  trivsubgd  19276  trivnsgd  19295  oppglsm  19769  subglsm  19800  lsmdisj  19808  gsumval3  20034  dprdres  20157  dprdss  20158  dprd2da  20171  dmdprdsplit2lem  20174  ablfac1b  20199  pgpfac1lem3  20206  subsubrng  20725  subsubrg  20760  rgspnval  20774  issubdrg  20946  islssd  21119  lspun  21171  lspssp  21172  lsslsp  21199  lsmssspx  21272  lspabs2  21307  lspabs3  21308  lspsolvlem  21329  lbsextlem3  21347  0ringidl  21423  0ringprmidl  21540  qsssubdrg  21639  obselocv  21941  lsslindf  22043  sraassa  22084  mplbas2  22258  gsumply1subr  22458  tgcl  23194  basgen  23213  tgfiss  23216  bastop1  23218  bastop2  23219  clsss2  23297  elcls3  23308  topssnei  23349  neiptopnei  23357  neitr  23405  restcls  23406  restlp  23408  ordtrest2  23429  iscncl  23494  cncls2  23498  cncls  23499  cnntr  23500  lmcls  23527  tgcmp  23626  cmpcld  23627  uncmp  23628  hauscmplem  23631  cmpfi  23633  clsconn  23655  2ndcsb  23674  2ndcctbss  23681  2ndcomap  23684  nllyrest  23712  1stckgenlem  23779  kgencn2  23783  kgen2cn  23785  ptbasfi  23807  txcld  23829  txcls  23830  txbasval  23832  neitx  23833  ptcld  23839  ptclsg  23841  txnlly  23863  hausdiag  23871  txkgen  23878  xkopt  23881  xkopjcn  23882  xkococnlem  23885  cnmpt1res  23902  cnmpt2res  23903  imasnopn  23916  imasncld  23917  imasncls  23918  qtopcld  23939  qtoprest  23943  qtopcmap  23945  kqcldsat  23959  kqreglem2  23968  kqnrmlem2  23970  hmeontr  23995  neifil  24106  fgtr  24116  trnei  24118  uffixfr  24149  uffix2  24150  uffixsn  24151  elflim  24197  flimclslem  24210  fclsopn  24240  fclscmpi  24255  fclscmp  24256  alexsubALTlem3  24275  alexsubALT  24277  ptcmplem3  24280  subgntr  24333  opnsubg  24334  clssubg  24335  clsnsg  24336  cldsubg  24337  tgpconncompeqg  24338  snclseqg  24342  tsmsgsum  24365  tsmsid  24366  tgptsmscld  24377  ustssco  24441  utop2nei  24476  utop3cls  24477  utopreg  24478  cnextucn  24528  ressprdsds  24597  lpbl  24729  met2ndci  24748  prdsxmslem2  24755  metustexhalf  24782  psmetutop  24793  tgioo  25022  metdstri  25078  metdseq0  25081  xlebnum  25193  clsocv  25478  metelcls  25533  metsscmetcld  25543  cmetss  25544  relcmpcmet  25546  cmpcmet  25547  minveclem4a  25658  uniioovol  25807  uniioombllem3  25813  limcres  26113  dvbss  26128  perfdvf  26130  dvreslem  26136  dvres2lem  26137  dvmptresicc  26143  dvcnp2  26147  dvaddbr  26165  dvmulbr  26166  dvcmulf  26172  dvcj  26177  dvnfre  26179  dvmptres2  26189  dvmptcmul  26191  dvmptntr  26198  dvlip2  26222  dvcnvrelem2  26245  ftc1cn  26270  dvntaylp  26607  taylthlem1  26609  ulmdvlem3  26638  pserulm  26658  nodense  27928  mulsproplem13  28393  mulsproplem14  28394  onsbnd  28546  prlnghpg  29303  shsub2  31806  spanssoc  31830  shub2  31864  ococin  31889  ssjo  31928  chub2  31989  spanpr  32061  elnlfn  32409  mdslj1i  32800  mdslmd3i  32813  mdexchi  32816  chirredlem1  32871  atcvat3i  32877  mdsymlem1  32884  mdsymlem5  32888  imadifxp  33074  fnpreimac  33143  suppovss  33153  symgcom2  33524  pmtrcnelor  33531  cycpmco2f1  33564  0ringsubrg  33691  erlval  33698  1fldgenq  33763  elrspunidl  33856  drngmxidl  33879  drngmxidlr  33880  idlsrgmulrss1  33921  idlsrgmulrss2  33922  1arithidomlem2  33946  ply1dg3rt0irred  33994  resssra  34097  lsssra  34098  drgextlsp  34104  lvecdim0  34117  lbslsat  34126  dimkerim  34137  fedgmullem2  34140  fedgmul  34141  fldgenfldext  34178  fldextrspunlsplem  34183  fldextrspunlsp  34184  fldextrspunlem1  34185  fldextrspunfld  34186  fldextrspundgdvdslem  34190  fldextrspundgdvds  34191  algextdeglem3  34229  algextdeglem4  34230  qtophaus  34346  locfinreflem  34350  rspecbas  34375  zarclssn  34383  zarmxt1  34390  zarcmplem  34391  fsumcvg4  34460  esum2d  34603  omsmon  34809  omssubadd  34811  carsgclctun  34832  sitgclg  34853  eulerpartlemgf  34890  reprpmtf1o  35134  cvmscld  35852  cvmliftmolem1  35860  cvmlift2lem9  35890  cvmlift2lem11  35892  cvmlift3lem6  35903  nadddilem4  36803  opnregcld  36949  ivthALT  36954  neibastop2  36980  fnemeet1  36985  fnejoin1  36987  pibt2  38171  poimirlem11  38380  poimirlem12  38381  poimirlem30  38399  ftc1cnnc  38441  sstotbnd  38525  ssbnd  38538  heibor1lem  38559  heiborlem3  38563  heibor  38571  lsmsat  39881  lssats  39885  lcvexchlem3  39909  lsatcvat3  39925  lkrscss  39971  lkrpssN  40036  pmod1i  40721  pclbtwnN  40770  pclunN  40771  pclss2polN  40794  pcl0N  40795  sspmaplubN  40798  paddunN  40800  pnonsingN  40806  pclfinclN  40823  osumcllem4N  40832  dia2dimlem13  41949  dvhopellsm  41990  dvadiaN  42001  dicelval1stN  42061  dicelval2nd  42062  dihssxp  42125  dihvalrel  42152  dochsscl  42241  dihoml4  42250  dochnoncon  42264  dvh3dim3N  42322  lcfrlem2  42416  lcfrlem5  42419  lcfr  42458  lcdlsp  42494  mapdsn  42514  mapdlsm  42537  mapdpglem1  42545  mapdindp0  42592  hlhilocv  42830  primrootscoprbij  42968  rntrclfvOAI  43536  ismrcd1  43543  ismrcd2  43544  coeq0i  43598  hbtlem6  43970  iocinico  44053  omabs2  44173  naddwordnexlem4  44242  trclubNEW  44459  ntrk2imkb  44877  isotone1  44888  k0004ss3  44993  iccdifprioo  46346  limsupequzmptlem  46556  cncfuni  46714  cncfiooicclem1  46721  dvresntr  46746  itgsubsticclem  46803  fourierdlem42  46977  fourierdlem48  46982  fourierdlem49  46983  fourierdlem50  46984  qndenserrn  47127  prsal  47146  intsaluni  47157  sssalgen  47163  dfsalgen2  47169  sge0split  47237  ismeannd  47295  caragensspw  47337  caragendifcl  47342  carageniuncl  47351  caratheodorylem1  47354  hoicvrrex  47384  ovnssle  47389  ovn02  47396  ovnsubadd  47400  hoidmv1le  47422  ovnlecvr2  47438  ovncvr2  47439  isvonmbl  47466  vonmblss  47468  ovolval4lem2  47478  ovnovollem1  47484  ovnovollem2  47485  incsmf  47570  decsmf  47595  uspgropssxp  49060  mreuniss  49826  restcls2lem  49839  restcls2  49840  cnneiima  49843  imassc  50079