Theorem eqsstrrd 4018

Description: Substitution of equality into a subclass relationship. (Contributed by NM, 25-Apr-2004.)

Hypotheses

Ref	Expression
eqsstrrd.1	⊢ (𝜑 → 𝐵 = 𝐴)
eqsstrrd.2	⊢ (𝜑 → 𝐵 ⊆ 𝐶)

Assertion

Ref	Expression
eqsstrrd	⊢ (𝜑 → 𝐴 ⊆ 𝐶)

Proof of Theorem eqsstrrd

Step	Hyp	Ref	Expression
1		eqsstrrd.1	. . 3 ⊢ (𝜑 → 𝐵 = 𝐴)
2	1	eqcomd 2738	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
3		eqsstrrd.2	. 2 ⊢ (𝜑 → 𝐵 ⊆ 𝐶)
4	2, 3	eqsstrd 4017	1 ⊢ (𝜑 → 𝐴 ⊆ 𝐶)

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

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 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-in 3952  df-ss 3962

This theorem is referenced by:  ssxpb  6163  fnsnr  7148  suppssof1  8168  oaword1  8537  omword2  8559  oeeui  8587  nnaword1  8614  naddword1  8675  naddunif  8677  cantnfle  9650  cantnflem1d  9667  r1val1  9765  rankr1id  9841  rankxplim3  9860  ackbij2  10222  ttukeylem7  10494  gruima  10781  hashdmpropge2  14428  rlimi  15441  rlimi2  15442  lo1bdd  15448  o1bdd  15459  rlimuni  15478  rlimcld2  15506  o1co  15514  rlimcn1  15516  rlimcn3  15518  o1add2  15552  o1mul2  15553  o1sub2  15554  lo1add  15555  lo1mul  15556  o1dif  15558  rlimneg  15577  rlimsqzlem  15579  lo1le  15582  rlimno1  15584  ramub1lem1  16943  imasaddfnlem  17458  imasvscafn  17467  mrcidb  17543  mrieqv2d  17567  mreexexlem4d  17575  funcres  17830  funcsetcres2  18027  acsfiindd  18490  tsrdir  18541  resmhm2  18680  f1omvdco2  19282  sylow2a  19453  sylow3lem6  19466  dprdspan  19858  dprd2dlem2  19871  dprd2dlem1  19872  dprd2da  19873  dmdprdsplit2lem  19876  dprdsplit  19879  dpjcntz  19883  ablfac1eu  19904  ringidss  20053  subrg1  20324  subrgdvds  20328  subrguss  20329  subrginv  20330  subdrgint  20370  primefld  20372  islss3  20521  lspsnneg  20568  lspextmo  20618  lspsnvs  20678  lsmcv  20705  islbs3  20719  drngdomn  20857  f1lindf  21312  psrbaglesupp  21410  psrbaglesuppOLD  21411  resspsrbas  21468  resspsradd  21469  resspsrmul  21470  evlseu  21577  epttop  22443  neitr  22615  ordtbas  22627  ordtrest2  22639  pnfnei  22655  mnfnei  22656  ordtrestixx  22657  dnsconst  22813  cmpcld  22837  txindis  23069  txtube  23075  xkohaus  23088  xkopt  23090  xkococnlem  23094  xkoinjcn  23122  qtopval2  23131  ssufl  23353  ufldom  23397  cnextcn  23502  tmdgsum2  23531  clssubg  23544  clsnsg  23545  ustund  23657  ustneism  23659  trust  23665  fmucnd  23728  imasdsf1olem  23810  setsmstopn  23917  metequiv2  23950  metust  23998  restmetu  24010  tngtopn  24098  xlebnum  24412  pi1xfrcnv  24504  limcdif  25324  limccnp  25339  limccnp2  25340  limcco  25341  dvn2bss  25378  cpnord  25383  dvcmulf  25393  dvmptres2  25410  dvmptcmul  25412  dvmptntr  25419  dvcnvrelem2  25466  dvcnvre  25467  taylthlem1  25816  taylthlem2  25817  ulmdvlem3  25845  psercnlem2  25867  rlimcxp  26407  o1cxp  26408  nosupbnd2lem1  27147  noinfbnd2lem1  27162  noetainflem4  27172  negsbday  27460  sspg  29908  ssps  29910  sspn  29916  mdslj1i  31499  mdslj2i  31500  sh1dle  31531  shatomistici  31541  sumdmdii  31595  unidifsnel  31701  resf1o  31890  gsumpart  32142  gsumhashmul  32143  symgcom2  32180  submarchi  32267  nsgmgc  32443  ghmqusker  32451  lmhmqusker  32453  rhmqusker  32459  idlinsubrg  32464  ply1degltdimlem  32609  fedgmullem1  32616  fedgmullem2  32617  fedgmul  32618  extdg1id  32644  madjusmdetlem1  32702  txomap  32709  rspectopn  32742  zarclssn  32748  zarcmplem  32756  cnvordtrestixx  32788  dya2iocucvr  33178  carsggect  33212  bnj1241  33713  bnj906  33836  fineqvac  33992  cvmscld  34159  fvline2  35012  cldregopn  35084  pibt2  36166  poimirlem15  36371  sstotbnd2  36511  totbndbnd  36526  heibor1  36547  heiborlem8  36555  lsmsat  37747  lssats  37751  lkrpssN  37902  dia2dimlem5  39808  cdlemn2a  39936  dihglblem6  40080  dochocsp  40119  dochdmj1  40130  dochsatshpb  40192  lcfl9a  40245  lclkrlem2r  40264  lclkrlem2s  40265  lclkrlem2v  40268  lcfrlem6  40287  lcfrlem25  40307  lcfrlem35  40317  mapdval2N  40370  mapdin  40402  baerlem5alem2  40451  baerlem5blem2  40452  mhphf  41021  dnnumch2  41622  oege1  41891  omabs2  41917  nadd2rabex  41971  clrellem  42208  iunrelexpmin1  42294  iunrelexpmin2  42298  dftrcl3  42306  brtrclfv2  42313  dfrtrcl3  42319  mnuprdlem1  42866  mnuprdlem2  42867  mullimc  44169  islptre  44172  mullimcf  44176  limcmptdm  44188  dvresntr  44471  itgperiod  44534  fourierdlem89  44748  fourierdlem91  44750  iccpartgt  45931  resmgmhm2  46405  setrecsres  47459