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

Theorem eqsstr3d 3632
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 2626 . 2 (𝜑𝐴 = 𝐵)
3 eqsstr3d.2 . 2 (𝜑𝐵𝐶)
42, 3eqsstrd 3631 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1481  wss 3567
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-in 3574  df-ss 3581
This theorem is referenced by:  ssxpb  5556  fnsnb  6417  suppssof1  7313  oaword1  7617  omword2  7639  oeeui  7667  nnaword1  7694  cantnfle  8553  cantnflem1d  8570  r1val1  8634  rankr1id  8710  rankxplim3  8729  ackbij2  9050  ttukeylem7  9322  gruima  9609  hashdmpropge2  13248  rlimi  14225  rlimi2  14226  lo1bdd  14232  o1bdd  14243  rlimuni  14262  rlimcld2  14290  o1co  14298  rlimcn1  14300  rlimcn2  14302  o1add2  14335  o1mul2  14336  o1sub2  14337  lo1add  14338  lo1mul  14339  o1dif  14341  rlimneg  14358  rlimsqzlem  14360  lo1le  14363  rlimno1  14365  ramub1lem1  15711  imasaddfnlem  16169  imasvscafn  16178  mrcidb  16256  mrieqv2d  16280  mreexexlem4d  16288  funcres  16537  funcsetcres2  16724  acsfiindd  17158  tsrdir  17219  resmhm2  17341  f1omvdco2  17849  sylow2a  18015  sylow3lem6  18028  dprdspan  18407  dprd2dlem2  18420  dprd2dlem1  18421  dprd2da  18422  dmdprdsplit2lem  18425  dprdsplit  18428  dpjcntz  18432  ablfac1eu  18453  ringidss  18558  subrg1  18771  subrgdvds  18775  subrguss  18776  subrginv  18777  islss3  18940  lspsnneg  18987  lspextmo  19037  lspsnvs  19095  lsmcv  19122  islbs3  19136  drngdomn  19284  psrbaglesupp  19349  resspsrbas  19396  resspsradd  19397  resspsrmul  19398  evlseu  19497  f1lindf  20142  epttop  20794  neitr  20965  ordtbas  20977  ordtrest2  20989  pnfnei  21005  mnfnei  21006  ordtrestixx  21007  dnsconst  21163  cmpcld  21186  txindis  21418  txtube  21424  xkohaus  21437  xkopt  21439  xkococnlem  21443  xkoinjcn  21471  qtopval2  21480  ssufl  21703  ufldom  21747  cnextcn  21852  tmdgsum2  21881  clssubg  21893  clsnsg  21894  ustund  22006  ustneism  22008  trust  22014  fmucnd  22077  imasdsf1olem  22159  setsmstopn  22264  metequiv2  22296  metust  22344  restmetu  22356  tngtopn  22435  xlebnum  22745  pi1xfrcnv  22838  limcdif  23621  limccnp  23636  limccnp2  23637  limcco  23638  dvn2bss  23674  cpnord  23679  dvcmulf  23689  dvmptres2  23706  dvmptcmul  23708  dvmptntr  23715  dvcnvrelem2  23762  dvcnvre  23763  taylthlem1  24108  taylthlem2  24109  ulmdvlem3  24137  psercnlem2  24159  rlimcxp  24681  o1cxp  24682  structgrssvtxlemOLD  25896  sspg  27553  ssps  27555  sspn  27561  mdslj1i  29148  mdslj2i  29149  sh1dle  29180  shatomistici  29190  sumdmdii  29244  resf1o  29479  submarchi  29714  madjusmdetlem1  29867  txomap  29875  cnvordtrestixx  29933  dya2iocucvr  30320  carsggect  30354  bnj142OLD  30768  bnj1241  30852  bnj906  30974  cvmscld  31229  nosupbnd2lem1  31835  noetalem4  31840  fvline2  32228  cldregopn  32301  poimirlem15  33395  sstotbnd2  33544  totbndbnd  33559  heibor1  33580  heiborlem8  33588  lsmsat  34114  lssats  34118  lkrpssN  34269  dia2dimlem5  36176  cdlemn2a  36304  dihglblem6  36448  dochocsp  36487  dochdmj1  36498  dochsatshpb  36560  lcfl9a  36613  lclkrlem2r  36632  lclkrlem2s  36633  lclkrlem2v  36636  lcfrlem6  36655  lcfrlem25  36675  lcfrlem35  36685  mapdval2N  36738  mapdin  36770  baerlem5alem2  36819  baerlem5blem2  36820  dnnumch2  37434  clrellem  37748  iunrelexpmin1  37819  iunrelexpmin2  37823  dftrcl3  37831  brtrclfv2  37838  dfrtrcl3  37844  mullimc  39648  islptre  39651  mullimcf  39655  limcmptdm  39667  dvresntr  39895  itgperiod  39960  fourierdlem89  40175  fourierdlem91  40177  iccpartgt  41127  resmgmhm2  41564
  Copyright terms: Public domain W3C validator