Theorem eqsstrrd 4019

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 2743	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
3		eqsstrrd.2	. 2 ⊢ (𝜑 → 𝐵 ⊆ 𝐶)
4	2, 3	eqsstrd 4018	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:  3sstr3d  4038  ssxpb  6194  fnsnr  7185  suppssof1  8224  oaword1  8590  omword2  8612  oeeui  8640  nnaword1  8667  naddword1  8729  naddunif  8731  cantnfle  9711  cantnflem1d  9728  r1val1  9826  rankr1id  9902  rankxplim3  9921  ackbij2  10282  ttukeylem7  10555  gruima  10842  hashdmpropge2  14522  rlimi  15549  rlimi2  15550  lo1bdd  15556  o1bdd  15567  rlimuni  15586  rlimcld2  15614  o1co  15622  rlimcn1  15624  rlimcn3  15626  o1add2  15660  o1mul2  15661  o1sub2  15662  lo1add  15663  lo1mul  15664  o1dif  15666  rlimneg  15683  rlimsqzlem  15685  lo1le  15688  rlimno1  15690  ramub1lem1  17064  imasaddfnlem  17573  imasvscafn  17582  mrcidb  17658  mrieqv2d  17682  mreexexlem4d  17690  funcres  17941  funcsetcres2  18138  acsfiindd  18598  tsrdir  18649  resmgmhm2  18725  resmhm2  18834  ghmqusnsg  19300  ghmquskerlem3  19304  ghmqusker  19305  f1omvdco2  19466  sylow2a  19637  sylow3lem6  19650  dprdspan  20047  dprd2dlem2  20060  dprd2dlem1  20061  dprd2da  20062  dmdprdsplit2lem  20065  dprdsplit  20068  dpjcntz  20072  ablfac1eu  20093  ringidss  20274  subrg1  20582  subrgdvds  20586  subrguss  20587  subrginv  20588  drngdomn  20749  subdrgint  20804  primefld  20806  islss3  20957  lspsnneg  21004  lspextmo  21055  lspsnvs  21116  lsmcv  21143  islbs3  21157  rhmqusnsg  21295  f1lindf  21842  psrbaglesupp  21942  resspsrbas  21994  resspsradd  21995  resspsrmul  21996  evlseu  22107  epttop  23016  neitr  23188  ordtbas  23200  ordtrest2  23212  pnfnei  23228  mnfnei  23229  ordtrestixx  23230  dnsconst  23386  cmpcld  23410  txindis  23642  txtube  23648  xkohaus  23661  xkopt  23663  xkococnlem  23667  xkoinjcn  23695  qtopval2  23704  ssufl  23926  ufldom  23970  cnextcn  24075  tmdgsum2  24104  clssubg  24117  clsnsg  24118  ustund  24230  ustneism  24232  trust  24238  fmucnd  24301  imasdsf1olem  24383  setsmstopn  24490  metequiv2  24523  metust  24571  restmetu  24583  tngtopn  24671  xlebnum  24997  pi1xfrcnv  25090  limcdif  25911  limccnp  25926  limccnp2  25927  limcco  25928  dvn2bss  25966  cpnord  25971  dvcmulf  25982  dvmptres2  26000  dvmptcmul  26002  dvmptntr  26009  dvcnvrelem2  26057  dvcnvre  26058  taylthlem1  26415  taylthlem2  26416  taylthlem2OLD  26417  ulmdvlem3  26445  psercnlem2  26468  rlimcxp  27017  o1cxp  27018  nosupbnd2lem1  27760  noinfbnd2lem1  27775  noetainflem4  27785  negsbday  28089  sspg  30747  ssps  30749  sspn  30755  mdslj1i  32338  mdslj2i  32339  sh1dle  32370  shatomistici  32380  sumdmdii  32434  unidifsnel  32553  fisuppov1  32692  resf1o  32741  gsumpart  33060  gsumhashmul  33064  symgcom2  33104  submarchi  33193  nsgmgc  33440  lmhmqusker  33445  rhmquskerlem  33453  idlinsubrg  33459  ply1degltdimlem  33673  fedgmullem1  33680  fedgmullem2  33681  fedgmul  33682  extdg1id  33716  fldextrspunlem1  33725  madjusmdetlem1  33826  txomap  33833  rspectopn  33866  zarclssn  33872  zarcmplem  33880  cnvordtrestixx  33912  dya2iocucvr  34286  carsggect  34320  bnj1241  34821  bnj906  34944  fineqvac  35111  cvmscld  35278  fvline2  36147  cldregopn  36332  pibt2  37418  poimirlem15  37642  sstotbnd2  37781  totbndbnd  37796  heibor1  37817  heiborlem8  37825  lsmsat  39009  lssats  39013  lkrpssN  39164  dia2dimlem5  41070  cdlemn2a  41198  dihglblem6  41342  dochocsp  41381  dochdmj1  41392  dochsatshpb  41454  lcfl9a  41507  lclkrlem2r  41526  lclkrlem2s  41527  lclkrlem2v  41530  lcfrlem6  41549  lcfrlem25  41569  lcfrlem35  41579  mapdval2N  41632  mapdin  41664  baerlem5alem2  41713  baerlem5blem2  41714  evlsvvval  42573  evlsbagval  42576  evlsmhpvvval  42605  mhphf  42607  dnnumch2  43057  oege1  43319  omabs2  43345  nadd2rabex  43399  clrellem  43635  iunrelexpmin1  43721  iunrelexpmin2  43725  dftrcl3  43733  brtrclfv2  43740  dfrtrcl3  43746  mnuprdlem1  44291  mnuprdlem2  44292  mullimc  45631  islptre  45634  mullimcf  45638  limcmptdm  45650  dvresntr  45933  itgperiod  45996  fourierdlem89  46210  fourierdlem91  46212  iccpartgt  47414  clnbgrgrim  47902  setrecsres  49221