Theorem eqsstrrd 4006

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

Syntax hints:   → wi 4   = wceq 1537   ⊆ wss 3936

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 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-in 3943  df-ss 3952

This theorem is referenced by:  ssxpb  6031  fnsnr  6927  suppssof1  7863  oaword1  8178  omword2  8200  oeeui  8228  nnaword1  8255  cantnfle  9134  cantnflem1d  9151  r1val1  9215  rankr1id  9291  rankxplim3  9310  ackbij2  9665  ttukeylem7  9937  gruima  10224  hashdmpropge2  13842  rlimi  14870  rlimi2  14871  lo1bdd  14877  o1bdd  14888  rlimuni  14907  rlimcld2  14935  o1co  14943  rlimcn1  14945  rlimcn2  14947  o1add2  14980  o1mul2  14981  o1sub2  14982  lo1add  14983  lo1mul  14984  o1dif  14986  rlimneg  15003  rlimsqzlem  15005  lo1le  15008  rlimno1  15010  ramub1lem1  16362  imasaddfnlem  16801  imasvscafn  16810  mrcidb  16886  mrieqv2d  16910  mreexexlem4d  16918  funcres  17166  funcsetcres2  17353  acsfiindd  17787  tsrdir  17848  resmhm2  17986  f1omvdco2  18576  sylow2a  18744  sylow3lem6  18757  dprdspan  19149  dprd2dlem2  19162  dprd2dlem1  19163  dprd2da  19164  dmdprdsplit2lem  19167  dprdsplit  19170  dpjcntz  19174  ablfac1eu  19195  ringidss  19327  subrg1  19545  subrgdvds  19549  subrguss  19550  subrginv  19551  subdrgint  19582  primefld  19584  islss3  19731  lspsnneg  19778  lspextmo  19828  lspsnvs  19886  lsmcv  19913  islbs3  19927  drngdomn  20076  psrbaglesupp  20148  resspsrbas  20195  resspsradd  20196  resspsrmul  20197  evlseu  20296  f1lindf  20966  epttop  21617  neitr  21788  ordtbas  21800  ordtrest2  21812  pnfnei  21828  mnfnei  21829  ordtrestixx  21830  dnsconst  21986  cmpcld  22010  txindis  22242  txtube  22248  xkohaus  22261  xkopt  22263  xkococnlem  22267  xkoinjcn  22295  qtopval2  22304  ssufl  22526  ufldom  22570  cnextcn  22675  tmdgsum2  22704  clssubg  22717  clsnsg  22718  ustund  22830  ustneism  22832  trust  22838  fmucnd  22901  imasdsf1olem  22983  setsmstopn  23088  metequiv2  23120  metust  23168  restmetu  23180  tngtopn  23259  xlebnum  23569  pi1xfrcnv  23661  limcdif  24474  limccnp  24489  limccnp2  24490  limcco  24491  dvn2bss  24527  cpnord  24532  dvcmulf  24542  dvmptres2  24559  dvmptcmul  24561  dvmptntr  24568  dvcnvrelem2  24615  dvcnvre  24616  taylthlem1  24961  taylthlem2  24962  ulmdvlem3  24990  psercnlem2  25012  rlimcxp  25551  o1cxp  25552  sspg  28505  ssps  28507  sspn  28513  mdslj1i  30096  mdslj2i  30097  sh1dle  30128  shatomistici  30138  sumdmdii  30192  unidifsnel  30295  resf1o  30466  symgcom2  30728  submarchi  30815  fedgmullem1  31025  fedgmullem2  31026  fedgmul  31027  extdg1id  31053  madjusmdetlem1  31092  txomap  31098  cnvordtrestixx  31156  dya2iocucvr  31542  carsggect  31576  bnj1241  32079  bnj906  32202  cvmscld  32520  nosupbnd2lem1  33215  noetalem4  33220  fvline2  33607  cldregopn  33679  pibt2  34701  poimirlem15  34922  sstotbnd2  35067  totbndbnd  35082  heibor1  35103  heiborlem8  35111  lsmsat  36159  lssats  36163  lkrpssN  36314  dia2dimlem5  38219  cdlemn2a  38347  dihglblem6  38491  dochocsp  38530  dochdmj1  38541  dochsatshpb  38603  lcfl9a  38656  lclkrlem2r  38675  lclkrlem2s  38676  lclkrlem2v  38679  lcfrlem6  38698  lcfrlem25  38718  lcfrlem35  38728  mapdval2N  38781  mapdin  38813  baerlem5alem2  38862  baerlem5blem2  38863  dnnumch2  39694  clrellem  40031  iunrelexpmin1  40102  iunrelexpmin2  40106  dftrcl3  40114  brtrclfv2  40121  dfrtrcl3  40127  mnuprdlem1  40657  mnuprdlem2  40658  mullimc  41946  islptre  41949  mullimcf  41953  limcmptdm  41965  dvresntr  42251  itgperiod  42315  fourierdlem89  42529  fourierdlem91  42531  iccpartgt  43636  resmgmhm2  44115  setrecsres  44853