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

Theorem eqbrtrrd 4265
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 2448 . 2
3 eqbrtrrd.2 . 2
42, 3eqbrtrd 4263 1
Colors of variables: wff set class
Syntax hints:  ->wi 4  =wceq 1654   class class class wbr 4243
This theorem is referenced by:  dftpos4  6548  fodomfi  7434  cnfcom2lem  7707  infcda1  8124  enfin1ai  8315  fin56  8324  pwcfsdom  8509  fpwwe2lem7  8562  fpwwe2  8569  canthp1lem1  8578  1nqenq  8890  prlem936  8975  lemulge11  9923  supmul1  10024  xaddge0  10888  xadddi2  10927  ltexp2a  11482  leexp2a  11486  nnlesq  11535  digit1  11564  faclbnd4lem1  11635  faclbnd6  11641  facavg  11643  abs3dif  12186  abs2dif  12187  limsupgre  12326  rlimclim1  12390  rlimuni  12395  rlimres2  12406  rlimcn1  12433  rlimcn1b  12434  recn2  12445  imcn2  12446  rlimo1  12461  o1rlimmul  12463  iserex  12501  isercoll  12512  caucvgrlem2  12519  caucvgr  12520  iseraltlem3  12528  summolem2a  12560  fsumge1  12627  o1fsum  12643  isumrpcl  12674  climcnds  12682  harmonic  12689  mertenslem1  12712  ege2le3  12743  efgt1p2  12766  efgt1p  12767  eirrlem  12854  rpnnen2lem11  12875  fsumdvds  12944  bitsfzo  12998  bitsmod  12999  bitscmp  13001  mulgcd  13097  dvdssqlem  13110  nn0seqcvgd  13112  mulgcddvds  13155  rpdvds  13175  qden1elz  13200  phimullem  13219  pcdvdstr  13300  pockthg  13325  prmreclem1  13335  4sqlem11  13374  ramub1lem1  13445  ramub1lem2  13446  mreexexlem4d  13923  sscid  14075  latmlej21  14572  latmlej22  14573  lubel  14600  efginvrel1  15411  odadd2  15515  odadd  15516  gexexlem  15518  cyggex2  15557  ablfacrplem  15674  ablfac1c  15680  ablfac1eu  15682  pgpfac1lem3a  15685  isabvd  15959  znrrg  16897  lmcn2  17732  metrtri  18438  imasdsf1olem  18454  stdbdxmet  18596  nrmmetd  18673  nmmtri  18719  nlmvscnlem2  18772  blcvx  18880  recld2  18896  zdis  18898  opnreen  18913  cnheibor  19031  lebnumlem3  19039  nmoleub2lem3  19174  nmoleub2lem2  19175  nmoleub3  19178  ipcnlem2  19249  cmetcaulem  19292  cncmet  19326  minveclem4  19384  ovoliunlem1  19449  ovoliun2  19453  ovolscalem1  19460  ovolicopnf  19471  voliunlem2  19496  volsup  19501  ioorcl2  19515  uniiccvol  19523  uniioombllem4  19529  i1fd  19622  mbfi1fseqlem4  19659  itg2const2  19682  itg2eqa  19686  itg2split  19690  itg2i1fseqle  19695  itg2cnlem2  19703  dvcnv  19912  dveflem  19914  dvferm1lem  19919  dvlip2  19930  c1liplem1  19931  dvivthlem1  19943  lhop1lem  19948  dvcvx  19955  dvfsumle  19956  dvfsumabs  19958  dvfsumlem4  19964  dvfsumrlim2  19967  ftc1a  19972  deg1pwle  20093  fta1blem  20142  aalioulem3  20302  aaliou2b  20309  ulmbdd  20365  ulmdvlem1  20367  itgulm  20375  pserdvlem2  20395  abelthlem3  20400  abelthlem5  20402  abelthlem6  20403  abelthlem7  20405  tanregt0  20492  argimlt0  20559  logdivlti  20566  logcnlem3  20586  logcnlem4  20587  logtayl  20602  logtayl2  20604  cxple2  20639  cxpcn3lem  20682  cxpaddle  20687  isosctrlem1  20713  atantayl  20828  efrlim  20859  dfef2  20860  o1cxp  20864  cxp2lim  20866  divsqrsumo1  20873  amgmlem  20879  logdifbnd  20883  emcllem7  20891  harmonicbnd4  20900  fsumharmonic  20901  ftalem2  20907  basellem2  20915  basellem5  20918  basellem9  20922  vma1  21000  sqff1o  21016  fsumfldivdiaglem  21025  chtub  21047  fsumvma2  21049  chpchtsum  21054  chpub  21055  logfaclbnd  21057  logfacbnd3  21058  logfacrlim  21059  logexprlim  21060  bcmono  21112  bposlem2  21120  bposlem5  21123  bposlem6  21124  lgsne0  21168  lgsquadlem1  21189  lgsquadlem2  21190  2sqblem  21212  chebbnd1lem1  21214  chtppilimlem1  21218  chtppilimlem2  21219  chpchtlim  21224  rplogsumlem1  21229  dchrvmasumiflem1  21246  dchrisum0flblem2  21254  dchrisum0fno1  21256  dchrisum0re  21258  dchrisum0lem2a  21262  dchrisum0lem3  21264  dirith  21274  mulog2sumlem1  21279  mulog2sumlem2  21280  log2sumbnd  21289  selberglem2  21291  logdivbnd  21301  selberg3lem1  21302  selberg4lem1  21305  pntrsumbnd2  21312  pntrlog2bndlem1  21322  pntrlog2bndlem5  21326  pntrlog2bndlem6  21328  pntpbnd1a  21330  pntpbnd1  21331  pntpbnd2  21332  pntibndlem3  21337  pntlemb  21342  pntlemn  21345  pntlemr  21347  pntlemj  21348  pntlemf  21350  pntlemo  21352  ostth2lem3  21380  ostth3  21383  nvabs  22213  nvlmle  22239  smcnlem  22244  ubthlem2  22424  minvecolem4  22433  htthlem  22471  normpyc  22699  nmophmi  23585  hstle  23784  hstles  23785  stlei  23794  xrge0npcan  24265  esumpinfval  24512  esumpinfsum  24516  esumpcvgval  24517  dya2icoseg  24676  eulerpartlems  24746  lgamgulmlem2  24918  lgamgulmlem3  24919  lgamucov  24926  lgamcvg2  24943  gamcvg2  24948  rescon  25037  sinccvglem  25213  circum  25215  prodmolem2a  25364  btwnxfr  26094  supaddc  26342  mblfinlem3  26354  mblfinlem4  26355  dvtanlem  26365  itg2addnclem3  26369  ftc1anc  26399  nn0prpwlem  26436  csbren  26567  trirn  26568  isbnd3  26604  cntotbnd  26616  bfp  26644  rrndstprj2  26651  irrapxlem1  27064  irrapxlem4  27067  pell1qrgaplem  27115  pellfundglb  27127  rmspecfund  27151  monotoddzzfi  27184  rmynn  27200  jm2.24nn  27203  jm2.17c  27206  jm2.24  27207  acongeq  27227  jm2.20nn  27247  jm2.26lem3  27251  jm2.27a  27255  jm2.27c  27257  rmydioph  27264  jm3.1lem2  27268  frlmpwfi  27418  f1linds  27451  hashgcdlem  27672  hashgcdeq  27673  cncmpmax  27857  fmul01lt1lem2  27869  clim1fr1  27881  stoweidlem1  27904  stoweidlem11  27914  stoweidlem14  27917  stoweidlem24  27927  stoweidlem26  27929  wallispilem4  27971  wallispilem5  27972  stirlinglem1  27977  2leaddle2  28279  isosctrlem1ALT  29287  1cvrjat  30512  3atlem1  30520  3atlem6  30525  llnmlplnN  30576  2llnjaN  30603  2lplnja  30656  dalem57  30766  dalawlem11  30918  dalawlem12  30919  lhp2lt  31038  lhpj1  31059  lhpm0atN  31066  4atexlemex2  31108  lautm  31131  cdleme17b  31324  cdleme20j  31355  cdleme30a  31415  cdlemg4c  31649  cdlemg17a  31698  cdlemg31c  31736  trljco  31777  cdlemk46  31985  dia2dimlem2  32103  cdlemm10N  32156  cdlemn10  32244  dihmeetlem1N  32328  dihglblem5apreN  32329  dihmeetlem15N  32359  mapdat  32705
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1628  ax-9 1669  ax-8 1690  ax-6 1747  ax-7 1752  ax-11 1764  ax-12 1954  ax-ext 2424
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1661  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-rab 2721  df-v 2967  df-dif 3312  df-un 3314  df-in 3316  df-ss 3323  df-nul 3617  df-if 3766  df-sn 3847  df-pr 3848  df-op 3850  df-br 4244
  Copyright terms: Public domain W3C validator