Theorem eqsstrd 3978

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-ss 3928

This theorem is referenced by:  eqsstrrd  3979  eqsstrdi  3988  3sstr4d  3999  fpr2g  7167  tfisi  7815  suppssof1  8155  suppss2  8156  onfununi  8287  oawordeulem  8495  oeeui  8543  nnawordex  8578  oaabslem  8588  oaabs2  8590  omabslem  8591  omabs  8592  cofonr  8615  pw2f1olem  9022  fodomr  9069  fodomfir  9255  fival  9339  dffi3  9358  ordtypelem7  9453  ordtypelem8  9454  wemapso2lem  9481  cantnflt2  9602  cantnflem1  9618  tcss  9673  tcel  9674  r1val1  9715  rankuni2b  9782  tcrank  9813  cardonle  9886  harval2  9926  ackbij2  10171  cfub  10178  cflecard  10182  cfflb  10188  isf32lem8  10289  itunitc1  10349  ttukeylem7  10444  fpwwe2lem8  10567  wuncss  10674  wuncval2  10676  grur1a  10748  trclfvub  14949  cotrtrclfv  14954  relexpfld  14991  rtrclreclem4  15003  limsupgre  15423  isercolllem3  15609  4sqlem19  16910  vdwlem1  16928  vdwlem12  16939  ramub1lem1  16973  setsstruct2  17120  ressress  17193  imasaddfnlem  17467  imasaddflem  17469  imasvscafn  17476  imasvscaf  17478  imasless  17479  isohom  17714  ressffth  17878  acsfiindd  18488  acsmap2d  18490  dirref  18536  mndind  18731  f1omvdco2  19354  pmtrfrn  19364  symgsssg  19373  symggen  19376  psgnunilem1  19399  sylow2alem2  19524  lsmssv  19549  smndlsmidm  19562  gsumzres  19815  dprdlub  19934  dprdf1  19941  dprdsn  19944  dprdcntz2  19946  dprd2dlem1  19949  dprd2da  19950  dmdprdsplit2lem  19953  ablfac1eu  19981  rgspnmin  20500  drnglpir  21218  znleval  21440  evpmss  21471  frlmsplit2  21658  f1lindf  21707  issubassa2  21777  mplsubglem  21884  evlslem4  21959  evlseu  21966  mhpaddcl  22014  mhpinvcl  22015  psdmul  22029  lpsscls  23004  tgrest  23022  resttopon  23024  rest0  23032  restfpw  23042  ordtrest  23065  ordtrest2  23067  lmcnp  23167  tgcmp  23264  uncmp  23266  hauscmplem  23269  1stcfb  23308  2ndcdisj  23319  dissnref  23391  kgencmp  23408  xkouni  23462  prdstopn  23491  txtube  23503  txcmplem2  23505  xkoptsub  23517  xkopt  23518  xkococnlem  23522  qtoprest  23580  imastopn  23583  kqdisj  23595  reghmph  23656  nrmhmph  23657  fbssfi  23700  trfilss  23752  trfg  23754  elfm3  23813  alexsubALTlem3  23912  alexsubALT  23914  cnextf  23929  cnextcn  23930  clsnsg  23973  tgpconncompeqg  23975  qustgphaus  23986  trust  24093  ustuqtop3  24107  neipcfilu  24159  metequiv2  24374  prdsxmslem2  24393  metustfbas  24421  icccmplem1  24687  metdstri  24716  pi1addf  24923  pi1addval  24924  caubl  25184  caublcls  25185  relcmpcmet  25194  minveclem4  25308  hlhil  25319  ovolficcss  25346  uniioombllem3a  25461  uniioombllem3  25462  dyadss  25471  opnmbllem  25478  i1fima2  25556  limcfval  25749  dvfval  25774  dvnres  25809  dvivth  25891  lhop  25897  taylf  26244  xrlimcnp  26854  jensen  26875  ppisval  26990  chtlepsi  27093  chpub  27107  noextend  27554  nosupbday  27593  noinfbday  27608  scutun12  27698  scutbdaybnd  27703  scutbdaybnd2  27704  scutbdaylt  27706  cofcut1  27804  cofcutr  27808  addsbday  27900  negsbdaylem  27938  precsexlem8  28092  bdayon  28149  noseqind  28162  n0sbday  28220  iscgrglt  28417  cyclnumvtx  29703  chssoc  31398  mdsl0  32212  mdexchi  32237  atcvat3i  32298  dmdbr5ati  32324  funimass4f  32534  xrofsup  32663  swrdrn2  32849  gsumpart  32970  pmtrcnel  33019  tocycfvres1  33040  tocycfvres2  33041  cycpmco2lem6  33061  cycpmconjvlem  33071  cycpmconjslem2  33085  elrgspnsubrunlem2  33172  fldgenssv  33238  fldgenssp  33241  nsgmgc  33356  idlsrgmulrss1  33455  idlsrgmulrss2  33456  fedgmullem1  33598  fedgmullem2  33599  constrsscn  33703  constrmon  33707  ist0cld  33796  locfinreflem  33803  cmpcref  33813  zarcls0  33831  zarclsiin  33834  zarcmplem  33844  cnvordtrestixx  33876  ordtrestNEW  33884  ordtrest2NEW  33886  pnfneige0  33914  sigagenss  34112  imambfm  34226  dya2iocress  34238  dya2icoseg  34241  dya2iocucvr  34248  ballotlemro  34487  ftc2re  34562  bnj1097  34944  bnj1452  35015  cvmlift3lem6  35284  msubrn  35489  mclsssv  35524  mclsind  35530  liness  36106  neibastop2lem  36321  opnmbllem0  37623  mblfinlem2  37625  isbndx  37749  isbnd2  37750  ssbnd  37755  heiborlem3  37780  igenmin  38031  lsatlss  38962  lsmsat  38974  lsatfixedN  38975  lssats  38978  lpssat  38979  lssatle  38981  lssat  38982  lsatcvat3  39018  paddssat  39781  paddasslem17  39803  pmodlem2  39814  hlmod1i  39823  pl42lem4N  39949  diassdvaN  41027  dia2dimlem10  41040  cdlemn4a  41166  cdlemn5pre  41167  dihord5apre  41229  lclkrlem2e  41478  lclkrlem2p  41489  lclkrlem2v  41495  lclkrslem2  41505  lclkrs  41506  lcfrlem25  41534  lcfrlem35  41544  mapdval2N  41597  mapdpglem8  41646  mapdpglem13  41651  baerlem3lem2  41677  mapdindp2  41688  hdmap11lem2  41809  primrootspoweq0  42067  aks6d1c6lem2  42132  evlsmhpvvval  42556  prjspnssbas  42582  elrfi  42655  isnacs3  42671  mzpf  42697  mzpindd  42707  diophrw  42720  eldiophss  42735  rmxyelqirrOLD  42872  pw2f1ocnv  42999  aomclem6  43021  hbt  43092  oasubex  43248  oaabsb  43256  nnoeomeqom  43274  omcl2  43295  naddgeoa  43356  naddwordnexlem4  43363  oaltom  43367  omltoe  43369  minregex  43496  cnvssb  43548  trclubgNEW  43580  dfrcl2  43636  fvmptiunrelexplb0da  43647  relexp0a  43678  cotrcltrcl  43687  trclimalb2  43688  cotrclrcl  43704  isotone2  44011  k0004ss1  44113  fnresdmss  45135  mptelpm  45143  ssnnf1octb  45161  uzfissfz  45295  iuneqfzuzlem  45303  xlimliminflimsup  45833  icccncfext  45858  dvnprodlem2  45918  dvnprodlem3  45919  fourierdlem41  46119  fourierdlem70  46147  fourierdlem71  46148  fourierdlem80  46157  fourierdlem113  46190  ioorrnopnlem  46275  ioorrnopnxrlem  46277  salgenss  46307  dfsalgen2  46312  subsaliuncllem  46328  iundjiun  46431  meadjiunlem  46436  meaiunlelem  46439  meaiuninclem  46451  meaiininclem  46457  omeunle  46487  carageniuncllem2  46493  caratheodorylem1  46497  caratheodorylem2  46498  hoissre  46515  ovnsubaddlem1  46541  hoidmvlelem3  46568  ovnhoilem1  46572  ovnhoilem2  46573  ovnhoi  46574  ovncvr2  46582  voncmpl  46592  hspmbllem2  46598  hspmbl  46600  opnvonmbllem1  46603  vonmblss  46611  ovnsubadd2lem  46616  vonioolem2  46652  preimageiingt  46691  preimaleiinlt  46692  issmfd  46706  issmfdf  46708  sssmf  46709  cnfsmf  46711  issmfled  46728  issmfgtd  46732  smfadd  46736  smfrec  46760  smfmul  46766  smfmulc1  46767  smfpimbor1lem2  46770  smfsuplem1  46782  smflimsuplem1  46791  smflimsuplem7  46797  sprssspr  47455  isubgredgss  47838  isubgrsubgr  47842  uhgrimisgrgriclem  47903  stgrnbgr0  47936  uspgrlimlem3  47962  linc1  48387  iinfssc  49019  discsubc  49026  idfullsubc  49123