Theorem eqsstrrd 3933

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 2764	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
3		eqsstrrd.2	. 2 ⊢ (𝜑 → 𝐵 ⊆ 𝐶)
4	2, 3	eqsstrd 3932	1 ⊢ (𝜑 → 𝐴 ⊆ 𝐶)

Syntax hints:   → wi 4   = wceq 1538   ⊆ wss 3860

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2729

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-v 3411  df-in 3867  df-ss 3877

This theorem is referenced by:  ssxpb  6007  fnsnr  6923  suppssof1  7878  oaword1  8193  omword2  8215  oeeui  8243  nnaword1  8270  cantnfle  9172  cantnflem1d  9189  r1val1  9253  rankr1id  9329  rankxplim3  9348  ackbij2  9708  ttukeylem7  9980  gruima  10267  hashdmpropge2  13898  rlimi  14923  rlimi2  14924  lo1bdd  14930  o1bdd  14941  rlimuni  14960  rlimcld2  14988  o1co  14996  rlimcn1  14998  rlimcn2  15000  o1add2  15033  o1mul2  15034  o1sub2  15035  lo1add  15036  lo1mul  15037  o1dif  15039  rlimneg  15056  rlimsqzlem  15058  lo1le  15061  rlimno1  15063  ramub1lem1  16422  imasaddfnlem  16864  imasvscafn  16873  mrcidb  16949  mrieqv2d  16973  mreexexlem4d  16981  funcres  17230  funcsetcres2  17424  acsfiindd  17858  tsrdir  17919  resmhm2  18057  f1omvdco2  18648  sylow2a  18816  sylow3lem6  18829  dprdspan  19222  dprd2dlem2  19235  dprd2dlem1  19236  dprd2da  19237  dmdprdsplit2lem  19240  dprdsplit  19243  dpjcntz  19247  ablfac1eu  19268  ringidss  19403  subrg1  19618  subrgdvds  19622  subrguss  19623  subrginv  19624  subdrgint  19655  primefld  19657  islss3  19804  lspsnneg  19851  lspextmo  19901  lspsnvs  19959  lsmcv  19986  islbs3  20000  drngdomn  20149  f1lindf  20592  psrbaglesupp  20691  psrbaglesuppOLD  20692  resspsrbas  20748  resspsradd  20749  resspsrmul  20750  evlseu  20851  epttop  21714  neitr  21885  ordtbas  21897  ordtrest2  21909  pnfnei  21925  mnfnei  21926  ordtrestixx  21927  dnsconst  22083  cmpcld  22107  txindis  22339  txtube  22345  xkohaus  22358  xkopt  22360  xkococnlem  22364  xkoinjcn  22392  qtopval2  22401  ssufl  22623  ufldom  22667  cnextcn  22772  tmdgsum2  22801  clssubg  22814  clsnsg  22815  ustund  22927  ustneism  22929  trust  22935  fmucnd  22998  imasdsf1olem  23080  setsmstopn  23185  metequiv2  23217  metust  23265  restmetu  23277  tngtopn  23357  xlebnum  23671  pi1xfrcnv  23763  limcdif  24580  limccnp  24595  limccnp2  24596  limcco  24597  dvn2bss  24634  cpnord  24639  dvcmulf  24649  dvmptres2  24666  dvmptcmul  24668  dvmptntr  24675  dvcnvrelem2  24722  dvcnvre  24723  taylthlem1  25072  taylthlem2  25073  ulmdvlem3  25101  psercnlem2  25123  rlimcxp  25663  o1cxp  25664  sspg  28615  ssps  28617  sspn  28623  mdslj1i  30206  mdslj2i  30207  sh1dle  30238  shatomistici  30248  sumdmdii  30302  unidifsnel  30410  resf1o  30593  gsumpart  30845  gsumhashmul  30846  symgcom2  30883  submarchi  30970  nsgmgc  31122  idlinsubrg  31133  fedgmullem1  31235  fedgmullem2  31236  fedgmul  31237  extdg1id  31263  madjusmdetlem1  31302  txomap  31309  rspectopn  31342  zarclssn  31348  zarcmplem  31356  cnvordtrestixx  31388  dya2iocucvr  31774  carsggect  31808  bnj1241  32311  bnj906  32434  cvmscld  32755  nosupbnd2lem1  33507  noinfbnd2lem1  33522  noetainflem4  33532  fvline2  34023  cldregopn  34095  pibt2  35140  poimirlem15  35378  sstotbnd2  35518  totbndbnd  35533  heibor1  35554  heiborlem8  35562  lsmsat  36610  lssats  36614  lkrpssN  36765  dia2dimlem5  38670  cdlemn2a  38798  dihglblem6  38942  dochocsp  38981  dochdmj1  38992  dochsatshpb  39054  lcfl9a  39107  lclkrlem2r  39126  lclkrlem2s  39127  lclkrlem2v  39130  lcfrlem6  39149  lcfrlem25  39169  lcfrlem35  39179  mapdval2N  39232  mapdin  39264  baerlem5alem2  39313  baerlem5blem2  39314  mhphf  39818  dnnumch2  40390  clrellem  40723  iunrelexpmin1  40810  iunrelexpmin2  40814  dftrcl3  40822  brtrclfv2  40829  dfrtrcl3  40835  mnuprdlem1  41381  mnuprdlem2  41382  mullimc  42652  islptre  42655  mullimcf  42659  limcmptdm  42671  dvresntr  42954  itgperiod  43017  fourierdlem89  43231  fourierdlem91  43233  iccpartgt  44340  resmgmhm2  44814  setrecsres  45695