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

Theorem eqsstr3d 3781
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 2766 . 2 (𝜑𝐴 = 𝐵)
3 eqsstr3d.2 . 2 (𝜑𝐵𝐶)
42, 3eqsstrd 3780 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1632  wss 3715
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-in 3722  df-ss 3729
This theorem is referenced by:  ssxpb  5726  fnsnr  6596  suppssof1  7498  oaword1  7803  omword2  7825  oeeui  7853  nnaword1  7880  cantnfle  8743  cantnflem1d  8760  r1val1  8824  rankr1id  8900  rankxplim3  8919  ackbij2  9277  ttukeylem7  9549  gruima  9836  hashdmpropge2  13477  rlimi  14463  rlimi2  14464  lo1bdd  14470  o1bdd  14481  rlimuni  14500  rlimcld2  14528  o1co  14536  rlimcn1  14538  rlimcn2  14540  o1add2  14573  o1mul2  14574  o1sub2  14575  lo1add  14576  lo1mul  14577  o1dif  14579  rlimneg  14596  rlimsqzlem  14598  lo1le  14601  rlimno1  14603  ramub1lem1  15952  imasaddfnlem  16410  imasvscafn  16419  mrcidb  16497  mrieqv2d  16521  mreexexlem4d  16529  funcres  16777  funcsetcres2  16964  acsfiindd  17398  tsrdir  17459  resmhm2  17581  f1omvdco2  18088  sylow2a  18254  sylow3lem6  18267  dprdspan  18646  dprd2dlem2  18659  dprd2dlem1  18660  dprd2da  18661  dmdprdsplit2lem  18664  dprdsplit  18667  dpjcntz  18671  ablfac1eu  18692  ringidss  18797  subrg1  19012  subrgdvds  19016  subrguss  19017  subrginv  19018  islss3  19181  lspsnneg  19228  lspextmo  19278  lspsnvs  19336  lsmcv  19363  islbs3  19377  drngdomn  19525  psrbaglesupp  19590  resspsrbas  19637  resspsradd  19638  resspsrmul  19639  evlseu  19738  f1lindf  20383  epttop  21035  neitr  21206  ordtbas  21218  ordtrest2  21230  pnfnei  21246  mnfnei  21247  ordtrestixx  21248  dnsconst  21404  cmpcld  21427  txindis  21659  txtube  21665  xkohaus  21678  xkopt  21680  xkococnlem  21684  xkoinjcn  21712  qtopval2  21721  ssufl  21943  ufldom  21987  cnextcn  22092  tmdgsum2  22121  clssubg  22133  clsnsg  22134  ustund  22246  ustneism  22248  trust  22254  fmucnd  22317  imasdsf1olem  22399  setsmstopn  22504  metequiv2  22536  metust  22584  restmetu  22596  tngtopn  22675  xlebnum  22985  pi1xfrcnv  23077  limcdif  23859  limccnp  23874  limccnp2  23875  limcco  23876  dvn2bss  23912  cpnord  23917  dvcmulf  23927  dvmptres2  23944  dvmptcmul  23946  dvmptntr  23953  dvcnvrelem2  24000  dvcnvre  24001  taylthlem1  24346  taylthlem2  24347  ulmdvlem3  24375  psercnlem2  24397  rlimcxp  24920  o1cxp  24921  structgrssvtxlemOLD  26135  sspg  27913  ssps  27915  sspn  27921  mdslj1i  29508  mdslj2i  29509  sh1dle  29540  shatomistici  29550  sumdmdii  29604  resf1o  29835  submarchi  30070  madjusmdetlem1  30223  txomap  30231  cnvordtrestixx  30289  dya2iocucvr  30676  carsggect  30710  bnj1241  31206  bnj906  31328  cvmscld  31583  nosupbnd2lem1  32188  noetalem4  32193  fvline2  32580  cldregopn  32653  poimirlem15  33755  sstotbnd2  33904  totbndbnd  33919  heibor1  33940  heiborlem8  33948  lsmsat  34816  lssats  34820  lkrpssN  34971  dia2dimlem5  36877  cdlemn2a  37005  dihglblem6  37149  dochocsp  37188  dochdmj1  37199  dochsatshpb  37261  lcfl9a  37314  lclkrlem2r  37333  lclkrlem2s  37334  lclkrlem2v  37337  lcfrlem6  37356  lcfrlem25  37376  lcfrlem35  37386  mapdval2N  37439  mapdin  37471  baerlem5alem2  37520  baerlem5blem2  37521  dnnumch2  38135  clrellem  38449  iunrelexpmin1  38520  iunrelexpmin2  38524  dftrcl3  38532  brtrclfv2  38539  dfrtrcl3  38545  mullimc  40369  islptre  40372  mullimcf  40376  limcmptdm  40388  dvresntr  40653  itgperiod  40718  fourierdlem89  40933  fourierdlem91  40935  iccpartgt  41891  resmgmhm2  42327  setrecsres  42976
  Copyright terms: Public domain W3C validator