MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  eqsstr3d Structured version   Visualization version   GIF version

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
StepHypRef Expression
1 eqsstr3d.1 . . 3 (𝜑𝐵 = 𝐴)
21eqcomd 2616 . 2 (𝜑𝐴 = 𝐵)
3 eqsstr3d.2 . 2 (𝜑𝐵𝐶)
42, 3eqsstrd 3602 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
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  5473  fnsnb  6315  suppssof1  7193  oaword1  7497  omword2  7519  oeeui  7547  nnaword1  7574  cantnfle  8429  cantnflem1d  8446  r1val1  8510  rankr1id  8586  rankxplim3  8605  ackbij2  8926  ttukeylem7  9198  gruima  9481  rlimi  14041  rlimi2  14042  lo1bdd  14048  o1bdd  14059  rlimuni  14078  rlimcld2  14106  o1co  14114  rlimcn1  14116  rlimcn2  14118  o1add2  14151  o1mul2  14152  o1sub2  14153  lo1add  14154  lo1mul  14155  o1dif  14157  rlimneg  14174  rlimsqzlem  14176  lo1le  14179  rlimno1  14181  ramub1lem1  15517  imasaddfnlem  15960  imasvscafn  15969  mrcidb  16047  mrieqv2d  16071  mreexexlem4d  16079  funcres  16328  funcsetcres2  16515  acsfiindd  16949  tsrdir  17010  resmhm2  17132  f1omvdco2  17640  sylow2a  17806  sylow3lem6  17819  dprdspan  18198  dprd2dlem2  18211  dprd2dlem1  18212  dprd2da  18213  dmdprdsplit2lem  18216  dprdsplit  18219  dpjcntz  18223  ablfac1eu  18244  ringidss  18349  subrg1  18562  subrgdvds  18566  subrguss  18567  subrginv  18568  islss3  18729  lspsnneg  18776  lspextmo  18826  lspsnvs  18884  lsmcv  18911  islbs3  18925  drngdomn  19073  psrbaglesupp  19138  resspsrbas  19185  resspsradd  19186  resspsrmul  19187  evlseu  19286  f1lindf  19928  epttop  20571  neitr  20742  ordtbas  20754  ordtrest2  20766  pnfnei  20782  mnfnei  20783  ordtrestixx  20784  dnsconst  20940  cmpcld  20963  txindis  21195  txtube  21201  xkohaus  21214  xkopt  21216  xkococnlem  21220  xkoinjcn  21248  qtopval2  21257  ssufl  21480  ufldom  21524  cnextcn  21629  tmdgsum2  21658  clssubg  21670  clsnsg  21671  ustund  21783  ustneism  21785  trust  21791  fmucnd  21854  imasdsf1olem  21936  setsmstopn  22041  metequiv2  22073  metust  22121  restmetu  22133  tngtopn  22212  xlebnum  22520  pi1xfrcnv  22613  limcdif  23391  limccnp  23406  limccnp2  23407  limcco  23408  dvn2bss  23444  cpnord  23449  dvcmulf  23459  dvmptres2  23476  dvmptcmul  23478  dvmptntr  23485  dvcnvrelem2  23530  dvcnvre  23531  taylthlem1  23876  taylthlem2  23877  ulmdvlem3  23905  psercnlem2  23927  rlimcxp  24445  o1cxp  24446  nbgrassovt  25758  sspg  26761  ssps  26763  sspn  26769  mdslj1i  28356  mdslj2i  28357  sh1dle  28388  shatomistici  28398  sumdmdii  28452  resf1o  28687  submarchi  28865  madjusmdetlem1  29015  txomap  29023  cnvordtrestixx  29081  dya2iocucvr  29467  carsggect  29501  bnj142OLD  29842  bnj1241  29926  bnj906  30048  cvmscld  30303  nofulllem3  30897  fvline2  31217  cldregopn  31290  poimirlem15  32388  sstotbnd2  32537  totbndbnd  32552  heibor1  32573  heiborlem8  32581  lsmsat  33107  lssats  33111  lkrpssN  33262  dia2dimlem5  35169  cdlemn2a  35297  dihglblem6  35441  dochocsp  35480  dochdmj1  35491  dochsatshpb  35553  lcfl9a  35606  lclkrlem2r  35625  lclkrlem2s  35626  lclkrlem2v  35629  lcfrlem6  35648  lcfrlem25  35668  lcfrlem35  35678  mapdval2N  35731  mapdin  35763  baerlem5alem2  35812  baerlem5blem2  35813  dnnumch2  36427  clrellem  36742  iunrelexpmin1  36813  iunrelexpmin2  36817  dftrcl3  36825  brtrclfv2  36832  dfrtrcl3  36838  mullimc  38477  islptre  38480  mullimcf  38484  limcmptdm  38496  dvresntr  38600  itgperiod  38667  fourierdlem89  38882  fourierdlem91  38884  iccpartgt  39760  structgrssvtxlem  40248  uspgrupgrushgr  40399  resmgmhm2  41581
  Copyright terms: Public domain W3C validator