Theorem eqsstrd 3977

Description: Substitution of equality into a subclass relationship. (Contributed by NM, 25-Apr-2004.)

Hypotheses

Ref	Expression
eqsstrd.1	⊢ (𝜑 → 𝐴 = 𝐵)
eqsstrd.2	⊢ (𝜑 → 𝐵 ⊆ 𝐶)

Assertion

Ref	Expression
eqsstrd	⊢ (𝜑 → 𝐴 ⊆ 𝐶)

Proof of Theorem eqsstrd

Step	Hyp	Ref	Expression
1		eqsstrd.2	. 2 ⊢ (𝜑 → 𝐵 ⊆ 𝐶)
2		eqsstrd.1	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
3	2	sseq1d 3974	. 2 ⊢ (𝜑 → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶))
4	1, 3	mpbird 260	1 ⊢ (𝜑 → 𝐴 ⊆ 𝐶)

Syntax hints:   → wi 4   = wceq 1567   ⊆ wss 3911

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-cleq 2761  df-ss 3928

This theorem is referenced by:  eqsstrrd  3978  eqsstrdi  3987  3sstr4d  3998  fpr2g  7210  tfisi  7855  suppssof1  8195  suppss2  8196  onfununi  8328  oawordeulem  8539  oeeui  8588  nnawordex  8623  oaabslem  8633  oaabs2  8635  omabslem  8636  omabs  8637  cofonr  8660  pw2f1olem  9069  fodomr  9116  fodomfir  9287  fival  9372  dffi3  9391  ordtypelem7  9486  ordtypelem8  9487  wemapso2lem  9514  cantnflt2  9642  cantnflem1  9658  tcss  9711  tcel  9712  r1val1  9758  rankuni2b  9825  tcrank  9856  cardonle  9943  harval2  9983  ackbij2  10225  cfub  10232  cflecard  10236  cfflb  10243  isf32lem8  10344  itunitc1  10404  ttukeylem7  10499  fpwwe2lem8  10623  wuncss  10730  wuncval2  10732  grur1a  10804  trclfvub  15044  cotrtrclfv  15049  relexpfld  15086  rtrclreclem4  15098  limsupgre  15532  isercolllem3  15718  4sqlem19  17023  vdwlem1  17041  vdwlem12  17052  ramub1lem1  17086  setsstruct2  17234  ressress  17307  imasaddfnlem  17582  imasaddflem  17584  imasvscafn  17591  imasvscaf  17593  imasless  17594  isohom  17833  ressffth  17997  acsfiindd  18609  acsmap2d  18611  dirref  18657  mndind  18887  f1omvdco2  19518  pmtrfrn  19528  symgsssg  19537  symggen  19540  psgnunilem1  19563  sylow2alem2  19688  lsmssv  19713  smndlsmidm  19726  gsumzres  19979  dprdlub  20098  dprdf1  20105  dprdsn  20108  dprdcntz2  20110  dprd2dlem1  20113  dprd2da  20114  dmdprdsplit2lem  20117  ablfac1eu  20145  rgspnmin  20700  drnglpir  21469  znleval  21673  evpmss  21705  frlmsplit2  21892  f1lindf  21941  issubassa2  22011  mplsubglem  22117  evlslem4  22196  evlseu  22203  mhpaddcl  22283  mhpinvcl  22284  psdmul  22298  lpsscls  23267  tgrest  23285  resttopon  23287  rest0  23295  restfpw  23305  ordtrest  23328  ordtrest2  23330  lmcnp  23430  tgcmp  23527  uncmp  23529  hauscmplem  23532  1stcfb  23571  2ndcdisj  23582  dissnref  23654  kgencmp  23671  xkouni  23725  prdstopn  23754  txtube  23766  txcmplem2  23768  xkoptsub  23780  xkopt  23781  xkococnlem  23785  qtoprest  23843  imastopn  23846  kqdisj  23858  reghmph  23919  nrmhmph  23920  fbssfi  23963  trfilss  24015  trfg  24017  elfm3  24076  alexsubALTlem3  24175  alexsubALT  24177  cnextf  24192  cnextcn  24193  clsnsg  24236  tgpconncompeqg  24238  qustgphaus  24249  trust  24355  ustuqtop3  24369  neipcfilu  24421  metequiv2  24636  prdsxmslem2  24655  metustfbas  24683  icccmplem1  24949  metdstri  24978  pi1addf  25175  pi1addval  25176  caubl  25436  caublcls  25437  relcmpcmet  25446  minveclem4  25560  hlhil  25571  ovolficcss  25597  uniioombllem3a  25712  uniioombllem3  25713  dyadss  25722  opnmbllem  25729  i1fima2  25807  limcfval  26000  dvfval  26025  dvnres  26059  dvivth  26138  lhop  26144  taylf  26490  xrlimcnp  27099  jensen  27119  ppisval  27234  chtlepsi  27336  chpub  27350  noextend  27796  nosupbday  27835  noinfbday  27850  cutsun12  27949  cutbdaybnd  27954  cutbdaybnd2  27955  cutbdaylt  27957  sltsbday  28076  cofcut1  28079  cofcutr  28083  addbday  28177  negbdaylem  28215  precsexlem8  28373  bdayons  28435  onsbnd2  28441  noseqind  28451  n0bday  28511  bdaypw2n0bndlem  28622  iscgrglt  28749  cyclnumvtx  30090  chssoc  31789  mdsl0  32603  mdexchi  32628  atcvat3i  32689  dmdbr5ati  32715  funimass4f  32923  xrofsup  33053  swrdrn2  33215  gsumpart  33324  pmtrcnel  33350  tocycfvres1  33371  tocycfvres2  33372  cycpmco2lem6  33392  cycpmconjvlem  33402  cycpmconjslem2  33416  elrgspnsubrunlem2  33509  fldgenssv  33579  fldgenssp  33582  nsgmgc  33665  idlsrgmulrss1  33746  idlsrgmulrss2  33747  esplyfval1  33908  esplyfvaln  33909  esplyind  33910  fedgmullem1  33964  fedgmullem2  33965  constrsscn  34075  constrmon  34079  ist0cld  34168  locfinreflem  34175  cmpcref  34185  zarcls0  34203  zarclsiin  34206  zarcmplem  34216  cnvordtrestixx  34248  ordtrestNEW  34256  ordtrest2NEW  34258  pnfneige0  34286  sigagenss  34484  imambfm  34597  dya2iocress  34609  dya2icoseg  34612  dya2iocucvr  34619  ballotlemro  34858  ftc2re  34930  bnj1097  35314  bnj1452  35385  rankscottu  35456  cvmlift3lem6  35749  msubrn  35954  mclsssv  35989  mclsind  35995  liness  36570  neibastop2lem  36794  ttcmin  36930  dfttc3gw  36957  opnmbllem0  38230  mblfinlem2  38232  isbndx  38356  isbnd2  38357  ssbnd  38362  heiborlem3  38387  igenmin  38638  lsatlss  39695  lsmsat  39707  lsatfixedN  39708  lssats  39711  lpssat  39712  lssatle  39714  lssat  39715  lsatcvat3  39751  paddssat  40513  paddasslem17  40535  pmodlem2  40546  hlmod1i  40555  pl42lem4N  40681  diassdvaN  41759  dia2dimlem10  41772  cdlemn4a  41898  cdlemn5pre  41899  dihord5apre  41961  lclkrlem2e  42210  lclkrlem2p  42221  lclkrlem2v  42227  lclkrslem2  42237  lclkrs  42238  lcfrlem25  42266  lcfrlem35  42276  mapdval2N  42329  mapdpglem8  42378  mapdpglem13  42383  baerlem3lem2  42409  mapdindp2  42420  hdmap11lem2  42541  primrootspoweq0  42798  aks6d1c6lem2  42863  evlsmhpvvval  43254  prjspnssbas  43280  elrfi  43352  isnacs3  43368  mzpf  43394  mzpindd  43404  diophrw  43417  eldiophss  43432  pw2f1ocnv  43691  aomclem6  43713  hbt  43784  oasubex  43940  oaabsb  43948  nnoeomeqom  43966  omcl2  43987  naddgeoa  44048  naddwordnexlem4  44055  oaltom  44058  omltoe  44060  minregex  44187  cnvssb  44239  trclubgNEW  44271  dfrcl2  44327  fvmptiunrelexplb0da  44338  relexp0a  44369  cotrcltrcl  44378  trclimalb2  44379  cotrclrcl  44395  isotone2  44702  k0004ss1  44804  fnresdmss  45813  mptelpm  45821  ssnnf1octb  45839  uzfissfz  45969  iuneqfzuzlem  45977  xlimliminflimsup  46503  icccncfext  46528  dvnprodlem2  46588  dvnprodlem3  46589  fourierdlem41  46789  fourierdlem70  46817  fourierdlem71  46818  fourierdlem80  46827  ioorrnopnlem  46945  ioorrnopnxrlem  46947  salgenss  46977  dfsalgen2  46982  subsaliuncllem  46998  iundjiun  47101  meadjiunlem  47106  meaiunlelem  47109  meaiuninclem  47121  meaiininclem  47127  omeunle  47157  carageniuncllem2  47163  caratheodorylem1  47167  caratheodorylem2  47168  hoissre  47185  ovnsubaddlem1  47211  hoidmvlelem3  47238  ovnhoilem1  47242  ovnhoilem2  47243  ovnhoi  47244  ovncvr2  47252  voncmpl  47262  hspmbllem2  47268  hspmbl  47270  opnvonmbllem1  47273  vonmblss  47281  ovnsubadd2lem  47286  vonioolem2  47322  preimaleiinlt  47362  issmfd  47376  issmfdf  47378  cnfsmf  47381  issmfled  47398  issmfgtd  47402  smfadd  47406  smfrec  47430  smfmul  47436  smfmulc1  47437  smfpimbor1lem2  47440  smfsuplem1  47452  smflimsuplem1  47461  smflimsuplem7  47467  sprssspr  48154  isubgredgss  48554  isubgrsubgr  48558  uhgrimisgrgriclem  48619  stgrnbgr0  48653  uspgrlimlem3  48679  linc1  49125  iinfssc  49755  discsubc  49762  idfullsubc  49859