Theorem eqsstr3d 3603

Description: Substitution of equality into a subclass relationship. (Contributed by NM, 25-Apr-2004.)

Hypotheses

Ref	Expression
eqsstr3d.1	⊢ (𝜑 → 𝐵 = 𝐴)
eqsstr3d.2	⊢ (𝜑 → 𝐵 ⊆ 𝐶)

Assertion

Ref	Expression
eqsstr3d	⊢ (𝜑 → 𝐴 ⊆ 𝐶)

Proof of Theorem eqsstr3d

Step	Hyp	Ref	Expression
1		eqsstr3d.1	. . 3 ⊢ (𝜑 → 𝐵 = 𝐴)
2	1	eqcomd 2616	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
3		eqsstr3d.2	. 2 ⊢ (𝜑 → 𝐵 ⊆ 𝐶)
4	2, 3	eqsstrd 3602	1 ⊢ (𝜑 → 𝐴 ⊆ 𝐶)

Syntax hints:   → wi 4   = wceq 1475   ⊆ wss 3540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-in 3547  df-ss 3554

This theorem is referenced by:  ssxpb  5487  fnsnb  6337  suppssof1  7215  oaword1  7519  omword2  7541  oeeui  7569  nnaword1  7596  cantnfle  8451  cantnflem1d  8468  r1val1  8532  rankr1id  8608  rankxplim3  8627  ackbij2  8948  ttukeylem7  9220  gruima  9503  rlimi  14092  rlimi2  14093  lo1bdd  14099  o1bdd  14110  rlimuni  14129  rlimcld2  14157  o1co  14165  rlimcn1  14167  rlimcn2  14169  o1add2  14202  o1mul2  14203  o1sub2  14204  lo1add  14205  lo1mul  14206  o1dif  14208  rlimneg  14225  rlimsqzlem  14227  lo1le  14230  rlimno1  14232  ramub1lem1  15568  imasaddfnlem  16011  imasvscafn  16020  mrcidb  16098  mrieqv2d  16122  mreexexlem4d  16130  funcres  16379  funcsetcres2  16566  acsfiindd  17000  tsrdir  17061  resmhm2  17183  f1omvdco2  17691  sylow2a  17857  sylow3lem6  17870  dprdspan  18249  dprd2dlem2  18262  dprd2dlem1  18263  dprd2da  18264  dmdprdsplit2lem  18267  dprdsplit  18270  dpjcntz  18274  ablfac1eu  18295  ringidss  18400  subrg1  18613  subrgdvds  18617  subrguss  18618  subrginv  18619  islss3  18780  lspsnneg  18827  lspextmo  18877  lspsnvs  18935  lsmcv  18962  islbs3  18976  drngdomn  19124  psrbaglesupp  19189  resspsrbas  19236  resspsradd  19237  resspsrmul  19238  evlseu  19337  f1lindf  19980  epttop  20623  neitr  20794  ordtbas  20806  ordtrest2  20818  pnfnei  20834  mnfnei  20835  ordtrestixx  20836  dnsconst  20992  cmpcld  21015  txindis  21247  txtube  21253  xkohaus  21266  xkopt  21268  xkococnlem  21272  xkoinjcn  21300  qtopval2  21309  ssufl  21532  ufldom  21576  cnextcn  21681  tmdgsum2  21710  clssubg  21722  clsnsg  21723  ustund  21835  ustneism  21837  trust  21843  fmucnd  21906  imasdsf1olem  21988  setsmstopn  22093  metequiv2  22125  metust  22173  restmetu  22185  tngtopn  22264  xlebnum  22572  pi1xfrcnv  22665  limcdif  23446  limccnp  23461  limccnp2  23462  limcco  23463  dvn2bss  23499  cpnord  23504  dvcmulf  23514  dvmptres2  23531  dvmptcmul  23533  dvmptntr  23540  dvcnvrelem2  23585  dvcnvre  23586  taylthlem1  23931  taylthlem2  23932  ulmdvlem3  23960  psercnlem2  23982  rlimcxp  24500  o1cxp  24501  structgrssvtxlem  25700  nbgrassovt  25964  sspg  26967  ssps  26969  sspn  26975  mdslj1i  28562  mdslj2i  28563  sh1dle  28594  shatomistici  28604  sumdmdii  28658  resf1o  28893  submarchi  29071  madjusmdetlem1  29221  txomap  29229  cnvordtrestixx  29287  dya2iocucvr  29673  carsggect  29707  bnj142OLD  30048  bnj1241  30132  bnj906  30254  cvmscld  30509  nofulllem3  31103  fvline2  31423  cldregopn  31496  poimirlem15  32594  sstotbnd2  32743  totbndbnd  32758  heibor1  32779  heiborlem8  32787  lsmsat  33313  lssats  33317  lkrpssN  33468  dia2dimlem5  35375  cdlemn2a  35503  dihglblem6  35647  dochocsp  35686  dochdmj1  35697  dochsatshpb  35759  lcfl9a  35812  lclkrlem2r  35831  lclkrlem2s  35832  lclkrlem2v  35835  lcfrlem6  35854  lcfrlem25  35874  lcfrlem35  35884  mapdval2N  35937  mapdin  35969  baerlem5alem2  36018  baerlem5blem2  36019  dnnumch2  36633  clrellem  36948  iunrelexpmin1  37019  iunrelexpmin2  37023  dftrcl3  37031  brtrclfv2  37038  dfrtrcl3  37044  mullimc  38683  islptre  38686  mullimcf  38690  limcmptdm  38702  dvresntr  38806  itgperiod  38873  fourierdlem89  39088  fourierdlem91  39090  iccpartgt  39965  uspgrupgrushgr  40407  resmgmhm2  41589