Theorem eqsstrrd 4021

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

Syntax hints:   → wi 4   = wceq 1540   ⊆ wss 3948

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1543  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3475  df-in 3955  df-ss 3965

This theorem is referenced by:  ssxpb  6173  fnsnr  7165  suppssof1  8188  oaword1  8556  omword2  8578  oeeui  8606  nnaword1  8633  naddword1  8694  naddunif  8696  cantnfle  9670  cantnflem1d  9687  r1val1  9785  rankr1id  9861  rankxplim3  9880  ackbij2  10242  ttukeylem7  10514  gruima  10801  hashdmpropge2  14449  rlimi  15462  rlimi2  15463  lo1bdd  15469  o1bdd  15480  rlimuni  15499  rlimcld2  15527  o1co  15535  rlimcn1  15537  rlimcn3  15539  o1add2  15573  o1mul2  15574  o1sub2  15575  lo1add  15576  lo1mul  15577  o1dif  15579  rlimneg  15598  rlimsqzlem  15600  lo1le  15603  rlimno1  15605  ramub1lem1  16964  imasaddfnlem  17479  imasvscafn  17488  mrcidb  17564  mrieqv2d  17588  mreexexlem4d  17596  funcres  17851  funcsetcres2  18048  acsfiindd  18511  tsrdir  18562  resmgmhm2  18638  resmhm2  18739  f1omvdco2  19358  sylow2a  19529  sylow3lem6  19542  dprdspan  19939  dprd2dlem2  19952  dprd2dlem1  19953  dprd2da  19954  dmdprdsplit2lem  19957  dprdsplit  19960  dpjcntz  19964  ablfac1eu  19985  ringidss  20166  subrg1  20473  subrgdvds  20477  subrguss  20478  subrginv  20479  subdrgint  20563  primefld  20565  islss3  20715  lspsnneg  20762  lspextmo  20812  lspsnvs  20873  lsmcv  20900  islbs3  20914  drngdomn  21122  f1lindf  21597  psrbaglesupp  21697  psrbaglesuppOLD  21698  resspsrbas  21755  resspsradd  21756  resspsrmul  21757  evlseu  21866  epttop  22733  neitr  22905  ordtbas  22917  ordtrest2  22929  pnfnei  22945  mnfnei  22946  ordtrestixx  22947  dnsconst  23103  cmpcld  23127  txindis  23359  txtube  23365  xkohaus  23378  xkopt  23380  xkococnlem  23384  xkoinjcn  23412  qtopval2  23421  ssufl  23643  ufldom  23687  cnextcn  23792  tmdgsum2  23821  clssubg  23834  clsnsg  23835  ustund  23947  ustneism  23949  trust  23955  fmucnd  24018  imasdsf1olem  24100  setsmstopn  24207  metequiv2  24240  metust  24288  restmetu  24300  tngtopn  24388  xlebnum  24712  pi1xfrcnv  24805  limcdif  25626  limccnp  25641  limccnp2  25642  limcco  25643  dvn2bss  25681  cpnord  25686  dvcmulf  25697  dvmptres2  25715  dvmptcmul  25717  dvmptntr  25724  dvcnvrelem2  25771  dvcnvre  25772  taylthlem1  26122  taylthlem2  26123  ulmdvlem3  26151  psercnlem2  26173  rlimcxp  26715  o1cxp  26716  nosupbnd2lem1  27455  noinfbnd2lem1  27470  noetainflem4  27480  negsbday  27771  sspg  30249  ssps  30251  sspn  30257  mdslj1i  31840  mdslj2i  31841  sh1dle  31872  shatomistici  31882  sumdmdii  31936  unidifsnel  32040  resf1o  32223  gsumpart  32478  gsumhashmul  32479  symgcom2  32516  submarchi  32603  nsgmgc  32798  ghmquskerlem3  32806  ghmqusker  32807  lmhmqusker  32809  rhmquskerlem  32818  idlinsubrg  32824  ply1degltdimlem  32996  fedgmullem1  33003  fedgmullem2  33004  fedgmul  33005  extdg1id  33031  madjusmdetlem1  33106  txomap  33113  rspectopn  33146  zarclssn  33152  zarcmplem  33160  cnvordtrestixx  33192  dya2iocucvr  33582  carsggect  33616  bnj1241  34117  bnj906  34240  fineqvac  34396  cvmscld  34563  fvline2  35423  cldregopn  35520  pibt2  36602  poimirlem15  36807  sstotbnd2  36946  totbndbnd  36961  heibor1  36982  heiborlem8  36990  lsmsat  38182  lssats  38186  lkrpssN  38337  dia2dimlem5  40243  cdlemn2a  40371  dihglblem6  40515  dochocsp  40554  dochdmj1  40565  dochsatshpb  40627  lcfl9a  40680  lclkrlem2r  40699  lclkrlem2s  40700  lclkrlem2v  40703  lcfrlem6  40722  lcfrlem25  40742  lcfrlem35  40752  mapdval2N  40805  mapdin  40837  baerlem5alem2  40886  baerlem5blem2  40887  evlsvvval  41438  evlsbagval  41441  evlsmhpvvval  41470  mhphf  41472  dnnumch2  42090  oege1  42359  omabs2  42385  nadd2rabex  42439  clrellem  42676  iunrelexpmin1  42762  iunrelexpmin2  42766  dftrcl3  42774  brtrclfv2  42781  dfrtrcl3  42787  mnuprdlem1  43334  mnuprdlem2  43335  mullimc  44631  islptre  44634  mullimcf  44638  limcmptdm  44650  dvresntr  44933  itgperiod  44996  fourierdlem89  45210  fourierdlem91  45212  iccpartgt  46394  setrecsres  47835