Theorem eqsstrrd 3956

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890  df-ss 3900

This theorem is referenced by:  ssxpb  6066  fnsnr  7019  suppssof1  7986  oaword1  8345  omword2  8367  oeeui  8395  nnaword1  8422  cantnfle  9359  cantnflem1d  9376  r1val1  9475  rankr1id  9551  rankxplim3  9570  ackbij2  9930  ttukeylem7  10202  gruima  10489  hashdmpropge2  14125  rlimi  15150  rlimi2  15151  lo1bdd  15157  o1bdd  15168  rlimuni  15187  rlimcld2  15215  o1co  15223  rlimcn1  15225  rlimcn3  15227  o1add2  15261  o1mul2  15262  o1sub2  15263  lo1add  15264  lo1mul  15265  o1dif  15267  rlimneg  15286  rlimsqzlem  15288  lo1le  15291  rlimno1  15293  ramub1lem1  16655  imasaddfnlem  17156  imasvscafn  17165  mrcidb  17241  mrieqv2d  17265  mreexexlem4d  17273  funcres  17527  funcsetcres2  17724  acsfiindd  18186  tsrdir  18237  resmhm2  18375  f1omvdco2  18971  sylow2a  19139  sylow3lem6  19152  dprdspan  19545  dprd2dlem2  19558  dprd2dlem1  19559  dprd2da  19560  dmdprdsplit2lem  19563  dprdsplit  19566  dpjcntz  19570  ablfac1eu  19591  ringidss  19731  subrg1  19949  subrgdvds  19953  subrguss  19954  subrginv  19955  subdrgint  19986  primefld  19988  islss3  20136  lspsnneg  20183  lspextmo  20233  lspsnvs  20291  lsmcv  20318  islbs3  20332  drngdomn  20487  f1lindf  20939  psrbaglesupp  21037  psrbaglesuppOLD  21038  resspsrbas  21094  resspsradd  21095  resspsrmul  21096  evlseu  21203  epttop  22067  neitr  22239  ordtbas  22251  ordtrest2  22263  pnfnei  22279  mnfnei  22280  ordtrestixx  22281  dnsconst  22437  cmpcld  22461  txindis  22693  txtube  22699  xkohaus  22712  xkopt  22714  xkococnlem  22718  xkoinjcn  22746  qtopval2  22755  ssufl  22977  ufldom  23021  cnextcn  23126  tmdgsum2  23155  clssubg  23168  clsnsg  23169  ustund  23281  ustneism  23283  trust  23289  fmucnd  23352  imasdsf1olem  23434  setsmstopn  23539  metequiv2  23572  metust  23620  restmetu  23632  tngtopn  23720  xlebnum  24034  pi1xfrcnv  24126  limcdif  24945  limccnp  24960  limccnp2  24961  limcco  24962  dvn2bss  24999  cpnord  25004  dvcmulf  25014  dvmptres2  25031  dvmptcmul  25033  dvmptntr  25040  dvcnvrelem2  25087  dvcnvre  25088  taylthlem1  25437  taylthlem2  25438  ulmdvlem3  25466  psercnlem2  25488  rlimcxp  26028  o1cxp  26029  sspg  28991  ssps  28993  sspn  28999  mdslj1i  30582  mdslj2i  30583  sh1dle  30614  shatomistici  30624  sumdmdii  30678  unidifsnel  30784  resf1o  30967  gsumpart  31217  gsumhashmul  31218  symgcom2  31255  submarchi  31342  nsgmgc  31499  idlinsubrg  31510  fedgmullem1  31612  fedgmullem2  31613  fedgmul  31614  extdg1id  31640  madjusmdetlem1  31679  txomap  31686  rspectopn  31719  zarclssn  31725  zarcmplem  31733  cnvordtrestixx  31765  dya2iocucvr  32151  carsggect  32185  bnj1241  32687  bnj906  32810  fineqvac  32966  cvmscld  33135  nosupbnd2lem1  33845  noinfbnd2lem1  33860  noetainflem4  33870  fvline2  34375  cldregopn  34447  pibt2  35515  poimirlem15  35719  sstotbnd2  35859  totbndbnd  35874  heibor1  35895  heiborlem8  35903  lsmsat  36949  lssats  36953  lkrpssN  37104  dia2dimlem5  39009  cdlemn2a  39137  dihglblem6  39281  dochocsp  39320  dochdmj1  39331  dochsatshpb  39393  lcfl9a  39446  lclkrlem2r  39465  lclkrlem2s  39466  lclkrlem2v  39469  lcfrlem6  39488  lcfrlem25  39508  lcfrlem35  39518  mapdval2N  39571  mapdin  39603  baerlem5alem2  39652  baerlem5blem2  39653  mhphf  40208  dnnumch2  40786  clrellem  41119  iunrelexpmin1  41205  iunrelexpmin2  41209  dftrcl3  41217  brtrclfv2  41224  dfrtrcl3  41230  mnuprdlem1  41779  mnuprdlem2  41780  mullimc  43047  islptre  43050  mullimcf  43054  limcmptdm  43066  dvresntr  43349  itgperiod  43412  fourierdlem89  43626  fourierdlem91  43628  iccpartgt  44767  resmgmhm2  45241  setrecsres  46293