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

Theorem eqsstr3d 3673
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 2657 . 2 (𝜑𝐴 = 𝐵)
3 eqsstr3d.2 . 2 (𝜑𝐵𝐶)
42, 3eqsstrd 3672 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1523  wss 3607
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-in 3614  df-ss 3621
This theorem is referenced by:  ssxpb  5603  fnsnr  6472  suppssof1  7373  oaword1  7677  omword2  7699  oeeui  7727  nnaword1  7754  cantnfle  8606  cantnflem1d  8623  r1val1  8687  rankr1id  8763  rankxplim3  8782  ackbij2  9103  ttukeylem7  9375  gruima  9662  hashdmpropge2  13303  rlimi  14288  rlimi2  14289  lo1bdd  14295  o1bdd  14306  rlimuni  14325  rlimcld2  14353  o1co  14361  rlimcn1  14363  rlimcn2  14365  o1add2  14398  o1mul2  14399  o1sub2  14400  lo1add  14401  lo1mul  14402  o1dif  14404  rlimneg  14421  rlimsqzlem  14423  lo1le  14426  rlimno1  14428  ramub1lem1  15777  imasaddfnlem  16235  imasvscafn  16244  mrcidb  16322  mrieqv2d  16346  mreexexlem4d  16354  funcres  16603  funcsetcres2  16790  acsfiindd  17224  tsrdir  17285  resmhm2  17407  f1omvdco2  17914  sylow2a  18080  sylow3lem6  18093  dprdspan  18472  dprd2dlem2  18485  dprd2dlem1  18486  dprd2da  18487  dmdprdsplit2lem  18490  dprdsplit  18493  dpjcntz  18497  ablfac1eu  18518  ringidss  18623  subrg1  18838  subrgdvds  18842  subrguss  18843  subrginv  18844  islss3  19007  lspsnneg  19054  lspextmo  19104  lspsnvs  19162  lsmcv  19189  islbs3  19203  drngdomn  19351  psrbaglesupp  19416  resspsrbas  19463  resspsradd  19464  resspsrmul  19465  evlseu  19564  f1lindf  20209  epttop  20861  neitr  21032  ordtbas  21044  ordtrest2  21056  pnfnei  21072  mnfnei  21073  ordtrestixx  21074  dnsconst  21230  cmpcld  21253  txindis  21485  txtube  21491  xkohaus  21504  xkopt  21506  xkococnlem  21510  xkoinjcn  21538  qtopval2  21547  ssufl  21769  ufldom  21813  cnextcn  21918  tmdgsum2  21947  clssubg  21959  clsnsg  21960  ustund  22072  ustneism  22074  trust  22080  fmucnd  22143  imasdsf1olem  22225  setsmstopn  22330  metequiv2  22362  metust  22410  restmetu  22422  tngtopn  22501  xlebnum  22811  pi1xfrcnv  22903  limcdif  23685  limccnp  23700  limccnp2  23701  limcco  23702  dvn2bss  23738  cpnord  23743  dvcmulf  23753  dvmptres2  23770  dvmptcmul  23772  dvmptntr  23779  dvcnvrelem2  23826  dvcnvre  23827  taylthlem1  24172  taylthlem2  24173  ulmdvlem3  24201  psercnlem2  24223  rlimcxp  24745  o1cxp  24746  structgrssvtxlemOLD  25960  sspg  27711  ssps  27713  sspn  27719  mdslj1i  29306  mdslj2i  29307  sh1dle  29338  shatomistici  29348  sumdmdii  29402  resf1o  29633  submarchi  29868  madjusmdetlem1  30021  txomap  30029  cnvordtrestixx  30087  dya2iocucvr  30474  carsggect  30508  bnj1241  31004  bnj906  31126  cvmscld  31381  nosupbnd2lem1  31986  noetalem4  31991  fvline2  32378  cldregopn  32451  poimirlem15  33554  sstotbnd2  33703  totbndbnd  33718  heibor1  33739  heiborlem8  33747  lsmsat  34613  lssats  34617  lkrpssN  34768  dia2dimlem5  36674  cdlemn2a  36802  dihglblem6  36946  dochocsp  36985  dochdmj1  36996  dochsatshpb  37058  lcfl9a  37111  lclkrlem2r  37130  lclkrlem2s  37131  lclkrlem2v  37134  lcfrlem6  37153  lcfrlem25  37173  lcfrlem35  37183  mapdval2N  37236  mapdin  37268  baerlem5alem2  37317  baerlem5blem2  37318  dnnumch2  37932  clrellem  38246  iunrelexpmin1  38317  iunrelexpmin2  38321  dftrcl3  38329  brtrclfv2  38336  dfrtrcl3  38342  mullimc  40166  islptre  40169  mullimcf  40173  limcmptdm  40185  dvresntr  40450  itgperiod  40515  fourierdlem89  40730  fourierdlem91  40732  iccpartgt  41688  resmgmhm2  42124  setrecsres  42773
  Copyright terms: Public domain W3C validator