MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  eqsstri Unicode version

Theorem eqsstri 3533
Description: Substitution of equality into a subclass relationship. (Contributed by NM, 16-Jul-1995.)
Hypotheses
Ref Expression
eqsstr.1
eqsstr.2
Assertion
Ref Expression
eqsstri

Proof of Theorem eqsstri
StepHypRef Expression
1 eqsstr.2 . 2
2 eqsstr.1 . . 3
32sseq1i 3527 . 2
41, 3mpbir 209 1
Colors of variables: wff setvar class
Syntax hints:  =wceq 1395  C_wss 3475
This theorem is referenced by:  eqsstr3i  3534  ssrab2  3584  rabssab  3586  opabss  4513  brab2ga  5080  relopabi  5133  dmopabss  5219  resss  5302  relres  5306  rnin  5420  rnxpss  5444  cnvcnvss  5466  dmmptss  5508  fnres  5702  f0  5771  nfvres  5901  fvopab4ndm  5978  ffvresb  6062  funiunfv  6160  isoini2  6235  ovssunirn  6325  dmoprabss  6384  mpt2ndm0  6516  elmpt2cl  6517  omsson  6704  exse2  6739  fabexg  6756  frxp  6910  tposssxp  6978  dftpos4  6993  smores  7042  smores2  7044  iordsmo  7047  oawordeulem  7222  swoer  7358  swoord1  7359  swoord2  7360  ecss  7372  ecopovsym  7432  ecopovtrn  7433  ecopover  7434  sbthlem7  7653  nnfi  7730  imafi  7833  elfiun  7910  marypha1lem  7913  marypha2lem1  7915  ordtypelem2  7965  hartogslem1  7988  wemapso2OLD  7998  wemapso2lem  7999  wdomima2g  8033  inf3lem1  8066  wemapwe  8160  wemapweOLD  8161  tc2  8194  tz9.12lem1  8226  rankuni  8302  rankuniss  8305  rankmapu  8317  cplem1  8328  hta  8336  r0weon  8411  infxpenlem  8412  ackbij1lem9  8629  ackbij1lem10  8630  ackbij1b  8640  cofsmo  8670  sdom2en01  8703  fin23lem26  8726  fin23lem28  8741  fin23lem30  8743  isf32lem5  8758  isf32lem6  8759  isf32lem7  8760  isf32lem8  8761  fin56  8794  fin1a2lem9  8809  hsmexlem4  8830  hsmexlem5  8831  hsmexlem6  8832  axdc3lem  8851  axdc3lem2  8852  axcclem  8858  zorn2lem1  8897  zorn2lem3  8899  zorn2lem4  8900  zorn2lem5  8901  imadomg  8933  iundom2g  8936  smobeth  8982  canth4  9046  gruina  9217  grur1a  9218  pinn  9277  niex  9280  ltsopi  9287  ltrelpi  9288  dmaddpi  9289  dmmulpi  9290  enqex  9321  0nnq  9323  elpqn  9324  ltrelnq  9325  nqerf  9329  nqerrel  9331  dmrecnq  9367  lterpq  9369  ltrelpr  9397  enrex  9465  ltrelsr  9466  dmaddsr  9483  dmmulsr  9484  ltrelre  9532  axaddf  9543  axmulf  9544  ltrelxr  9669  lerelxr  9671  nn0ssre  10824  nn0ssz  10910  uzsupss  11203  rpnnen1lem1  11237  rpnnen1lem2  11238  rpnnen1lem3  11239  rpnnen1lem5  11241  rpre  11255  uzsup  11990  fzfi  12082  swrd00  12645  sqrlem3  13078  sqrlem5  13080  cau3  13188  caubnd  13191  limsupgre  13304  rlimpm  13323  rlimclim  13369  isercolllem1  13487  isercolllem2  13488  isercoll  13490  caurcvg  13499  caucvg  13501  iseraltlem2  13505  iseraltlem3  13506  zsum  13540  fsumcvg3  13551  climfsum  13634  ackbijnn  13640  infcvgaux1i  13668  clim2prod  13697  ntrivcvg  13706  ntrivcvgfvn0  13708  ntrivcvgtail  13709  ntrivcvgmullem  13710  ntrivcvgmul  13711  zprod  13744  dvdszrcl  13991  divalglem2  14053  divalglem5  14055  divalglem8  14058  gcdcllem3  14151  bezoutlem2  14177  bezoutlem3  14178  maxprmfct  14254  phimullem  14309  eulerthlem2  14312  prmdiveq  14316  prmdivdiv  14317  pclem  14362  infpn2  14431  prmreclem2  14435  prmreclem3  14436  prmreclem5  14438  4sqlem1  14466  4sqlem13  14475  4sqlem14  14476  4sqlem17  14479  4sqlem18  14480  4sqlem19  14481  vdwnnlem3  14515  ramcl2lem  14527  ramtcl  14528  ramtcl2  14529  ramtub  14530  ramub1lem2  14545  structcnvcnv  14643  fvsetsid  14657  strlemor0  14723  strlemor1  14724  strleun  14727  imasdsval2  14913  gsumval1  15904  nmzsubg  16242  nmznsg  16245  conjnmz  16300  conjnmzb  16301  gicer  16324  gastacl  16347  symgbasfi  16411  mvdco  16470  symgsssg  16492  sylow1lem2  16619  sylow1lem3  16620  sylow1lem4  16621  sylow1lem5  16622  sylow2a  16639  sylow3lem2  16648  efglem  16734  efgtf  16740  efgtlen  16744  efginvrel2  16745  efginvrel1  16746  efgsfo  16757  efgredlemg  16760  efgredleme  16761  efgredlemd  16762  efgredlemc  16763  efgredlem  16765  efgred  16766  efgrelexlemb  16768  efgcpbllemb  16773  frgpinv  16782  frgpuplem  16790  frgpupf  16791  frgpup1  16793  frgpnabllem2  16878  gsumval3OLD  16908  gsumval3lem1  16909  gsumval3lem2  16910  gsumval3  16911  ablfacrplem  17116  ablfacrp2  17118  ablfac1eu  17124  pgpfaclem1  17132  ablfaclem2  17137  ablfaclem3  17138  lspsolvlem  17788  lbsextlem2  17805  lbsextlem3  17806  lbsextlem4  17807  rrgeq0  17938  rrgss  17941  psrbagconf1o  18026  psrass1lem  18029  mplbasss  18091  ply1bascl  18242  coe1mul2lem2  18309  znf1o  18590  zntoslem  18595  cygznlem2a  18606  psgnghm  18616  pjpm  18739  dsmmbase  18766  frlmsslsp  18829  frlmsslspOLD  18830  mretopd  19593  ordtbas  19693  leordtval2  19713  lecldbas  19720  lmfval  19733  lmbrf  19761  cnconst2  19784  hauscmplem  19906  concompcld  19935  hauspwdom  20002  txuni2  20066  xkouni  20100  xkoccn  20120  txkgen  20153  qtoptop2  20200  kqdisj  20233  hmphtop  20279  hmpher  20285  uzrest  20398  uzfbas  20399  lmflf  20506  ptcmplem1  20552  ptcmplem3  20554  tgpconcompeqg  20610  tgpconcomp  20611  ustn0  20723  imasdsf1olem  20876  xmeter  20936  blcld  21008  isngp2  21117  xrtgioo  21311  iccntr  21326  icccmplem1  21327  icccmplem2  21328  icccmplem3  21329  xmetdcn  21343  metdcn  21345  metdscn2  21361  icchmeo  21441  cnheiborlem  21454  lmmbrf  21701  iscau4  21718  iscauf  21719  caucfil  21722  lmclimf  21742  rrxf  21828  ivthlem1  21863  ivthlem2  21864  ivthlem3  21865  ovolsslem  21895  ovolicc2lem3  21930  ovolicc2lem4  21931  ovolicc2lem5  21932  ovolicc2  21933  volf  21940  uniioombllem3  21994  uniioombllem4  21995  uniioombllem5  21996  dyadmbllem  22008  dyadmbl  22009  volcn  22015  mbfimaopnlem  22062  mbflimsup  22073  i1f1  22097  itg2lcl  22134  iblmbf  22174  itgioo  22222  itgsplitioo  22244  limcflflem  22284  limcflf  22285  limcresi  22289  lhop  22417  dvfsumlem1  22427  dvfsumlem2  22428  dvfsumlem3  22429  dvfsumlem4  22430  dvfsumrlimge0  22431  dvfsumrlim  22432  dvfsumrlim2  22433  dvfsum2  22435  vieta1lem1  22706  vieta1lem2  22707  psercnlem2  22819  psercnlem1  22820  psercn  22821  pserdvlem1  22822  pserdvlem2  22823  pserdv  22824  pserdv2  22825  abelthlem4  22829  abelthlem6  22831  abelthlem9  22835  abelth  22836  logcnlem5  23027  dvlog  23032  dvlog2lem  23033  dvlog2  23034  cxpcn3lem  23121  cxpcn3  23122  sqrtcn  23124  1cubr  23173  atansssdm  23264  atancn  23267  jensen  23318  wilthlem1  23342  ftalem3  23348  dvdsflip  23458  musum  23467  dvdsmulf1o  23470  fsumdvdsmul  23471  ppiub  23479  lgsfcl2  23577  lgsquadlem1  23629  lgsquadlem2  23630  lgsquadlem3  23631  2sqlem7  23645  rpvmasum2  23697  dchrisum0re  23698  dchrisum0lema  23699  dchrisum0lem1b  23700  dchrisum0lem1  23701  dchrisum0lem2a  23702  dchrisum0lem2  23703  dchrisum0lem3  23704  dchrisum0  23705  pntlem3  23794  axtgcgrrflx  23859  axtgcgrid  23860  axtgsegcon  23861  axtg5seg  23862  axtgbtwnid  23863  axtgpasch  23864  axtgcont1  23865  tglng  23933  axcontlem2  24268  axcontlem7  24273  axcontlem8  24274  axcontlem10  24276  nbgraf1olem1  24441  disjxwwlkn  24745  clwlknclwlkdifnum  24961  frgrawopreg1  25050  frgrawopreg2  25051  issubgoi  25312  flddivrng  25417  phnv  25729  htthlem  25834  hlimadd  26110  hlimcaui  26154  hhsscms  26195  occllem  26221  shjshsi  26410  3oalem4  26583  pjfi  26622  dmadjss  26806  nlelshi  26979  nlelchi  26980  hmopidmchi  27070  atssch  27262  shatomistici  27280  fcoinver  27460  mptctf  27544  fcobijfs  27549  cnre2csqima  27893  raddcn  27911  rrhre  27999  esumsn  28072  sxbrsiga  28261  oddpwdc  28293  eulerpartlem1  28306  eulerpartlemt  28310  eulerpartgbij  28311  eulerpartlemmf  28314  eulerpartlemgvv  28315  eulerpartlemgh  28317  sseqf  28331  ballotlemfmpn  28433  ballotth  28476  signswch  28518  lgamucov  28580  lgamucov2  28581  subfacp1lem3  28626  subfacp1lem5  28628  erdszelem2  28636  kur14lem3  28652  kur14lem6  28655  kur14lem7  28656  kur14lem9  28658  cvmlift2lem12  28759  mpstssv  28899  mstapst  28907  mppspstlem  28931  mppspst  28934  mthmsta  28938  mthmpps  28942  mclsppslem  28943  ghomgrpilem2  29026  divcnvshft  29117  dfpo2  29184  predss  29251  wfrlem7  29349  wlimss  29385  frrlem7  29397  txpss3v  29528  pprodss4v  29534  relsset  29538  fixssdm  29556  fixssrn  29557  limitssson  29561  funpartss  29594  colinearex  29710  dvcncxp1  30100  dvcnsqrt  30101  dvasin  30103  dvacos  30104  areacirc  30112  fneer  30171  neibastop1  30177  neibastop2lem  30178  filnetlem2  30197  filnetlem3  30198  caures  30253  bnd2lem  30287  ismtyres  30304  eldiophb  30690  monotuz  30877  fglmod  31019  pwssplit4  31035  pwfi2f1o  31044  arearect  31183  uzmptshftfval  31251  binomcxplemdvbinom  31258  binomcxplemdvsum  31260  binomcxplemnotnn0  31261  rabexgf  31399  fz1ssfz0  31510  limcperiod  31634  sumnnodd  31636  cncfshift  31676  cncfperiod  31681  ibliooicc  31770  stoweidlem26  31808  stoweidlem44  31826  stoweidlem50  31832  stoweidlem51  31833  stoweidlem52  31834  stoweidlem57  31839  stoweidlem59  31841  fourierdlem16  31905  fourierdlem19  31908  fourierdlem21  31910  fourierdlem22  31911  fourierdlem42  31931  fourierdlem83  31972  fouriersw  32014  oddibas  32501  2zlidl  32740  2zrngbas  32742  2zrng0  32744  fldc  32891  fldhmsubc  32892  fldcOLD  32910  fldhmsubcOLD  32911  bnj21  33770  bnj1146  33850  bnj1292  33874  bnj1293  33875  bnj1145  34049  bnj1177  34062  bj-tagss  34538  bj-cmnssmnd  34652  bj-ablssgrp  34654  bj-ablsscmn  34656  bj-vecssmod  34659  bj-rrvecssvec  34666  toycom  34698  dihglblem2N  37021  lcdvbase  37320  mapdunirnN  37377  rp-imass  37795  xphe  37804  0he  37805
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-in 3482  df-ss 3489
  Copyright terms: Public domain W3C validator