Theorem eqsstrd 4018

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

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

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 2708

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

This theorem is referenced by:  eqsstrrd  4019  eqsstrdi  4028  3sstr4d  4039  fpr2g  7231  tfisi  7880  suppssof1  8224  suppss2  8225  onfununi  8381  oawordeulem  8592  oeeui  8640  nnawordex  8675  oaabslem  8685  oaabs2  8687  omabslem  8688  omabs  8689  cofonr  8712  pw2f1olem  9116  fodomr  9168  fodomfir  9368  fival  9452  dffi3  9471  ordtypelem7  9564  ordtypelem8  9565  wemapso2lem  9592  cantnflt2  9713  cantnflem1  9729  tcss  9784  tcel  9785  r1val1  9826  rankuni2b  9893  tcrank  9924  cardonle  9997  harval2  10037  ackbij2  10282  cfub  10289  cflecard  10293  cfflb  10299  isf32lem8  10400  itunitc1  10460  ttukeylem7  10555  fpwwe2lem8  10678  wuncss  10785  wuncval2  10787  grur1a  10859  trclfvub  15046  cotrtrclfv  15051  relexpfld  15088  rtrclreclem4  15100  limsupgre  15517  isercolllem3  15703  4sqlem19  17001  vdwlem1  17019  vdwlem12  17030  ramub1lem1  17064  setsstruct2  17211  ressress  17293  imasaddfnlem  17573  imasaddflem  17575  imasvscafn  17582  imasvscaf  17584  imasless  17585  isohom  17820  ressffth  17985  acsfiindd  18598  acsmap2d  18600  dirref  18646  mndind  18841  f1omvdco2  19466  pmtrfrn  19476  symgsssg  19485  symggen  19488  psgnunilem1  19511  sylow2alem2  19636  lsmssv  19661  smndlsmidm  19674  gsumzres  19927  dprdlub  20046  dprdf1  20053  dprdsn  20056  dprdcntz2  20058  dprd2dlem1  20061  dprd2da  20062  dmdprdsplit2lem  20065  ablfac1eu  20093  rgspnmin  20615  drnglpir  21342  znleval  21573  evpmss  21604  frlmsplit2  21793  f1lindf  21842  issubassa2  21912  mplsubglem  22019  evlslem4  22100  evlseu  22107  mhpaddcl  22155  mhpinvcl  22156  psdmul  22170  lpsscls  23149  tgrest  23167  resttopon  23169  rest0  23177  restfpw  23187  ordtrest  23210  ordtrest2  23212  lmcnp  23312  tgcmp  23409  uncmp  23411  hauscmplem  23414  1stcfb  23453  2ndcdisj  23464  dissnref  23536  kgencmp  23553  xkouni  23607  prdstopn  23636  txtube  23648  txcmplem2  23650  xkoptsub  23662  xkopt  23663  xkococnlem  23667  qtoprest  23725  imastopn  23728  kqdisj  23740  reghmph  23801  nrmhmph  23802  fbssfi  23845  trfilss  23897  trfg  23899  elfm3  23958  alexsubALTlem3  24057  alexsubALT  24059  cnextf  24074  cnextcn  24075  clsnsg  24118  tgpconncompeqg  24120  qustgphaus  24131  trust  24238  ustuqtop3  24252  neipcfilu  24305  metequiv2  24523  prdsxmslem2  24542  metustfbas  24570  icccmplem1  24844  metdstri  24873  pi1addf  25080  pi1addval  25081  caubl  25342  caublcls  25343  relcmpcmet  25352  minveclem4  25466  hlhil  25477  ovolficcss  25504  uniioombllem3a  25619  uniioombllem3  25620  dyadss  25629  opnmbllem  25636  i1fima2  25714  limcfval  25907  dvfval  25932  dvnres  25967  dvivth  26049  lhop  26055  taylf  26402  xrlimcnp  27011  jensen  27032  ppisval  27147  chtlepsi  27250  chpub  27264  noextend  27711  nosupbday  27750  noinfbday  27765  scutun12  27855  scutbdaybnd  27860  scutbdaybnd2  27861  scutbdaylt  27863  cofcut1  27954  cofcutr  27958  addsbday  28050  negsbdaylem  28088  precsexlem8  28238  noseqind  28298  n0sbday  28354  pw2bday  28418  iscgrglt  28522  cyclnumvtx  29820  chssoc  31515  mdsl0  32329  mdexchi  32354  atcvat3i  32415  dmdbr5ati  32441  funimass4f  32647  xrofsup  32771  swrdrn2  32939  gsumpart  33060  pmtrcnel  33109  tocycfvres1  33130  tocycfvres2  33131  cycpmco2lem6  33151  cycpmconjvlem  33161  cycpmconjslem2  33175  elrgspnsubrunlem2  33252  fldgenssv  33317  fldgenssp  33320  nsgmgc  33440  idlsrgmulrss1  33539  idlsrgmulrss2  33540  fedgmullem1  33680  fedgmullem2  33681  constrsscn  33781  constrmon  33785  ist0cld  33832  locfinreflem  33839  cmpcref  33849  zarcls0  33867  zarclsiin  33870  zarcmplem  33880  cnvordtrestixx  33912  ordtrestNEW  33920  ordtrest2NEW  33922  pnfneige0  33950  sigagenss  34150  imambfm  34264  dya2iocress  34276  dya2icoseg  34279  dya2iocucvr  34286  ballotlemro  34525  ftc2re  34613  bnj1097  34995  bnj1452  35066  cvmlift3lem6  35329  msubrn  35534  mclsssv  35569  mclsind  35575  liness  36146  neibastop2lem  36361  opnmbllem0  37663  mblfinlem2  37665  isbndx  37789  isbnd2  37790  ssbnd  37795  heiborlem3  37820  igenmin  38071  lsatlss  38997  lsmsat  39009  lsatfixedN  39010  lssats  39013  lpssat  39014  lssatle  39016  lssat  39017  lsatcvat3  39053  paddssat  39816  paddasslem17  39838  pmodlem2  39849  hlmod1i  39858  pl42lem4N  39984  diassdvaN  41062  dia2dimlem10  41075  cdlemn4a  41201  cdlemn5pre  41202  dihord5apre  41264  lclkrlem2e  41513  lclkrlem2p  41524  lclkrlem2v  41530  lclkrslem2  41540  lclkrs  41541  lcfrlem25  41569  lcfrlem35  41579  mapdval2N  41632  mapdpglem8  41681  mapdpglem13  41686  baerlem3lem2  41712  mapdindp2  41723  hdmap11lem2  41844  primrootspoweq0  42107  aks6d1c6lem2  42172  evlsmhpvvval  42605  prjspnssbas  42631  elrfi  42705  isnacs3  42721  mzpf  42747  mzpindd  42757  diophrw  42770  eldiophss  42785  rmxyelqirrOLD  42922  pw2f1ocnv  43049  aomclem6  43071  hbt  43142  oasubex  43299  oaabsb  43307  nnoeomeqom  43325  omcl2  43346  naddgeoa  43407  naddwordnexlem4  43414  oaltom  43418  omltoe  43420  minregex  43547  cnvssb  43599  trclubgNEW  43631  dfrcl2  43687  fvmptiunrelexplb0da  43698  relexp0a  43729  cotrcltrcl  43738  trclimalb2  43739  cotrclrcl  43755  isotone2  44062  k0004ss1  44164  fnresdmss  45173  mptelpm  45181  ssnnf1octb  45199  uzfissfz  45337  iuneqfzuzlem  45345  xlimliminflimsup  45877  icccncfext  45902  dvnprodlem2  45962  dvnprodlem3  45963  fourierdlem41  46163  fourierdlem70  46191  fourierdlem71  46192  fourierdlem80  46201  fourierdlem113  46234  ioorrnopnlem  46319  ioorrnopnxrlem  46321  salgenss  46351  dfsalgen2  46356  subsaliuncllem  46372  iundjiun  46475  meadjiunlem  46480  meaiunlelem  46483  meaiuninclem  46495  meaiininclem  46501  omeunle  46531  carageniuncllem2  46537  caratheodorylem1  46541  caratheodorylem2  46542  hoissre  46559  ovnsubaddlem1  46585  hoidmvlelem3  46612  ovnhoilem1  46616  ovnhoilem2  46617  ovnhoi  46618  ovncvr2  46626  voncmpl  46636  hspmbllem2  46642  hspmbl  46644  opnvonmbllem1  46647  vonmblss  46655  ovnsubadd2lem  46660  vonioolem2  46696  preimageiingt  46735  preimaleiinlt  46736  issmfd  46750  issmfdf  46752  sssmf  46753  cnfsmf  46755  issmfled  46772  issmfgtd  46776  smfadd  46780  smfrec  46804  smfmul  46810  smfmulc1  46811  smfpimbor1lem2  46814  smfsuplem1  46826  smflimsuplem1  46835  smflimsuplem7  46841  sprssspr  47468  isubgredgss  47851  isubgrsubgr  47855  uspgrimprop  47873  uhgrimisgrgriclem  47898  stgrnbgr0  47931  uspgrlimlem3  47957  linc1  48342