Theorem eqsstrd 3985

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

Syntax hints:   → wi 4   = wceq 1541   ⊆ wss 3913

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3448  df-in 3920  df-ss 3930

This theorem is referenced by:  eqsstrrd  3986  eqsstrdi  4001  fpr2g  7166  tfisi  7800  suppssof1  8135  suppss2  8136  onfununi  8292  oawordeulem  8506  oeeui  8554  nnawordex  8589  oaabslem  8598  oaabs2  8600  omabslem  8601  omabs  8602  cofonr  8625  pw2f1olem  9027  fodomr  9079  fival  9357  dffi3  9376  ordtypelem7  9469  ordtypelem8  9470  wemapso2lem  9497  cantnflt2  9618  cantnflem1  9634  tcss  9689  tcel  9690  r1val1  9731  rankuni2b  9798  tcrank  9829  cardonle  9902  harval2  9942  ackbij2  10188  cfub  10194  cflecard  10198  cfflb  10204  isf32lem8  10305  itunitc1  10365  ttukeylem7  10460  fpwwe2lem8  10583  wuncss  10690  wuncval2  10692  grur1a  10764  trclfvub  14904  cotrtrclfv  14909  relexpfld  14946  rtrclreclem4  14958  limsupgre  15375  isercolllem3  15563  4sqlem19  16846  vdwlem1  16864  vdwlem12  16875  ramub1lem1  16909  setsstruct2  17057  ressress  17143  imasaddfnlem  17424  imasaddflem  17426  imasvscafn  17433  imasvscaf  17435  imasless  17436  isohom  17673  ressffth  17839  acsfiindd  18456  acsmap2d  18458  dirref  18504  mndind  18652  f1omvdco2  19244  pmtrfrn  19254  symgsssg  19263  symggen  19266  psgnunilem1  19289  sylow2alem2  19414  lsmssv  19439  smndlsmidm  19452  gsumzres  19700  dprdlub  19819  dprdf1  19826  dprdsn  19829  dprdcntz2  19831  dprd2dlem1  19834  dprd2da  19835  dmdprdsplit2lem  19838  ablfac1eu  19866  drnglpir  20782  znleval  20998  evpmss  21027  frlmsplit2  21216  f1lindf  21265  issubassa2  21332  mplsubglem  21442  evlslem4  21521  evlseu  21530  mhpaddcl  21578  mhpinvcl  21579  lpsscls  22529  tgrest  22547  resttopon  22549  rest0  22557  restfpw  22567  ordtrest  22590  ordtrest2  22592  lmcnp  22692  tgcmp  22789  uncmp  22791  hauscmplem  22794  1stcfb  22833  2ndcdisj  22844  dissnref  22916  kgencmp  22933  xkouni  22987  prdstopn  23016  txtube  23028  txcmplem2  23030  xkoptsub  23042  xkopt  23043  xkococnlem  23047  qtoprest  23105  imastopn  23108  kqdisj  23120  reghmph  23181  nrmhmph  23182  fbssfi  23225  trfilss  23277  trfg  23279  elfm3  23338  alexsubALTlem3  23437  alexsubALT  23439  cnextf  23454  cnextcn  23455  clsnsg  23498  tgpconncompeqg  23500  qustgphaus  23511  trust  23618  ustuqtop3  23632  neipcfilu  23685  metequiv2  23903  prdsxmslem2  23922  metustfbas  23950  icccmplem1  24222  metdstri  24251  pi1addf  24447  pi1addval  24448  caubl  24709  caublcls  24710  relcmpcmet  24719  minveclem4  24833  hlhil  24844  ovolficcss  24870  uniioombllem3a  24985  uniioombllem3  24986  dyadss  24995  opnmbllem  25002  i1fima2  25080  limcfval  25273  dvfval  25298  dvnres  25332  dvivth  25411  lhop  25417  taylf  25757  xrlimcnp  26355  jensen  26375  ppisval  26490  chtlepsi  26591  chpub  26605  noextend  27051  nosupbday  27090  noinfbday  27105  scutun12  27192  scutbdaybnd  27197  scutbdaybnd2  27198  scutbdaylt  27200  cofcut1  27282  cofcutr  27286  iscgrglt  27519  chssoc  30501  mdsl0  31315  mdexchi  31340  atcvat3i  31401  dmdbr5ati  31427  funimass4f  31618  xrofsup  31740  swrdrn2  31878  gsumpart  31967  pmtrcnel  32010  tocycfvres1  32029  tocycfvres2  32030  cycpmco2lem6  32050  cycpmconjvlem  32060  cycpmconjslem2  32074  fldgenssv  32153  fldgenssp  32156  nsgmgc  32264  idlsrgmulrss1  32329  idlsrgmulrss2  32330  fedgmullem1  32411  fedgmullem2  32412  ist0cld  32503  locfinreflem  32510  cmpcref  32520  zarcls0  32538  zarclsiin  32541  zarcmplem  32551  cnvordtrestixx  32583  ordtrestNEW  32591  ordtrest2NEW  32593  pnfneige0  32621  sigagenss  32837  imambfm  32951  dya2iocress  32963  dya2icoseg  32966  dya2iocucvr  32973  ballotlemro  33211  ftc2re  33300  bnj1097  33682  bnj1452  33753  cvmlift3lem6  34005  msubrn  34210  mclsssv  34245  mclsind  34251  liness  34806  neibastop2lem  34908  opnmbllem0  36187  mblfinlem2  36189  isbndx  36314  isbnd2  36315  ssbnd  36320  heiborlem3  36345  igenmin  36596  lsatlss  37531  lsmsat  37543  lsatfixedN  37544  lssats  37547  lpssat  37548  lssatle  37550  lssat  37551  lsatcvat3  37587  paddssat  38350  paddasslem17  38372  pmodlem2  38383  hlmod1i  38392  pl42lem4N  38518  diassdvaN  39596  dia2dimlem10  39609  cdlemn4a  39735  cdlemn5pre  39736  dihord5apre  39798  lclkrlem2e  40047  lclkrlem2p  40058  lclkrlem2v  40064  lclkrslem2  40074  lclkrs  40075  lcfrlem25  40103  lcfrlem35  40113  mapdval2N  40166  mapdpglem8  40215  mapdpglem13  40220  baerlem3lem2  40246  mapdindp2  40257  hdmap11lem2  40378  prjspnssbas  41017  elrfi  41075  isnacs3  41091  mzpf  41117  mzpindd  41127  diophrw  41140  eldiophss  41155  rmxyelqirrOLD  41292  pw2f1ocnv  41419  aomclem6  41444  hbt  41515  rgspnmin  41556  oasubex  41679  oaabsb  41687  nnoeomeqom  41705  omcl2  41726  naddgeoa  41788  naddwordnexlem4  41795  oaltom  41799  omltoe  41801  minregex  41928  cnvssb  41980  trclubgNEW  42012  dfrcl2  42068  fvmptiunrelexplb0da  42079  relexp0a  42110  cotrcltrcl  42119  trclimalb2  42120  cotrclrcl  42136  isotone2  42443  k0004ss1  42545  fnresdmss  43507  mptelpm  43515  ssnnf1octb  43536  uzfissfz  43681  iuneqfzuzlem  43689  xlimliminflimsup  44223  icccncfext  44248  dvnprodlem1  44307  dvnprodlem2  44308  dvnprodlem3  44309  fourierdlem41  44509  fourierdlem70  44537  fourierdlem71  44538  fourierdlem80  44547  fourierdlem113  44580  ioorrnopnlem  44665  ioorrnopnxrlem  44667  salgenss  44697  dfsalgen2  44702  subsaliuncllem  44718  iundjiun  44821  meadjiunlem  44826  meaiunlelem  44829  meaiuninclem  44841  meaiininclem  44847  omeunle  44877  carageniuncllem2  44883  caratheodorylem1  44887  caratheodorylem2  44888  hoissre  44905  ovnsubaddlem1  44931  hoidmvlelem3  44958  ovnhoilem1  44962  ovnhoilem2  44963  ovnhoi  44964  ovncvr2  44972  voncmpl  44982  hspmbllem2  44988  hspmbl  44990  opnvonmbllem1  44993  vonmblss  45001  ovnsubadd2lem  45006  vonioolem2  45042  preimageiingt  45081  preimaleiinlt  45082  issmfd  45096  issmfdf  45098  sssmf  45099  cnfsmf  45101  issmfled  45118  issmfgtd  45122  smfadd  45126  smfrec  45150  smfmul  45156  smfmulc1  45157  smfpimbor1lem2  45160  smfsuplem1  45172  smflimsuplem1  45181  smflimsuplem7  45187  sprssspr  45793  linc1  46626