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

Theorem eqbrtrrd 4324
Description: Substitution of equal classes into a binary relation. (Contributed by NM, 24-Oct-1999.)
Hypotheses
Ref Expression
eqbrtrrd.1
eqbrtrrd.2
Assertion
Ref Expression
eqbrtrrd

Proof of Theorem eqbrtrrd
StepHypRef Expression
1 eqbrtrrd.1 . . 3
21eqcomd 2486 . 2
3 eqbrtrrd.2 . 2
42, 3eqbrtrd 4322 1
Colors of variables: wff set class
Syntax hints:  ->wi 4  =wceq 1662   class class class wbr 4302
This theorem is referenced by:  dftpos4  6681  fodomfi  7497  cnfcom2lem  7770  infcda1  8187  enfin1ai  8378  fin56  8387  pwcfsdom  8572  fpwwe2lem7  8625  fpwwe2  8632  canthp1lem1  8641  1nqenq  8953  prlem936  9038  lemulge11  10003  supmul1  10104  xaddge0  11028  xadddi2  11067  ltexp2a  11707  leexp2a  11711  nnlesq  11761  digit1  11790  faclbnd4lem1  11861  faclbnd6  11867  facavg  11869  abs3dif  12605  abs2dif  12606  limsupgre  12745  rlimclim1  12809  rlimuni  12814  rlimres2  12825  rlimcn1  12852  rlimcn1b  12853  recn2  12864  imcn2  12865  rlimo1  12880  o1rlimmul  12882  iserex  12920  isercoll  12931  caucvgrlem2  12938  caucvgr  12939  iseraltlem3  12947  summolem2a  12979  fsumge1  13046  o1fsum  13062  isumrpcl  13092  climcnds  13100  harmonic  13107  mertenslem1  13130  ege2le3  13161  efgt1p2  13184  efgt1p  13185  eirrlem  13272  rpnnen2lem11  13293  fsumdvds  13362  bitsfzo  13417  bitsmod  13418  bitscmp  13420  mulgcd  13516  dvdssqlem  13529  nn0seqcvgd  13531  mulgcddvds  13576  rpdvds  13596  qden1elz  13621  phimullem  13640  pcdvdstr  13728  pockthg  13753  prmreclem1  13763  4sqlem11  13802  ramub1lem1  13873  ramub1lem2  13874  mreexexlem4d  14363  sscid  14515  latmlej21  15040  latmlej22  15041  lubel  15070  efginvrel1  15863  odadd2  15967  odadd  15968  gexexlem  15970  cyggex2  16009  ablfacrplem  16126  ablfac1c  16132  ablfac1eu  16134  pgpfac1lem3a  16137  isabvd  16411  znrrg  17349  lmcn2  18185  metrtri  18891  imasdsf1olem  18907  stdbdxmet  19049  nrmmetd  19126  nmmtri  19172  nlmvscnlem2  19225  blcvx  19333  recld2  19349  zdis  19351  opnreen  19366  cnheibor  19484  lebnumlem3  19492  nmoleub2lem3  19627  nmoleub2lem2  19628  nmoleub3  19631  ipcnlem2  19702  cmetcaulem  19745  cncmet  19779  minveclem4  19837  ovoliunlem1  19902  ovoliun2  19906  ovolscalem1  19913  ovolicopnf  19924  voliunlem2  19949  volsup  19954  ioorcl2  19968  uniiccvol  19976  uniioombllem4  19982  i1fd  20075  mbfi1fseqlem4  20112  itg2const2  20135  itg2eqa  20139  itg2split  20143  itg2i1fseqle  20148  itg2cnlem2  20156  dvcnv  20365  dveflem  20367  dvferm1lem  20372  dvlip2  20383  c1liplem1  20384  dvivthlem1  20396  lhop1lem  20401  dvcvx  20408  dvfsumle  20409  dvfsumabs  20411  dvfsumlem4  20417  dvfsumrlim2  20420  ftc1a  20425  deg1pwle  20546  fta1blem  20595  aalioulem3  20755  aaliou2b  20762  ulmbdd  20818  ulmdvlem1  20820  itgulm  20828  pserdvlem2  20848  abelthlem3  20853  abelthlem5  20855  abelthlem6  20856  abelthlem7  20858  tanregt0  20950  argimlt0  21017  logdivlti  21024  logcnlem3  21044  logcnlem4  21045  logtayl  21060  logtayl2  21062  cxple2  21097  cxpcn3lem  21140  cxpaddle  21145  isosctrlem1  21171  atantayl  21286  efrlim  21317  dfef2  21318  o1cxp  21322  cxp2lim  21324  divsqrsumo1  21331  amgmlem  21337  logdifbnd  21341  emcllem7  21349  harmonicbnd4  21358  fsumharmonic  21359  ftalem2  21365  basellem2  21373  basellem5  21376  basellem9  21380  vma1  21458  sqff1o  21474  fsumfldivdiaglem  21483  chtub  21505  fsumvma2  21507  chpchtsum  21512  chpub  21513  logfaclbnd  21515  logfacbnd3  21516  logfacrlim  21517  logexprlim  21518  bcmono  21570  bposlem2  21578  bposlem5  21581  bposlem6  21582  lgsne0  21626  lgsquadlem1  21647  lgsquadlem2  21648  2sqblem  21670  chebbnd1lem1  21672  chtppilimlem1  21676  chtppilimlem2  21677  chpchtlim  21682  rplogsumlem1  21687  dchrvmasumiflem1  21704  dchrisum0flblem2  21712  dchrisum0fno1  21714  dchrisum0re  21716  dchrisum0lem2a  21720  dchrisum0lem3  21722  dirith  21732  mulog2sumlem1  21737  mulog2sumlem2  21738  log2sumbnd  21747  selberglem2  21749  logdivbnd  21759  selberg3lem1  21760  selberg4lem1  21763  pntrsumbnd2  21770  pntrlog2bndlem1  21780  pntrlog2bndlem5  21784  pntrlog2bndlem6  21786  pntpbnd1a  21788  pntpbnd1  21789  pntpbnd2  21790  pntibndlem3  21795  pntlemb  21800  pntlemn  21803  pntlemr  21805  pntlemj  21806  pntlemf  21808  pntlemo  21810  ostth2lem3  21838  ostth3  21841  nvabs  22671  nvlmle  22697  smcnlem  22702  ubthlem2  22882  minvecolem4  22891  htthlem  22929  normpyc  23158  nmophmi  24045  hstle  24244  hstles  24245  stlei  24254  mul2lt0llt0  24661  mul2lt0lgt0  24662  xrge0npcan  24780  archirngz  24829  archiabllem1a  24831  archiabllem2a  24834  archiabllem2c  24835  ornglmulle  24925  orngrmulle  24926  esumpinfval  25193  esumpinfsum  25197  esumpcvgval  25198  dya2icoseg  25363  eulerpartlems  25408  sgnmulsgn  25573  signsply0  25594  lgamgulmlem2  25653  lgamgulmlem3  25654  lgamucov  25661  lgamcvg2  25678  gamcvg2  25683  rescon  25772  sinccvglem  25948  circum  25950  prodmolem2a  26090  btwnxfr  26820  supaddc  27089  mblfinlem3  27101  mblfinlem4  27102  dvtanlem  27112  itg2addnclem3  27116  ftc1anc  27146  nn0prpwlem  27188  csbren  27319  trirn  27320  isbnd3  27356  cntotbnd  27368  bfp  27396  rrndstprj2  27403  irrapxlem1  27814  irrapxlem4  27817  pell1qrgaplem  27865  pellfundglb  27877  rmspecfund  27901  monotoddzzfi  27934  rmynn  27950  jm2.24nn  27953  jm2.17c  27956  jm2.24  27957  acongeq  27977  jm2.20nn  27997  jm2.26lem3  28001  jm2.27a  28005  jm2.27c  28007  rmydioph  28014  jm3.1lem2  28018  frlmpwfi  28168  f1linds  28201  hashgcdlem  28422  hashgcdeq  28423  cncmpmax  28604  fmul01lt1lem2  28616  clim1fr1  28627  stoweidlem1  28650  stoweidlem11  28660  stoweidlem14  28663  stoweidlem24  28673  stoweidlem26  28675  wallispilem4  28717  wallispilem5  28718  stirlinglem1  28723  2leaddle2  29032  isosctrlem1ALT  30239  1cvrjat  31545  3atlem1  31553  3atlem6  31558  llnmlplnN  31609  2llnjaN  31636  2lplnja  31689  dalem57  31799  dalawlem11  31951  dalawlem12  31952  lhp2lt  32071  lhpj1  32092  lhpm0atN  32099  4atexlemex2  32141  lautm  32164  cdleme17b  32357  cdleme20j  32388  cdleme30a  32448  cdlemg4c  32682  cdlemg17a  32731  cdlemg31c  32769  trljco  32810  cdlemk46  33018  dia2dimlem2  33136  cdlemm10N  33189  cdlemn10  33277  dihmeetlem1N  33361  dihglblem5apreN  33362  dihmeetlem15N  33392  mapdat  33738
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1562  ax-4 1573  ax-5 1636  ax-6 1677  ax-7 1697  ax-10 1743  ax-11 1748  ax-12 1760  ax-13 1947  ax-ext 2462
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 941  df-tru 1337  df-ex 1558  df-nf 1561  df-sb 1669  df-clab 2468  df-cleq 2474  df-clel 2477  df-nfc 2606  df-rab 2760  df-v 3008  df-dif 3356  df-un 3358  df-in 3360  df-ss 3367  df-nul 3661  df-if 3813  df-sn 3900  df-pr 3901  df-op 3903  df-br 4303
  Copyright terms: Public domain W3C validator