Theorem eqsstrrd 3954

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

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

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 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-in 3888  df-ss 3898

This theorem is referenced by:  ssxpb  5998  fnsnr  6904  suppssof1  7846  oaword1  8161  omword2  8183  oeeui  8211  nnaword1  8238  cantnfle  9118  cantnflem1d  9135  r1val1  9199  rankr1id  9275  rankxplim3  9294  ackbij2  9654  ttukeylem7  9926  gruima  10213  hashdmpropge2  13837  rlimi  14862  rlimi2  14863  lo1bdd  14869  o1bdd  14880  rlimuni  14899  rlimcld2  14927  o1co  14935  rlimcn1  14937  rlimcn2  14939  o1add2  14972  o1mul2  14973  o1sub2  14974  lo1add  14975  lo1mul  14976  o1dif  14978  rlimneg  14995  rlimsqzlem  14997  lo1le  15000  rlimno1  15002  ramub1lem1  16352  imasaddfnlem  16793  imasvscafn  16802  mrcidb  16878  mrieqv2d  16902  mreexexlem4d  16910  funcres  17158  funcsetcres2  17345  acsfiindd  17779  tsrdir  17840  resmhm2  17978  f1omvdco2  18568  sylow2a  18736  sylow3lem6  18749  dprdspan  19142  dprd2dlem2  19155  dprd2dlem1  19156  dprd2da  19157  dmdprdsplit2lem  19160  dprdsplit  19163  dpjcntz  19167  ablfac1eu  19188  ringidss  19323  subrg1  19538  subrgdvds  19542  subrguss  19543  subrginv  19544  subdrgint  19575  primefld  19577  islss3  19724  lspsnneg  19771  lspextmo  19821  lspsnvs  19879  lsmcv  19906  islbs3  19920  drngdomn  20069  f1lindf  20511  psrbaglesupp  20606  resspsrbas  20653  resspsradd  20654  resspsrmul  20655  evlseu  20755  epttop  21614  neitr  21785  ordtbas  21797  ordtrest2  21809  pnfnei  21825  mnfnei  21826  ordtrestixx  21827  dnsconst  21983  cmpcld  22007  txindis  22239  txtube  22245  xkohaus  22258  xkopt  22260  xkococnlem  22264  xkoinjcn  22292  qtopval2  22301  ssufl  22523  ufldom  22567  cnextcn  22672  tmdgsum2  22701  clssubg  22714  clsnsg  22715  ustund  22827  ustneism  22829  trust  22835  fmucnd  22898  imasdsf1olem  22980  setsmstopn  23085  metequiv2  23117  metust  23165  restmetu  23177  tngtopn  23256  xlebnum  23570  pi1xfrcnv  23662  limcdif  24479  limccnp  24494  limccnp2  24495  limcco  24496  dvn2bss  24533  cpnord  24538  dvcmulf  24548  dvmptres2  24565  dvmptcmul  24567  dvmptntr  24574  dvcnvrelem2  24621  dvcnvre  24622  taylthlem1  24968  taylthlem2  24969  ulmdvlem3  24997  psercnlem2  25019  rlimcxp  25559  o1cxp  25560  sspg  28511  ssps  28513  sspn  28519  mdslj1i  30102  mdslj2i  30103  sh1dle  30134  shatomistici  30144  sumdmdii  30198  unidifsnel  30307  resf1o  30492  gsumpart  30740  gsumhashmul  30741  symgcom2  30778  submarchi  30865  idlinsubrg  31016  fedgmullem1  31113  fedgmullem2  31114  fedgmul  31115  extdg1id  31141  madjusmdetlem1  31180  txomap  31187  rspectopn  31220  zarclssn  31226  zarcmplem  31234  cnvordtrestixx  31266  dya2iocucvr  31652  carsggect  31686  bnj1241  32189  bnj906  32312  cvmscld  32633  nosupbnd2lem1  33328  noetalem4  33333  fvline2  33720  cldregopn  33792  pibt2  34834  poimirlem15  35072  sstotbnd2  35212  totbndbnd  35227  heibor1  35248  heiborlem8  35256  lsmsat  36304  lssats  36308  lkrpssN  36459  dia2dimlem5  38364  cdlemn2a  38492  dihglblem6  38636  dochocsp  38675  dochdmj1  38686  dochsatshpb  38748  lcfl9a  38801  lclkrlem2r  38820  lclkrlem2s  38821  lclkrlem2v  38824  lcfrlem6  38843  lcfrlem25  38863  lcfrlem35  38873  mapdval2N  38926  mapdin  38958  baerlem5alem2  39007  baerlem5blem2  39008  dnnumch2  39989  clrellem  40322  iunrelexpmin1  40409  iunrelexpmin2  40413  dftrcl3  40421  brtrclfv2  40428  dfrtrcl3  40434  mnuprdlem1  40980  mnuprdlem2  40981  mullimc  42258  islptre  42261  mullimcf  42265  limcmptdm  42277  dvresntr  42560  itgperiod  42623  fourierdlem89  42837  fourierdlem91  42839  iccpartgt  43944  resmgmhm2  44419  setrecsres  45231