Theorem eqsstrd 3993

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

Syntax hints:   → wi 4   = wceq 1540   ⊆ wss 3926

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2727  df-ss 3943

This theorem is referenced by:  eqsstrrd  3994  eqsstrdi  4003  3sstr4d  4014  fpr2g  7203  tfisi  7854  suppssof1  8198  suppss2  8199  onfununi  8355  oawordeulem  8566  oeeui  8614  nnawordex  8649  oaabslem  8659  oaabs2  8661  omabslem  8662  omabs  8663  cofonr  8686  pw2f1olem  9090  fodomr  9142  fodomfir  9340  fival  9424  dffi3  9443  ordtypelem7  9538  ordtypelem8  9539  wemapso2lem  9566  cantnflt2  9687  cantnflem1  9703  tcss  9758  tcel  9759  r1val1  9800  rankuni2b  9867  tcrank  9898  cardonle  9971  harval2  10011  ackbij2  10256  cfub  10263  cflecard  10267  cfflb  10273  isf32lem8  10374  itunitc1  10434  ttukeylem7  10529  fpwwe2lem8  10652  wuncss  10759  wuncval2  10761  grur1a  10833  trclfvub  15026  cotrtrclfv  15031  relexpfld  15068  rtrclreclem4  15080  limsupgre  15497  isercolllem3  15683  4sqlem19  16983  vdwlem1  17001  vdwlem12  17012  ramub1lem1  17046  setsstruct2  17193  ressress  17268  imasaddfnlem  17542  imasaddflem  17544  imasvscafn  17551  imasvscaf  17553  imasless  17554  isohom  17789  ressffth  17953  acsfiindd  18563  acsmap2d  18565  dirref  18611  mndind  18806  f1omvdco2  19429  pmtrfrn  19439  symgsssg  19448  symggen  19451  psgnunilem1  19474  sylow2alem2  19599  lsmssv  19624  smndlsmidm  19637  gsumzres  19890  dprdlub  20009  dprdf1  20016  dprdsn  20019  dprdcntz2  20021  dprd2dlem1  20024  dprd2da  20025  dmdprdsplit2lem  20028  ablfac1eu  20056  rgspnmin  20575  drnglpir  21293  znleval  21515  evpmss  21546  frlmsplit2  21733  f1lindf  21782  issubassa2  21852  mplsubglem  21959  evlslem4  22034  evlseu  22041  mhpaddcl  22089  mhpinvcl  22090  psdmul  22104  lpsscls  23079  tgrest  23097  resttopon  23099  rest0  23107  restfpw  23117  ordtrest  23140  ordtrest2  23142  lmcnp  23242  tgcmp  23339  uncmp  23341  hauscmplem  23344  1stcfb  23383  2ndcdisj  23394  dissnref  23466  kgencmp  23483  xkouni  23537  prdstopn  23566  txtube  23578  txcmplem2  23580  xkoptsub  23592  xkopt  23593  xkococnlem  23597  qtoprest  23655  imastopn  23658  kqdisj  23670  reghmph  23731  nrmhmph  23732  fbssfi  23775  trfilss  23827  trfg  23829  elfm3  23888  alexsubALTlem3  23987  alexsubALT  23989  cnextf  24004  cnextcn  24005  clsnsg  24048  tgpconncompeqg  24050  qustgphaus  24061  trust  24168  ustuqtop3  24182  neipcfilu  24234  metequiv2  24449  prdsxmslem2  24468  metustfbas  24496  icccmplem1  24762  metdstri  24791  pi1addf  24998  pi1addval  24999  caubl  25260  caublcls  25261  relcmpcmet  25270  minveclem4  25384  hlhil  25395  ovolficcss  25422  uniioombllem3a  25537  uniioombllem3  25538  dyadss  25547  opnmbllem  25554  i1fima2  25632  limcfval  25825  dvfval  25850  dvnres  25885  dvivth  25967  lhop  25973  taylf  26320  xrlimcnp  26930  jensen  26951  ppisval  27066  chtlepsi  27169  chpub  27183  noextend  27630  nosupbday  27669  noinfbday  27684  scutun12  27774  scutbdaybnd  27779  scutbdaybnd2  27780  scutbdaylt  27782  cofcut1  27880  cofcutr  27884  addsbday  27976  negsbdaylem  28014  precsexlem8  28168  bdayon  28225  noseqind  28238  n0sbday  28296  iscgrglt  28493  cyclnumvtx  29782  chssoc  31477  mdsl0  32291  mdexchi  32316  atcvat3i  32377  dmdbr5ati  32403  funimass4f  32615  xrofsup  32744  swrdrn2  32930  gsumpart  33051  pmtrcnel  33100  tocycfvres1  33121  tocycfvres2  33122  cycpmco2lem6  33142  cycpmconjvlem  33152  cycpmconjslem2  33166  elrgspnsubrunlem2  33243  fldgenssv  33309  fldgenssp  33312  nsgmgc  33427  idlsrgmulrss1  33526  idlsrgmulrss2  33527  fedgmullem1  33669  fedgmullem2  33670  constrsscn  33774  constrmon  33778  ist0cld  33864  locfinreflem  33871  cmpcref  33881  zarcls0  33899  zarclsiin  33902  zarcmplem  33912  cnvordtrestixx  33944  ordtrestNEW  33952  ordtrest2NEW  33954  pnfneige0  33982  sigagenss  34180  imambfm  34294  dya2iocress  34306  dya2icoseg  34309  dya2iocucvr  34316  ballotlemro  34555  ftc2re  34630  bnj1097  35012  bnj1452  35083  cvmlift3lem6  35346  msubrn  35551  mclsssv  35586  mclsind  35592  liness  36163  neibastop2lem  36378  opnmbllem0  37680  mblfinlem2  37682  isbndx  37806  isbnd2  37807  ssbnd  37812  heiborlem3  37837  igenmin  38088  lsatlss  39014  lsmsat  39026  lsatfixedN  39027  lssats  39030  lpssat  39031  lssatle  39033  lssat  39034  lsatcvat3  39070  paddssat  39833  paddasslem17  39855  pmodlem2  39866  hlmod1i  39875  pl42lem4N  40001  diassdvaN  41079  dia2dimlem10  41092  cdlemn4a  41218  cdlemn5pre  41219  dihord5apre  41281  lclkrlem2e  41530  lclkrlem2p  41541  lclkrlem2v  41547  lclkrslem2  41557  lclkrs  41558  lcfrlem25  41586  lcfrlem35  41596  mapdval2N  41649  mapdpglem8  41698  mapdpglem13  41703  baerlem3lem2  41729  mapdindp2  41740  hdmap11lem2  41861  primrootspoweq0  42119  aks6d1c6lem2  42184  evlsmhpvvval  42618  prjspnssbas  42644  elrfi  42717  isnacs3  42733  mzpf  42759  mzpindd  42769  diophrw  42782  eldiophss  42797  rmxyelqirrOLD  42934  pw2f1ocnv  43061  aomclem6  43083  hbt  43154  oasubex  43310  oaabsb  43318  nnoeomeqom  43336  omcl2  43357  naddgeoa  43418  naddwordnexlem4  43425  oaltom  43429  omltoe  43431  minregex  43558  cnvssb  43610  trclubgNEW  43642  dfrcl2  43698  fvmptiunrelexplb0da  43709  relexp0a  43740  cotrcltrcl  43749  trclimalb2  43750  cotrclrcl  43766  isotone2  44073  k0004ss1  44175  fnresdmss  45192  mptelpm  45200  ssnnf1octb  45218  uzfissfz  45353  iuneqfzuzlem  45361  xlimliminflimsup  45891  icccncfext  45916  dvnprodlem2  45976  dvnprodlem3  45977  fourierdlem41  46177  fourierdlem70  46205  fourierdlem71  46206  fourierdlem80  46215  fourierdlem113  46248  ioorrnopnlem  46333  ioorrnopnxrlem  46335  salgenss  46365  dfsalgen2  46370  subsaliuncllem  46386  iundjiun  46489  meadjiunlem  46494  meaiunlelem  46497  meaiuninclem  46509  meaiininclem  46515  omeunle  46545  carageniuncllem2  46551  caratheodorylem1  46555  caratheodorylem2  46556  hoissre  46573  ovnsubaddlem1  46599  hoidmvlelem3  46626  ovnhoilem1  46630  ovnhoilem2  46631  ovnhoi  46632  ovncvr2  46640  voncmpl  46650  hspmbllem2  46656  hspmbl  46658  opnvonmbllem1  46661  vonmblss  46669  ovnsubadd2lem  46674  vonioolem2  46710  preimageiingt  46749  preimaleiinlt  46750  issmfd  46764  issmfdf  46766  sssmf  46767  cnfsmf  46769  issmfled  46786  issmfgtd  46790  smfadd  46794  smfrec  46818  smfmul  46824  smfmulc1  46825  smfpimbor1lem2  46828  smfsuplem1  46840  smflimsuplem1  46849  smflimsuplem7  46855  sprssspr  47495  isubgredgss  47878  isubgrsubgr  47882  uhgrimisgrgriclem  47943  stgrnbgr0  47976  uspgrlimlem3  48002  linc1  48401  iinfssc  49024  discsubc  49031  idfullsubc  49100