Theorem eqsstrd 3970

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

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

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 3920

This theorem is referenced by:  eqsstrrd  3971  eqsstrdi  3980  3sstr4d  3991  fpr2g  7167  tfisi  7811  suppssof1  8151  suppss2  8152  onfununi  8283  oawordeulem  8491  oeeui  8540  nnawordex  8575  oaabslem  8585  oaabs2  8587  omabslem  8588  omabs  8589  cofonr  8612  pw2f1olem  9021  fodomr  9068  fodomfir  9240  fival  9327  dffi3  9346  ordtypelem7  9441  ordtypelem8  9442  wemapso2lem  9469  cantnflt2  9594  cantnflem1  9610  tcss  9663  tcel  9664  r1val1  9710  rankuni2b  9777  tcrank  9808  cardonle  9881  harval2  9921  ackbij2  10164  cfub  10171  cflecard  10175  cfflb  10181  isf32lem8  10282  itunitc1  10342  ttukeylem7  10437  fpwwe2lem8  10561  wuncss  10668  wuncval2  10670  grur1a  10742  trclfvub  14942  cotrtrclfv  14947  relexpfld  14984  rtrclreclem4  14996  limsupgre  15416  isercolllem3  15602  4sqlem19  16903  vdwlem1  16921  vdwlem12  16932  ramub1lem1  16966  setsstruct2  17113  ressress  17186  imasaddfnlem  17461  imasaddflem  17463  imasvscafn  17470  imasvscaf  17472  imasless  17473  isohom  17712  ressffth  17876  acsfiindd  18488  acsmap2d  18490  dirref  18536  mndind  18765  f1omvdco2  19389  pmtrfrn  19399  symgsssg  19408  symggen  19411  psgnunilem1  19434  sylow2alem2  19559  lsmssv  19584  smndlsmidm  19597  gsumzres  19850  dprdlub  19969  dprdf1  19976  dprdsn  19979  dprdcntz2  19981  dprd2dlem1  19984  dprd2da  19985  dmdprdsplit2lem  19988  ablfac1eu  20016  rgspnmin  20560  drnglpir  21299  znleval  21521  evpmss  21553  frlmsplit2  21740  f1lindf  21789  issubassa2  21860  mplsubglem  21966  evlslem4  22043  evlseu  22050  mhpaddcl  22106  mhpinvcl  22107  psdmul  22121  lpsscls  23097  tgrest  23115  resttopon  23117  rest0  23125  restfpw  23135  ordtrest  23158  ordtrest2  23160  lmcnp  23260  tgcmp  23357  uncmp  23359  hauscmplem  23362  1stcfb  23401  2ndcdisj  23412  dissnref  23484  kgencmp  23501  xkouni  23555  prdstopn  23584  txtube  23596  txcmplem2  23598  xkoptsub  23610  xkopt  23611  xkococnlem  23615  qtoprest  23673  imastopn  23676  kqdisj  23688  reghmph  23749  nrmhmph  23750  fbssfi  23793  trfilss  23845  trfg  23847  elfm3  23906  alexsubALTlem3  24005  alexsubALT  24007  cnextf  24022  cnextcn  24023  clsnsg  24066  tgpconncompeqg  24068  qustgphaus  24079  trust  24185  ustuqtop3  24199  neipcfilu  24251  metequiv2  24466  prdsxmslem2  24485  metustfbas  24513  icccmplem1  24779  metdstri  24808  pi1addf  25015  pi1addval  25016  caubl  25276  caublcls  25277  relcmpcmet  25286  minveclem4  25400  hlhil  25411  ovolficcss  25438  uniioombllem3a  25553  uniioombllem3  25554  dyadss  25563  opnmbllem  25570  i1fima2  25648  limcfval  25841  dvfval  25866  dvnres  25901  dvivth  25983  lhop  25989  taylf  26336  xrlimcnp  26946  jensen  26967  ppisval  27082  chtlepsi  27185  chpub  27199  noextend  27646  nosupbday  27685  noinfbday  27700  cutsun12  27798  cutbdaybnd  27803  cutbdaybnd2  27804  cutbdaylt  27806  sltsbday  27925  cofcut1  27928  cofcutr  27932  addbday  28026  negbdaylem  28064  precsexlem8  28222  bdayons  28284  onsbnd2  28290  noseqind  28300  n0bday  28360  bdaypw2n0bndlem  28471  iscgrglt  28598  cyclnumvtx  29885  chssoc  31584  mdsl0  32398  mdexchi  32423  atcvat3i  32484  dmdbr5ati  32510  funimass4f  32727  xrofsup  32858  swrdrn2  33047  gsumpart  33157  pmtrcnel  33183  tocycfvres1  33204  tocycfvres2  33205  cycpmco2lem6  33225  cycpmconjvlem  33235  cycpmconjslem2  33249  elrgspnsubrunlem2  33342  fldgenssv  33409  fldgenssp  33412  nsgmgc  33505  idlsrgmulrss1  33604  idlsrgmulrss2  33605  esplyfval1  33750  esplyfvaln  33751  esplyind  33752  fedgmullem1  33807  fedgmullem2  33808  constrsscn  33918  constrmon  33922  ist0cld  34011  locfinreflem  34018  cmpcref  34028  zarcls0  34046  zarclsiin  34049  zarcmplem  34059  cnvordtrestixx  34091  ordtrestNEW  34099  ordtrest2NEW  34101  pnfneige0  34129  sigagenss  34327  imambfm  34440  dya2iocress  34452  dya2icoseg  34455  dya2iocucvr  34462  ballotlemro  34701  ftc2re  34776  bnj1097  35157  bnj1452  35228  cvmlift3lem6  35540  msubrn  35745  mclsssv  35780  mclsind  35786  liness  36361  neibastop2lem  36576  opnmbllem0  37907  mblfinlem2  37909  isbndx  38033  isbnd2  38034  ssbnd  38039  heiborlem3  38064  igenmin  38315  lsatlss  39372  lsmsat  39384  lsatfixedN  39385  lssats  39388  lpssat  39389  lssatle  39391  lssat  39392  lsatcvat3  39428  paddssat  40190  paddasslem17  40212  pmodlem2  40223  hlmod1i  40232  pl42lem4N  40358  diassdvaN  41436  dia2dimlem10  41449  cdlemn4a  41575  cdlemn5pre  41576  dihord5apre  41638  lclkrlem2e  41887  lclkrlem2p  41898  lclkrlem2v  41904  lclkrslem2  41914  lclkrs  41915  lcfrlem25  41943  lcfrlem35  41953  mapdval2N  42006  mapdpglem8  42055  mapdpglem13  42060  baerlem3lem2  42086  mapdindp2  42097  hdmap11lem2  42218  primrootspoweq0  42476  aks6d1c6lem2  42541  evlsmhpvvval  42953  prjspnssbas  42979  elrfi  43051  isnacs3  43067  mzpf  43093  mzpindd  43103  diophrw  43116  eldiophss  43131  pw2f1ocnv  43394  aomclem6  43416  hbt  43487  oasubex  43643  oaabsb  43651  nnoeomeqom  43669  omcl2  43690  naddgeoa  43751  naddwordnexlem4  43758  oaltom  43761  omltoe  43763  minregex  43890  cnvssb  43942  trclubgNEW  43974  dfrcl2  44030  fvmptiunrelexplb0da  44041  relexp0a  44072  cotrcltrcl  44081  trclimalb2  44082  cotrclrcl  44098  isotone2  44405  k0004ss1  44507  fnresdmss  45527  mptelpm  45535  ssnnf1octb  45553  uzfissfz  45685  iuneqfzuzlem  45693  xlimliminflimsup  46220  icccncfext  46245  dvnprodlem2  46305  dvnprodlem3  46306  fourierdlem41  46506  fourierdlem70  46534  fourierdlem71  46535  fourierdlem80  46544  fourierdlem113  46577  ioorrnopnlem  46662  ioorrnopnxrlem  46664  salgenss  46694  dfsalgen2  46699  subsaliuncllem  46715  iundjiun  46818  meadjiunlem  46823  meaiunlelem  46826  meaiuninclem  46838  meaiininclem  46844  omeunle  46874  carageniuncllem2  46880  caratheodorylem1  46884  caratheodorylem2  46885  hoissre  46902  ovnsubaddlem1  46928  hoidmvlelem3  46955  ovnhoilem1  46959  ovnhoilem2  46960  ovnhoi  46961  ovncvr2  46969  voncmpl  46979  hspmbllem2  46985  hspmbl  46987  opnvonmbllem1  46990  vonmblss  46998  ovnsubadd2lem  47003  vonioolem2  47039  preimaleiinlt  47079  issmfd  47093  issmfdf  47095  sssmf  47096  cnfsmf  47098  issmfled  47115  issmfgtd  47119  smfadd  47123  smfrec  47147  smfmul  47153  smfmulc1  47154  smfpimbor1lem2  47157  smfsuplem1  47169  smflimsuplem1  47178  smflimsuplem7  47184  sprssspr  47841  isubgredgss  48225  isubgrsubgr  48229  uhgrimisgrgriclem  48290  stgrnbgr0  48324  uspgrlimlem3  48350  linc1  48785  iinfssc  49416  discsubc  49423  idfullsubc  49520