Theorem eqsstrd 3965

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

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

This theorem is used by:  eqsstrrd  3966  eqsstrdi  3975  3sstr4d  3986  fpr2g  7215  tfisi  7868  suppssof1  8209  suppss2  8210  onfununi  8342  oawordeulem  8555  oeeui  8604  nnawordex  8639  oaabslem  8649  oaabs2  8651  omabslem  8652  omabs  8653  cofonr  8676  pw2f1olem  9093  fodomr  9140  fodomfir  9312  fival  9397  dffi3  9416  ordtypelem7  9511  ordtypelem8  9512  wemapso2lem  9539  cantnflt2  9667  cantnflem1  9683  tcss  9736  tcel  9737  r1val1  9786  rankuni2b  9860  tcrank  9894  cardonle  10031  harval2  10071  ackbij2  10313  cfub  10319  cflecard  10323  cfflb  10330  isf32lem8  10431  itunitc1  10491  ttukeylem7  10586  fpwwe2lem8  10716  wuncss  10823  wuncval2  10825  grur1a  10897  trclfvub  15153  cotrtrclfv  15158  relexpfld  15195  rtrclreclem4  15207  limsupgre  15641  isercolllem3  15827  4sqlem19  17134  vdwlem1  17152  vdwlem12  17163  ramub1lem1  17197  setsstruct2  17345  ressress  17418  imasaddfnlem  17693  imasaddflem  17695  imasvscafn  17702  imasvscaf  17704  imasless  17705  isohom  17944  ressffth  18108  acsfiindd  18720  acsmap2d  18722  dirref  18768  mndind  19017  f1omvdco2  19655  pmtrfrn  19665  symgsssg  19674  symggen  19677  psgnunilem1  19700  sylow2alem2  19825  lsmssv  19850  smndlsmidm  19863  gsumzres  20116  dprdlub  20235  dprdf1  20242  dprdsn  20245  dprdcntz2  20247  dprd2dlem1  20250  dprd2da  20251  dmdprdsplit2lem  20254  ablfac1eu  20282  rgspnmin  20860  drnglpir  21649  znleval  21853  evpmss  21885  frlmsplit2  22072  f1lindf  22121  issubassa2  22193  mplsubglem  22299  evlslem4  22378  evlseu  22385  mhpaddcl  22465  mhpinvcl  22466  psdmul  22480  lpsscls  23452  tgrest  23470  resttopon  23472  rest0  23480  restfpw  23490  ordtrest  23513  ordtrest2  23515  lmcnp  23615  tgcmp  23712  uncmp  23714  hauscmplem  23717  1stcfb  23756  2ndcdisj  23768  dissnref  23840  kgencmp  23857  xkouni  23911  prdstopn  23940  txtube  23952  txcmplem2  23954  xkoptsub  23966  xkopt  23967  xkococnlem  23971  qtoprest  24029  imastopn  24032  kqdisj  24044  reghmph  24105  nrmhmph  24106  fbssfi  24149  trfilss  24201  trfg  24203  elfm3  24262  alexsubALTlem3  24361  alexsubALT  24363  cnextf  24378  cnextcn  24379  clsnsg  24422  tgpconncompeqg  24424  qustgphaus  24435  trust  24541  ustuqtop3  24555  neipcfilu  24607  metequiv2  24822  prdsxmslem2  24841  metustfbas  24869  icccmplem1  25135  metdstri  25164  pi1addf  25361  pi1addval  25362  caubl  25622  caublcls  25623  relcmpcmet  25632  minveclem4  25746  hlhil  25757  ovolficcss  25783  uniioombllem3a  25898  uniioombllem3  25899  dyadss  25908  opnmbllem  25915  i1fima2  25993  limcfval  26185  dvfval  26210  dvnres  26244  dvivth  26323  lhop  26329  taylf  26681  xrlimcnp  27289  jensen  27309  ppisval  27424  chtlepsi  27526  chpub  27540  noextend  28016  nosupbday  28055  noinfbday  28070  cutsun12  28169  cutbdaybnd  28174  cutbdaybnd2  28175  cutbdaylt  28177  sltsbday  28296  cofcut1  28299  cofcutr  28303  addbday  28397  negbdaylem  28435  precsexlem8  28593  bdayons  28655  onsbnd2  28661  noseqind  28671  n0bday  28731  bdaypw2n0bndlem  28842  iscgrglt  28970  cyclnumvtx  30381  chssoc  32091  mdsl0  32905  mdexchi  32930  atcvat3i  32991  dmdbr5ati  33017  funimass4f  33224  xrofsup  33352  swrdrn2  33510  gsumpart  33617  pmtrcnel  33643  tocycfvres1  33664  tocycfvres2  33665  cycpmco2lem6  33685  cycpmconjvlem  33695  cycpmconjslem2  33709  elrgspnsubrunlem2  33802  fldgenssv  33870  fldgenssp  33873  nsgmgc  33956  idlsrgmulrss1  34036  idlsrgmulrss2  34037  esplyfval1  34198  esplyfvaln  34199  esplyind  34200  fedgmullem1  34254  fedgmullem2  34255  constrsscn  34365  constrmon  34369  ist0cld  34458  locfinreflem  34465  cmpcref  34475  zarcls0  34493  zarclsiin  34496  zarcmplem  34506  cnvordtrestixx  34538  ordtrestNEW  34546  ordtrest2NEW  34548  pnfneige0  34576  sigagenss  34775  imambfm  34887  dya2iocress  34899  dya2icoseg  34902  dya2iocucvr  34909  ballotlemro  35148  ftc2re  35220  bnj1097  35604  bnj1452  35675  rankscottu  35741  cvmlift3lem6  36068  msubrn  36273  mclsssv  36308  mclsind  36314  liness  36890  neibastop2lem  37128  ttcmin  37264  dfttc3gw  37291  opnmbllem0  38554  mblfinlem2  38556  isbndx  38696  isbnd2  38697  ssbnd  38702  heiborlem3  38727  igenmin  38978  lsatlss  40033  lsmsat  40045  lsatfixedN  40046  lssats  40049  lpssat  40050  lssatle  40052  lssat  40053  lsatcvat3  40089  paddssat  40851  paddasslem17  40873  pmodlem2  40884  hlmod1i  40893  pl42lem4N  41019  diassdvaN  42097  dia2dimlem10  42110  cdlemn4a  42236  cdlemn5pre  42237  dihord5apre  42299  lclkrlem2e  42548  lclkrlem2p  42559  lclkrlem2v  42565  lclkrslem2  42575  lclkrs  42576  lcfrlem25  42604  lcfrlem35  42614  mapdval2N  42667  mapdpglem8  42716  mapdpglem13  42721  baerlem3lem2  42747  mapdindp2  42758  hdmap11lem2  42879  primrootspoweq0  43136  aks6d1c6lem2  43201  evlsmhpvvval  43603  prjspnssbas  43629  elrfi  43684  isnacs3  43700  mzpf  43726  mzpindd  43736  diophrw  43749  eldiophss  43764  pw2f1ocnv  44023  aomclem6  44045  hbt  44116  oasubex  44272  oaabsb  44280  nnoeomeqom  44298  omcl2  44319  naddgeoa  44380  naddwordnexlem4  44387  oaltom  44390  omltoe  44392  minregex  44519  cnvssb  44571  trclubgNEW  44603  dfrcl2  44659  fvmptiunrelexplb0da  44670  relexp0a  44701  cotrcltrcl  44710  trclimalb2  44711  cotrclrcl  44727  isotone2  45034  k0004ss1  45136  fnresdmss  46152  mptelpm  46160  ssnnf1octb  46178  uzfissfz  46307  iuneqfzuzlem  46315  xlimliminflimsup  46841  icccncfext  46866  dvnprodlem2  46926  dvnprodlem3  46927  fourierdlem41  47127  fourierdlem70  47155  fourierdlem71  47156  fourierdlem80  47165  ioorrnopnlem  47283  ioorrnopnxrlem  47285  salgenss  47315  dfsalgen2  47320  subsaliuncllem  47336  iundjiun  47439  meadjiunlem  47444  meaiunlelem  47447  meaiuninclem  47459  meaiininclem  47465  omeunle  47495  carageniuncllem2  47501  caratheodorylem1  47505  caratheodorylem2  47506  hoissre  47523  ovnsubaddlem1  47549  hoidmvlelem3  47576  ovnhoilem1  47580  ovnhoilem2  47581  ovnhoi  47582  ovncvr2  47590  voncmpl  47600  hspmbllem2  47606  hspmbl  47608  opnvonmbllem1  47611  vonmblss  47619  ovnsubadd2lem  47624  vonioolem2  47660  preimaleiinlt  47700  issmfd  47714  issmfdf  47716  cnfsmf  47719  issmfled  47736  issmfgtd  47740  smfadd  47744  smfrec  47768  smfmul  47774  smfmulc1  47775  smfpimbor1lem2  47778  smfsuplem1  47790  smflimsuplem1  47799  smflimsuplem7  47805  tmachlem-uassst  47922  sprssspr  48532  isubgredgss  48932  isubgrsubgr  48936  uhgrimisgrgriclem  48997  stgrnbgr0  49031  uspgrlimlem3  49057  linc1  49506  iinfssc  50134  discsubc  50141  idfullsubc  50238