Theorem eqsstr3d 3640

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

Syntax hints:   → wi 4   = wceq 1483   ⊆ wss 3574

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-in 3581  df-ss 3588

This theorem is referenced by:  ssxpb  5568  fnsnb  6432  suppssof1  7328  oaword1  7632  omword2  7654  oeeui  7682  nnaword1  7709  cantnfle  8568  cantnflem1d  8585  r1val1  8649  rankr1id  8725  rankxplim3  8744  ackbij2  9065  ttukeylem7  9337  gruima  9624  hashdmpropge2  13265  rlimi  14244  rlimi2  14245  lo1bdd  14251  o1bdd  14262  rlimuni  14281  rlimcld2  14309  o1co  14317  rlimcn1  14319  rlimcn2  14321  o1add2  14354  o1mul2  14355  o1sub2  14356  lo1add  14357  lo1mul  14358  o1dif  14360  rlimneg  14377  rlimsqzlem  14379  lo1le  14382  rlimno1  14384  ramub1lem1  15730  imasaddfnlem  16188  imasvscafn  16197  mrcidb  16275  mrieqv2d  16299  mreexexlem4d  16307  funcres  16556  funcsetcres2  16743  acsfiindd  17177  tsrdir  17238  resmhm2  17360  f1omvdco2  17868  sylow2a  18034  sylow3lem6  18047  dprdspan  18426  dprd2dlem2  18439  dprd2dlem1  18440  dprd2da  18441  dmdprdsplit2lem  18444  dprdsplit  18447  dpjcntz  18451  ablfac1eu  18472  ringidss  18577  subrg1  18790  subrgdvds  18794  subrguss  18795  subrginv  18796  islss3  18959  lspsnneg  19006  lspextmo  19056  lspsnvs  19114  lsmcv  19141  islbs3  19155  drngdomn  19303  psrbaglesupp  19368  resspsrbas  19415  resspsradd  19416  resspsrmul  19417  evlseu  19516  f1lindf  20161  epttop  20813  neitr  20984  ordtbas  20996  ordtrest2  21008  pnfnei  21024  mnfnei  21025  ordtrestixx  21026  dnsconst  21182  cmpcld  21205  txindis  21437  txtube  21443  xkohaus  21456  xkopt  21458  xkococnlem  21462  xkoinjcn  21490  qtopval2  21499  ssufl  21722  ufldom  21766  cnextcn  21871  tmdgsum2  21900  clssubg  21912  clsnsg  21913  ustund  22025  ustneism  22027  trust  22033  fmucnd  22096  imasdsf1olem  22178  setsmstopn  22283  metequiv2  22315  metust  22363  restmetu  22375  tngtopn  22454  xlebnum  22764  pi1xfrcnv  22857  limcdif  23640  limccnp  23655  limccnp2  23656  limcco  23657  dvn2bss  23693  cpnord  23698  dvcmulf  23708  dvmptres2  23725  dvmptcmul  23727  dvmptntr  23734  dvcnvrelem2  23781  dvcnvre  23782  taylthlem1  24127  taylthlem2  24128  ulmdvlem3  24156  psercnlem2  24178  rlimcxp  24700  o1cxp  24701  structgrssvtxlemOLD  25915  sspg  27583  ssps  27585  sspn  27591  mdslj1i  29178  mdslj2i  29179  sh1dle  29210  shatomistici  29220  sumdmdii  29274  resf1o  29505  submarchi  29740  madjusmdetlem1  29893  txomap  29901  cnvordtrestixx  29959  dya2iocucvr  30346  carsggect  30380  bnj142OLD  30794  bnj1241  30878  bnj906  31000  cvmscld  31255  nosupbnd2lem1  31861  noetalem4  31866  fvline2  32253  cldregopn  32326  poimirlem15  33424  sstotbnd2  33573  totbndbnd  33588  heibor1  33609  heiborlem8  33617  lsmsat  34295  lssats  34299  lkrpssN  34450  dia2dimlem5  36357  cdlemn2a  36485  dihglblem6  36629  dochocsp  36668  dochdmj1  36679  dochsatshpb  36741  lcfl9a  36794  lclkrlem2r  36813  lclkrlem2s  36814  lclkrlem2v  36817  lcfrlem6  36836  lcfrlem25  36856  lcfrlem35  36866  mapdval2N  36919  mapdin  36951  baerlem5alem2  37000  baerlem5blem2  37001  dnnumch2  37615  clrellem  37929  iunrelexpmin1  38000  iunrelexpmin2  38004  dftrcl3  38012  brtrclfv2  38019  dfrtrcl3  38025  mullimc  39848  islptre  39851  mullimcf  39855  limcmptdm  39867  dvresntr  40132  itgperiod  40197  fourierdlem89  40412  fourierdlem91  40414  iccpartgt  41363  resmgmhm2  41799