Theorem eqsstrrd 3961

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

Syntax hints:   → wi 4   = wceq 1539   ⊆ wss 3888

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-v 3435  df-in 3895  df-ss 3905

This theorem is referenced by:  ssxpb  6082  fnsnr  7046  suppssof1  8024  oaword1  8392  omword2  8414  oeeui  8442  nnaword1  8469  cantnfle  9438  cantnflem1d  9455  r1val1  9553  rankr1id  9629  rankxplim3  9648  ackbij2  10008  ttukeylem7  10280  gruima  10567  hashdmpropge2  14206  rlimi  15231  rlimi2  15232  lo1bdd  15238  o1bdd  15249  rlimuni  15268  rlimcld2  15296  o1co  15304  rlimcn1  15306  rlimcn3  15308  o1add2  15342  o1mul2  15343  o1sub2  15344  lo1add  15345  lo1mul  15346  o1dif  15348  rlimneg  15367  rlimsqzlem  15369  lo1le  15372  rlimno1  15374  ramub1lem1  16736  imasaddfnlem  17248  imasvscafn  17257  mrcidb  17333  mrieqv2d  17357  mreexexlem4d  17365  funcres  17620  funcsetcres2  17817  acsfiindd  18280  tsrdir  18331  resmhm2  18469  f1omvdco2  19065  sylow2a  19233  sylow3lem6  19246  dprdspan  19639  dprd2dlem2  19652  dprd2dlem1  19653  dprd2da  19654  dmdprdsplit2lem  19657  dprdsplit  19660  dpjcntz  19664  ablfac1eu  19685  ringidss  19825  subrg1  20043  subrgdvds  20047  subrguss  20048  subrginv  20049  subdrgint  20080  primefld  20082  islss3  20230  lspsnneg  20277  lspextmo  20327  lspsnvs  20385  lsmcv  20412  islbs3  20426  drngdomn  20583  f1lindf  21038  psrbaglesupp  21136  psrbaglesuppOLD  21137  resspsrbas  21193  resspsradd  21194  resspsrmul  21195  evlseu  21302  epttop  22168  neitr  22340  ordtbas  22352  ordtrest2  22364  pnfnei  22380  mnfnei  22381  ordtrestixx  22382  dnsconst  22538  cmpcld  22562  txindis  22794  txtube  22800  xkohaus  22813  xkopt  22815  xkococnlem  22819  xkoinjcn  22847  qtopval2  22856  ssufl  23078  ufldom  23122  cnextcn  23227  tmdgsum2  23256  clssubg  23269  clsnsg  23270  ustund  23382  ustneism  23384  trust  23390  fmucnd  23453  imasdsf1olem  23535  setsmstopn  23642  metequiv2  23675  metust  23723  restmetu  23735  tngtopn  23823  xlebnum  24137  pi1xfrcnv  24229  limcdif  25049  limccnp  25064  limccnp2  25065  limcco  25066  dvn2bss  25103  cpnord  25108  dvcmulf  25118  dvmptres2  25135  dvmptcmul  25137  dvmptntr  25144  dvcnvrelem2  25191  dvcnvre  25192  taylthlem1  25541  taylthlem2  25542  ulmdvlem3  25570  psercnlem2  25592  rlimcxp  26132  o1cxp  26133  sspg  29099  ssps  29101  sspn  29107  mdslj1i  30690  mdslj2i  30691  sh1dle  30722  shatomistici  30732  sumdmdii  30786  unidifsnel  30892  resf1o  31074  gsumpart  31324  gsumhashmul  31325  symgcom2  31362  submarchi  31449  nsgmgc  31606  idlinsubrg  31617  fedgmullem1  31719  fedgmullem2  31720  fedgmul  31721  extdg1id  31747  madjusmdetlem1  31786  txomap  31793  rspectopn  31826  zarclssn  31832  zarcmplem  31840  cnvordtrestixx  31872  dya2iocucvr  32260  carsggect  32294  bnj1241  32796  bnj906  32919  fineqvac  33075  cvmscld  33244  nosupbnd2lem1  33927  noinfbnd2lem1  33942  noetainflem4  33952  fvline2  34457  cldregopn  34529  pibt2  35597  poimirlem15  35801  sstotbnd2  35941  totbndbnd  35956  heibor1  35977  heiborlem8  35985  lsmsat  37029  lssats  37033  lkrpssN  37184  dia2dimlem5  39089  cdlemn2a  39217  dihglblem6  39361  dochocsp  39400  dochdmj1  39411  dochsatshpb  39473  lcfl9a  39526  lclkrlem2r  39545  lclkrlem2s  39546  lclkrlem2v  39549  lcfrlem6  39568  lcfrlem25  39588  lcfrlem35  39598  mapdval2N  39651  mapdin  39683  baerlem5alem2  39732  baerlem5blem2  39733  mhphf  40292  dnnumch2  40877  clrellem  41237  iunrelexpmin1  41323  iunrelexpmin2  41327  dftrcl3  41335  brtrclfv2  41342  dfrtrcl3  41348  mnuprdlem1  41897  mnuprdlem2  41898  mullimc  43164  islptre  43167  mullimcf  43171  limcmptdm  43183  dvresntr  43466  itgperiod  43529  fourierdlem89  43743  fourierdlem91  43745  iccpartgt  44890  resmgmhm2  45364  setrecsres  46418