Theorem eqsstrrd 4020

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

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

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-v 3474  df-in 3954  df-ss 3964

This theorem is referenced by:  ssxpb  6172  fnsnr  7164  suppssof1  8186  oaword1  8554  omword2  8576  oeeui  8604  nnaword1  8631  naddword1  8692  naddunif  8694  cantnfle  9668  cantnflem1d  9685  r1val1  9783  rankr1id  9859  rankxplim3  9878  ackbij2  10240  ttukeylem7  10512  gruima  10799  hashdmpropge2  14448  rlimi  15461  rlimi2  15462  lo1bdd  15468  o1bdd  15479  rlimuni  15498  rlimcld2  15526  o1co  15534  rlimcn1  15536  rlimcn3  15538  o1add2  15572  o1mul2  15573  o1sub2  15574  lo1add  15575  lo1mul  15576  o1dif  15578  rlimneg  15597  rlimsqzlem  15599  lo1le  15602  rlimno1  15604  ramub1lem1  16963  imasaddfnlem  17478  imasvscafn  17487  mrcidb  17563  mrieqv2d  17587  mreexexlem4d  17595  funcres  17850  funcsetcres2  18047  acsfiindd  18510  tsrdir  18561  resmgmhm2  18637  resmhm2  18738  f1omvdco2  19357  sylow2a  19528  sylow3lem6  19541  dprdspan  19938  dprd2dlem2  19951  dprd2dlem1  19952  dprd2da  19953  dmdprdsplit2lem  19956  dprdsplit  19959  dpjcntz  19963  ablfac1eu  19984  ringidss  20165  subrg1  20472  subrgdvds  20476  subrguss  20477  subrginv  20478  subdrgint  20562  primefld  20564  islss3  20714  lspsnneg  20761  lspextmo  20811  lspsnvs  20872  lsmcv  20899  islbs3  20913  drngdomn  21121  f1lindf  21596  psrbaglesupp  21696  psrbaglesuppOLD  21697  resspsrbas  21754  resspsradd  21755  resspsrmul  21756  evlseu  21865  epttop  22732  neitr  22904  ordtbas  22916  ordtrest2  22928  pnfnei  22944  mnfnei  22945  ordtrestixx  22946  dnsconst  23102  cmpcld  23126  txindis  23358  txtube  23364  xkohaus  23377  xkopt  23379  xkococnlem  23383  xkoinjcn  23411  qtopval2  23420  ssufl  23642  ufldom  23686  cnextcn  23791  tmdgsum2  23820  clssubg  23833  clsnsg  23834  ustund  23946  ustneism  23948  trust  23954  fmucnd  24017  imasdsf1olem  24099  setsmstopn  24206  metequiv2  24239  metust  24287  restmetu  24299  tngtopn  24387  xlebnum  24711  pi1xfrcnv  24804  limcdif  25625  limccnp  25640  limccnp2  25641  limcco  25642  dvn2bss  25680  cpnord  25685  dvcmulf  25696  dvmptres2  25714  dvmptcmul  25716  dvmptntr  25723  dvcnvrelem2  25770  dvcnvre  25771  taylthlem1  26121  taylthlem2  26122  ulmdvlem3  26150  psercnlem2  26172  rlimcxp  26714  o1cxp  26715  nosupbnd2lem1  27454  noinfbnd2lem1  27469  noetainflem4  27479  negsbday  27770  sspg  30248  ssps  30250  sspn  30256  mdslj1i  31839  mdslj2i  31840  sh1dle  31871  shatomistici  31881  sumdmdii  31935  unidifsnel  32039  resf1o  32222  gsumpart  32477  gsumhashmul  32478  symgcom2  32515  submarchi  32602  nsgmgc  32797  ghmquskerlem3  32805  ghmqusker  32806  lmhmqusker  32808  rhmquskerlem  32817  idlinsubrg  32823  ply1degltdimlem  32995  fedgmullem1  33002  fedgmullem2  33003  fedgmul  33004  extdg1id  33030  madjusmdetlem1  33105  txomap  33112  rspectopn  33145  zarclssn  33151  zarcmplem  33159  cnvordtrestixx  33191  dya2iocucvr  33581  carsggect  33615  bnj1241  34116  bnj906  34239  fineqvac  34395  cvmscld  34562  fvline2  35422  cldregopn  35519  pibt2  36601  poimirlem15  36806  sstotbnd2  36945  totbndbnd  36960  heibor1  36981  heiborlem8  36989  lsmsat  38181  lssats  38185  lkrpssN  38336  dia2dimlem5  40242  cdlemn2a  40370  dihglblem6  40514  dochocsp  40553  dochdmj1  40564  dochsatshpb  40626  lcfl9a  40679  lclkrlem2r  40698  lclkrlem2s  40699  lclkrlem2v  40702  lcfrlem6  40721  lcfrlem25  40741  lcfrlem35  40751  mapdval2N  40804  mapdin  40836  baerlem5alem2  40885  baerlem5blem2  40886  evlsvvval  41437  evlsbagval  41440  evlsmhpvvval  41469  mhphf  41471  dnnumch2  42089  oege1  42358  omabs2  42384  nadd2rabex  42438  clrellem  42675  iunrelexpmin1  42761  iunrelexpmin2  42765  dftrcl3  42773  brtrclfv2  42780  dfrtrcl3  42786  mnuprdlem1  43333  mnuprdlem2  43334  mullimc  44630  islptre  44633  mullimcf  44637  limcmptdm  44649  dvresntr  44932  itgperiod  44995  fourierdlem89  45209  fourierdlem91  45211  iccpartgt  46393  setrecsres  47834