Theorem eqsstrd 4033

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

Syntax hints:   → wi 4   = wceq 1536   ⊆ wss 3962

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-cleq 2726  df-ss 3979

This theorem is referenced by:  eqsstrrd  4034  eqsstrdi  4049  fpr2g  7230  tfisi  7879  suppssof1  8222  suppss2  8223  onfununi  8379  oawordeulem  8590  oeeui  8638  nnawordex  8673  oaabslem  8683  oaabs2  8685  omabslem  8686  omabs  8687  cofonr  8710  pw2f1olem  9114  fodomr  9166  fodomfir  9365  fival  9449  dffi3  9468  ordtypelem7  9561  ordtypelem8  9562  wemapso2lem  9589  cantnflt2  9710  cantnflem1  9726  tcss  9781  tcel  9782  r1val1  9823  rankuni2b  9890  tcrank  9921  cardonle  9994  harval2  10034  ackbij2  10279  cfub  10286  cflecard  10290  cfflb  10296  isf32lem8  10397  itunitc1  10457  ttukeylem7  10552  fpwwe2lem8  10675  wuncss  10782  wuncval2  10784  grur1a  10856  trclfvub  15042  cotrtrclfv  15047  relexpfld  15084  rtrclreclem4  15096  limsupgre  15513  isercolllem3  15699  4sqlem19  16996  vdwlem1  17014  vdwlem12  17025  ramub1lem1  17059  setsstruct2  17207  ressress  17293  imasaddfnlem  17574  imasaddflem  17576  imasvscafn  17583  imasvscaf  17585  imasless  17586  isohom  17823  ressffth  17991  acsfiindd  18610  acsmap2d  18612  dirref  18658  mndind  18853  f1omvdco2  19480  pmtrfrn  19490  symgsssg  19499  symggen  19502  psgnunilem1  19525  sylow2alem2  19650  lsmssv  19675  smndlsmidm  19688  gsumzres  19941  dprdlub  20060  dprdf1  20067  dprdsn  20070  dprdcntz2  20072  dprd2dlem1  20075  dprd2da  20076  dmdprdsplit2lem  20079  ablfac1eu  20107  rgspnmin  20631  drnglpir  21359  znleval  21590  evpmss  21621  frlmsplit2  21810  f1lindf  21859  issubassa2  21929  mplsubglem  22036  evlslem4  22117  evlseu  22124  mhpaddcl  22172  mhpinvcl  22173  psdmul  22187  lpsscls  23164  tgrest  23182  resttopon  23184  rest0  23192  restfpw  23202  ordtrest  23225  ordtrest2  23227  lmcnp  23327  tgcmp  23424  uncmp  23426  hauscmplem  23429  1stcfb  23468  2ndcdisj  23479  dissnref  23551  kgencmp  23568  xkouni  23622  prdstopn  23651  txtube  23663  txcmplem2  23665  xkoptsub  23677  xkopt  23678  xkococnlem  23682  qtoprest  23740  imastopn  23743  kqdisj  23755  reghmph  23816  nrmhmph  23817  fbssfi  23860  trfilss  23912  trfg  23914  elfm3  23973  alexsubALTlem3  24072  alexsubALT  24074  cnextf  24089  cnextcn  24090  clsnsg  24133  tgpconncompeqg  24135  qustgphaus  24146  trust  24253  ustuqtop3  24267  neipcfilu  24320  metequiv2  24538  prdsxmslem2  24557  metustfbas  24585  icccmplem1  24857  metdstri  24886  pi1addf  25093  pi1addval  25094  caubl  25355  caublcls  25356  relcmpcmet  25365  minveclem4  25479  hlhil  25490  ovolficcss  25517  uniioombllem3a  25632  uniioombllem3  25633  dyadss  25642  opnmbllem  25649  i1fima2  25727  limcfval  25921  dvfval  25946  dvnres  25981  dvivth  26063  lhop  26069  taylf  26416  xrlimcnp  27025  jensen  27046  ppisval  27161  chtlepsi  27264  chpub  27278  noextend  27725  nosupbday  27764  noinfbday  27779  scutun12  27869  scutbdaybnd  27874  scutbdaybnd2  27875  scutbdaylt  27877  cofcut1  27968  cofcutr  27972  addsbday  28064  negsbdaylem  28102  precsexlem8  28252  noseqind  28312  n0sbday  28368  pw2bday  28432  iscgrglt  28536  chssoc  31524  mdsl0  32338  mdexchi  32363  atcvat3i  32424  dmdbr5ati  32450  funimass4f  32653  xrofsup  32777  swrdrn2  32923  gsumpart  33042  pmtrcnel  33091  tocycfvres1  33112  tocycfvres2  33113  cycpmco2lem6  33133  cycpmconjvlem  33143  cycpmconjslem2  33157  fldgenssv  33296  fldgenssp  33299  nsgmgc  33419  idlsrgmulrss1  33518  idlsrgmulrss2  33519  fedgmullem1  33656  fedgmullem2  33657  constrsscn  33744  constrmon  33748  ist0cld  33793  locfinreflem  33800  cmpcref  33810  zarcls0  33828  zarclsiin  33831  zarcmplem  33841  cnvordtrestixx  33873  ordtrestNEW  33881  ordtrest2NEW  33883  pnfneige0  33911  sigagenss  34129  imambfm  34243  dya2iocress  34255  dya2icoseg  34258  dya2iocucvr  34265  ballotlemro  34503  ftc2re  34591  bnj1097  34973  bnj1452  35044  cvmlift3lem6  35308  msubrn  35513  mclsssv  35548  mclsind  35554  liness  36126  neibastop2lem  36342  opnmbllem0  37642  mblfinlem2  37644  isbndx  37768  isbnd2  37769  ssbnd  37774  heiborlem3  37799  igenmin  38050  lsatlss  38977  lsmsat  38989  lsatfixedN  38990  lssats  38993  lpssat  38994  lssatle  38996  lssat  38997  lsatcvat3  39033  paddssat  39796  paddasslem17  39818  pmodlem2  39829  hlmod1i  39838  pl42lem4N  39964  diassdvaN  41042  dia2dimlem10  41055  cdlemn4a  41181  cdlemn5pre  41182  dihord5apre  41244  lclkrlem2e  41493  lclkrlem2p  41504  lclkrlem2v  41510  lclkrslem2  41520  lclkrs  41521  lcfrlem25  41549  lcfrlem35  41559  mapdval2N  41612  mapdpglem8  41661  mapdpglem13  41666  baerlem3lem2  41692  mapdindp2  41703  hdmap11lem2  41824  primrootspoweq0  42087  aks6d1c6lem2  42152  evlsmhpvvval  42581  prjspnssbas  42607  elrfi  42681  isnacs3  42697  mzpf  42723  mzpindd  42733  diophrw  42746  eldiophss  42761  rmxyelqirrOLD  42898  pw2f1ocnv  43025  aomclem6  43047  hbt  43118  oasubex  43275  oaabsb  43283  nnoeomeqom  43301  omcl2  43322  naddgeoa  43383  naddwordnexlem4  43390  oaltom  43394  omltoe  43396  minregex  43523  cnvssb  43575  trclubgNEW  43607  dfrcl2  43663  fvmptiunrelexplb0da  43674  relexp0a  43705  cotrcltrcl  43714  trclimalb2  43715  cotrclrcl  43731  isotone2  44038  k0004ss1  44140  fnresdmss  45110  mptelpm  45118  ssnnf1octb  45136  uzfissfz  45275  iuneqfzuzlem  45283  xlimliminflimsup  45817  icccncfext  45842  dvnprodlem2  45902  dvnprodlem3  45903  fourierdlem41  46103  fourierdlem70  46131  fourierdlem71  46132  fourierdlem80  46141  fourierdlem113  46174  ioorrnopnlem  46259  ioorrnopnxrlem  46261  salgenss  46291  dfsalgen2  46296  subsaliuncllem  46312  iundjiun  46415  meadjiunlem  46420  meaiunlelem  46423  meaiuninclem  46435  meaiininclem  46441  omeunle  46471  carageniuncllem2  46477  caratheodorylem1  46481  caratheodorylem2  46482  hoissre  46499  ovnsubaddlem1  46525  hoidmvlelem3  46552  ovnhoilem1  46556  ovnhoilem2  46557  ovnhoi  46558  ovncvr2  46566  voncmpl  46576  hspmbllem2  46582  hspmbl  46584  opnvonmbllem1  46587  vonmblss  46595  ovnsubadd2lem  46600  vonioolem2  46636  preimageiingt  46675  preimaleiinlt  46676  issmfd  46690  issmfdf  46692  sssmf  46693  cnfsmf  46695  issmfled  46712  issmfgtd  46716  smfadd  46720  smfrec  46744  smfmul  46750  smfmulc1  46751  smfpimbor1lem2  46754  smfsuplem1  46766  smflimsuplem1  46775  smflimsuplem7  46781  sprssspr  47405  isubgredgss  47788  isubgrsubgr  47792  uspgrimprop  47810  uhgrimisgrgriclem  47835  stgrnbgr0  47866  uspgrlimlem3  47892  linc1  48270