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

Theorem eqsstr3d 3837
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 2812 . 2 (𝜑𝐴 = 𝐵)
3 eqsstr3d.2 . 2 (𝜑𝐵𝐶)
42, 3eqsstrd 3836 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1637  wss 3769
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-ext 2784
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-clab 2793  df-cleq 2799  df-clel 2802  df-in 3776  df-ss 3783
This theorem is referenced by:  ssxpb  5779  fnsnr  6656  suppssof1  7563  oaword1  7869  omword2  7891  oeeui  7919  nnaword1  7946  cantnfle  8815  cantnflem1d  8832  r1val1  8896  rankr1id  8972  rankxplim3  8991  ackbij2  9350  ttukeylem7  9622  gruima  9909  hashdmpropge2  13482  rlimi  14467  rlimi2  14468  lo1bdd  14474  o1bdd  14485  rlimuni  14504  rlimcld2  14532  o1co  14540  rlimcn1  14542  rlimcn2  14544  o1add2  14577  o1mul2  14578  o1sub2  14579  lo1add  14580  lo1mul  14581  o1dif  14583  rlimneg  14600  rlimsqzlem  14602  lo1le  14605  rlimno1  14607  ramub1lem1  15947  imasaddfnlem  16393  imasvscafn  16402  mrcidb  16480  mrieqv2d  16504  mreexexlem4d  16512  funcres  16760  funcsetcres2  16947  acsfiindd  17382  tsrdir  17443  resmhm2  17565  f1omvdco2  18069  sylow2a  18235  sylow3lem6  18248  dprdspan  18628  dprd2dlem2  18641  dprd2dlem1  18642  dprd2da  18643  dmdprdsplit2lem  18646  dprdsplit  18649  dpjcntz  18653  ablfac1eu  18674  ringidss  18779  subrg1  18994  subrgdvds  18998  subrguss  18999  subrginv  19000  islss3  19166  lspsnneg  19213  lspextmo  19263  lspsnvs  19321  lsmcv  19349  islbs3  19364  drngdomn  19512  psrbaglesupp  19577  resspsrbas  19624  resspsradd  19625  resspsrmul  19626  evlseu  19724  f1lindf  20371  epttop  21027  neitr  21198  ordtbas  21210  ordtrest2  21222  pnfnei  21238  mnfnei  21239  ordtrestixx  21240  dnsconst  21396  cmpcld  21419  txindis  21651  txtube  21657  xkohaus  21670  xkopt  21672  xkococnlem  21676  xkoinjcn  21704  qtopval2  21713  ssufl  21935  ufldom  21979  cnextcn  22084  tmdgsum2  22113  clssubg  22125  clsnsg  22126  ustund  22238  ustneism  22240  trust  22246  fmucnd  22309  imasdsf1olem  22391  setsmstopn  22496  metequiv2  22528  metust  22576  restmetu  22588  tngtopn  22667  xlebnum  22977  pi1xfrcnv  23069  limcdif  23854  limccnp  23869  limccnp2  23870  limcco  23871  dvn2bss  23907  cpnord  23912  dvcmulf  23922  dvmptres2  23939  dvmptcmul  23941  dvmptntr  23948  dvcnvrelem2  23995  dvcnvre  23996  taylthlem1  24341  taylthlem2  24342  ulmdvlem3  24370  psercnlem2  24392  rlimcxp  24914  o1cxp  24915  structgrssvtxlemOLD  26129  sspg  27911  ssps  27913  sspn  27919  mdslj1i  29506  mdslj2i  29507  sh1dle  29538  shatomistici  29548  sumdmdii  29602  resf1o  29832  submarchi  30065  madjusmdetlem1  30218  txomap  30226  cnvordtrestixx  30284  dya2iocucvr  30671  carsggect  30705  bnj1241  31201  bnj906  31323  cvmscld  31578  nosupbnd2lem1  32182  noetalem4  32187  fvline2  32574  cldregopn  32647  poimirlem15  33737  sstotbnd2  33884  totbndbnd  33899  heibor1  33920  heiborlem8  33928  lsmsat  34788  lssats  34792  lkrpssN  34943  dia2dimlem5  36849  cdlemn2a  36977  dihglblem6  37121  dochocsp  37160  dochdmj1  37171  dochsatshpb  37233  lcfl9a  37286  lclkrlem2r  37305  lclkrlem2s  37306  lclkrlem2v  37309  lcfrlem6  37328  lcfrlem25  37348  lcfrlem35  37358  mapdval2N  37411  mapdin  37443  baerlem5alem2  37492  baerlem5blem2  37493  dnnumch2  38116  clrellem  38429  iunrelexpmin1  38500  iunrelexpmin2  38504  dftrcl3  38512  brtrclfv2  38519  dfrtrcl3  38525  mullimc  40328  islptre  40331  mullimcf  40335  limcmptdm  40347  dvresntr  40612  itgperiod  40676  fourierdlem89  40891  fourierdlem91  40893  iccpartgt  41938  resmgmhm2  42367  setrecsres  43016
  Copyright terms: Public domain W3C validator