Theorem eqsstrd 3957

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

Syntax hints:   → wi 4   = wceq 1542   ⊆ wss 3890

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-ss 3907

This theorem is referenced by:  eqsstrrd  3958  eqsstrdi  3967  3sstr4d  3978  fpr2g  7159  tfisi  7803  suppssof1  8142  suppss2  8143  onfununi  8274  oawordeulem  8482  oeeui  8531  nnawordex  8566  oaabslem  8576  oaabs2  8578  omabslem  8579  omabs  8580  cofonr  8603  pw2f1olem  9012  fodomr  9059  fodomfir  9231  fival  9318  dffi3  9337  ordtypelem7  9432  ordtypelem8  9433  wemapso2lem  9460  cantnflt2  9585  cantnflem1  9601  tcss  9654  tcel  9655  r1val1  9701  rankuni2b  9768  tcrank  9799  cardonle  9872  harval2  9912  ackbij2  10155  cfub  10162  cflecard  10166  cfflb  10172  isf32lem8  10273  itunitc1  10333  ttukeylem7  10428  fpwwe2lem8  10552  wuncss  10659  wuncval2  10661  grur1a  10733  trclfvub  14960  cotrtrclfv  14965  relexpfld  15002  rtrclreclem4  15014  limsupgre  15434  isercolllem3  15620  4sqlem19  16925  vdwlem1  16943  vdwlem12  16954  ramub1lem1  16988  setsstruct2  17135  ressress  17208  imasaddfnlem  17483  imasaddflem  17485  imasvscafn  17492  imasvscaf  17494  imasless  17495  isohom  17734  ressffth  17898  acsfiindd  18510  acsmap2d  18512  dirref  18558  mndind  18787  f1omvdco2  19414  pmtrfrn  19424  symgsssg  19433  symggen  19436  psgnunilem1  19459  sylow2alem2  19584  lsmssv  19609  smndlsmidm  19622  gsumzres  19875  dprdlub  19994  dprdf1  20001  dprdsn  20004  dprdcntz2  20006  dprd2dlem1  20009  dprd2da  20010  dmdprdsplit2lem  20013  ablfac1eu  20041  rgspnmin  20583  drnglpir  21322  znleval  21544  evpmss  21576  frlmsplit2  21763  f1lindf  21812  issubassa2  21882  mplsubglem  21987  evlslem4  22064  evlseu  22071  mhpaddcl  22127  mhpinvcl  22128  psdmul  22142  lpsscls  23116  tgrest  23134  resttopon  23136  rest0  23144  restfpw  23154  ordtrest  23177  ordtrest2  23179  lmcnp  23279  tgcmp  23376  uncmp  23378  hauscmplem  23381  1stcfb  23420  2ndcdisj  23431  dissnref  23503  kgencmp  23520  xkouni  23574  prdstopn  23603  txtube  23615  txcmplem2  23617  xkoptsub  23629  xkopt  23630  xkococnlem  23634  qtoprest  23692  imastopn  23695  kqdisj  23707  reghmph  23768  nrmhmph  23769  fbssfi  23812  trfilss  23864  trfg  23866  elfm3  23925  alexsubALTlem3  24024  alexsubALT  24026  cnextf  24041  cnextcn  24042  clsnsg  24085  tgpconncompeqg  24087  qustgphaus  24098  trust  24204  ustuqtop3  24218  neipcfilu  24270  metequiv2  24485  prdsxmslem2  24504  metustfbas  24532  icccmplem1  24798  metdstri  24827  pi1addf  25024  pi1addval  25025  caubl  25285  caublcls  25286  relcmpcmet  25295  minveclem4  25409  hlhil  25420  ovolficcss  25446  uniioombllem3a  25561  uniioombllem3  25562  dyadss  25571  opnmbllem  25578  i1fima2  25656  limcfval  25849  dvfval  25874  dvnres  25908  dvivth  25987  lhop  25993  taylf  26337  xrlimcnp  26945  jensen  26966  ppisval  27081  chtlepsi  27183  chpub  27197  noextend  27644  nosupbday  27683  noinfbday  27698  cutsun12  27796  cutbdaybnd  27801  cutbdaybnd2  27802  cutbdaylt  27804  sltsbday  27923  cofcut1  27926  cofcutr  27930  addbday  28024  negbdaylem  28062  precsexlem8  28220  bdayons  28282  onsbnd2  28288  noseqind  28298  n0bday  28358  bdaypw2n0bndlem  28469  iscgrglt  28596  cyclnumvtx  29883  chssoc  31582  mdsl0  32396  mdexchi  32421  atcvat3i  32482  dmdbr5ati  32508  funimass4f  32725  xrofsup  32855  swrdrn2  33029  gsumpart  33139  pmtrcnel  33165  tocycfvres1  33186  tocycfvres2  33187  cycpmco2lem6  33207  cycpmconjvlem  33217  cycpmconjslem2  33231  elrgspnsubrunlem2  33324  fldgenssv  33391  fldgenssp  33394  nsgmgc  33487  idlsrgmulrss1  33586  idlsrgmulrss2  33587  esplyfval1  33732  esplyfvaln  33733  esplyind  33734  fedgmullem1  33789  fedgmullem2  33790  constrsscn  33900  constrmon  33904  ist0cld  33993  locfinreflem  34000  cmpcref  34010  zarcls0  34028  zarclsiin  34031  zarcmplem  34041  cnvordtrestixx  34073  ordtrestNEW  34081  ordtrest2NEW  34083  pnfneige0  34111  sigagenss  34309  imambfm  34422  dya2iocress  34434  dya2icoseg  34437  dya2iocucvr  34444  ballotlemro  34683  ftc2re  34758  bnj1097  35139  bnj1452  35210  cvmlift3lem6  35522  msubrn  35727  mclsssv  35762  mclsind  35768  liness  36343  neibastop2lem  36558  ttcmin  36694  dfttc3gw  36721  opnmbllem0  37991  mblfinlem2  37993  isbndx  38117  isbnd2  38118  ssbnd  38123  heiborlem3  38148  igenmin  38399  lsatlss  39456  lsmsat  39468  lsatfixedN  39469  lssats  39472  lpssat  39473  lssatle  39475  lssat  39476  lsatcvat3  39512  paddssat  40274  paddasslem17  40296  pmodlem2  40307  hlmod1i  40316  pl42lem4N  40442  diassdvaN  41520  dia2dimlem10  41533  cdlemn4a  41659  cdlemn5pre  41660  dihord5apre  41722  lclkrlem2e  41971  lclkrlem2p  41982  lclkrlem2v  41988  lclkrslem2  41998  lclkrs  41999  lcfrlem25  42027  lcfrlem35  42037  mapdval2N  42090  mapdpglem8  42139  mapdpglem13  42144  baerlem3lem2  42170  mapdindp2  42181  hdmap11lem2  42302  primrootspoweq0  42559  aks6d1c6lem2  42624  evlsmhpvvval  43042  prjspnssbas  43068  elrfi  43140  isnacs3  43156  mzpf  43182  mzpindd  43192  diophrw  43205  eldiophss  43220  pw2f1ocnv  43483  aomclem6  43505  hbt  43576  oasubex  43732  oaabsb  43740  nnoeomeqom  43758  omcl2  43779  naddgeoa  43840  naddwordnexlem4  43847  oaltom  43850  omltoe  43852  minregex  43979  cnvssb  44031  trclubgNEW  44063  dfrcl2  44119  fvmptiunrelexplb0da  44130  relexp0a  44161  cotrcltrcl  44170  trclimalb2  44171  cotrclrcl  44187  isotone2  44494  k0004ss1  44596  fnresdmss  45616  mptelpm  45624  ssnnf1octb  45642  uzfissfz  45774  iuneqfzuzlem  45782  xlimliminflimsup  46308  icccncfext  46333  dvnprodlem2  46393  dvnprodlem3  46394  fourierdlem41  46594  fourierdlem70  46622  fourierdlem71  46623  fourierdlem80  46632  fourierdlem113  46665  ioorrnopnlem  46750  ioorrnopnxrlem  46752  salgenss  46782  dfsalgen2  46787  subsaliuncllem  46803  iundjiun  46906  meadjiunlem  46911  meaiunlelem  46914  meaiuninclem  46926  meaiininclem  46932  omeunle  46962  carageniuncllem2  46968  caratheodorylem1  46972  caratheodorylem2  46973  hoissre  46990  ovnsubaddlem1  47016  hoidmvlelem3  47043  ovnhoilem1  47047  ovnhoilem2  47048  ovnhoi  47049  ovncvr2  47057  voncmpl  47067  hspmbllem2  47073  hspmbl  47075  opnvonmbllem1  47078  vonmblss  47086  ovnsubadd2lem  47091  vonioolem2  47127  preimaleiinlt  47167  issmfd  47181  issmfdf  47183  sssmf  47184  cnfsmf  47186  issmfled  47203  issmfgtd  47207  smfadd  47211  smfrec  47235  smfmul  47241  smfmulc1  47242  smfpimbor1lem2  47245  smfsuplem1  47257  smflimsuplem1  47266  smflimsuplem7  47272  sprssspr  47953  isubgredgss  48353  isubgrsubgr  48357  uhgrimisgrgriclem  48418  stgrnbgr0  48452  uspgrlimlem3  48478  linc1  48913  iinfssc  49544  discsubc  49551  idfullsubc  49648