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

Theorem 3brtr4d 4482
Description: Substitution of equality into both sides of a binary relation. (Contributed by NM, 21-Feb-2005.)
Hypotheses
Ref Expression
3brtr4d.1
3brtr4d.2
3brtr4d.3
Assertion
Ref Expression
3brtr4d

Proof of Theorem 3brtr4d
StepHypRef Expression
1 3brtr4d.1 . 2
2 3brtr4d.2 . . 3
3 3brtr4d.3 . . 3
42, 3breq12d 4465 . 2
51, 4mpbird 232 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  =wceq 1395   class class class wbr 4452
This theorem is referenced by:  f1oiso2  6248  sucdom2  7734  ordtypelem6  7969  cdaen  8574  cdacomen  8582  cdadom1  8587  fin23lem26  8726  distrnq  9360  lediv12a  10463  recp1lt1  10468  ifle  11425  xleadd1a  11474  xlemul1a  11509  quoremz  11982  quoremnn0ALT  11984  intfracq  11986  modmulnn  12013  fzennn  12078  monoord2  12138  expgt1  12204  leexp2r  12223  leexp1a  12224  bernneq  12292  expmulnbnd  12298  digit1  12300  faclbnd  12368  faclbnd4lem3  12373  faclbnd4lem4  12374  faclbnd6  12377  facubnd  12378  hashdomi  12448  fzsdom2  12486  absrele  13141  absimle  13142  abstri  13163  abs2difabs  13167  limsupval2  13303  rlimrege0  13402  rlimrecl  13403  climsqz  13463  climsqz2  13464  rlimdiv  13468  rlimsqz  13472  rlimsqz2  13473  isercolllem1  13487  isercoll2  13491  fsumcvg2  13549  fsumrlim  13625  o1fsum  13627  cvgcmpce  13632  isumle  13656  climcndslem1  13661  climcndslem2  13662  harmonic  13670  expcnv  13675  explecnv  13676  geomulcvg  13685  efcllem  13813  ege2le3  13825  eflegeo  13856  rpnnen2lem4  13951  ruclem2  13965  ruclem8  13970  fsumdvds  14029  phibnd  14301  iserodd  14359  pcdvdstr  14399  pcprmpw2  14405  pockthg  14424  prmreclem4  14437  2expltfac  14577  mod2ile  15736  odsubdvds  16591  pgpfi  16625  fislw  16645  efgredlemd  16762  efgredlem  16765  frgpcpbl  16777  abvres  17488  abvtrivd  17489  znrrg  18604  cstucnd  20787  psmetge0  20816  psmetres2  20818  xmetge0  20847  xmetres2  20864  imasf1oxmet  20878  comet  21016  stdbdxmet  21018  dscmet  21093  nrmmetd  21095  nmrtri  21143  tngngp  21168  nmolb2d  21225  nmoleub  21238  nmoco  21244  nmotri  21246  nmoid  21249  nmods  21251  cnmet  21279  xrsxmet  21314  metdstri  21355  metnrmlem3  21365  lebnumlem3  21463  ipcau2  21677  tchcphlem1  21678  tchcph  21680  trirn  21827  rrxmet  21835  rrxdstprj1  21836  minveclem2  21841  ovolunlem1a  21907  ovolscalem1  21924  volss  21944  voliunlem1  21960  volcn  22015  itg1climres  22121  mbfi1fseqlem5  22126  mbfi1fseqlem6  22127  itg2const2  22148  itg2seq  22149  itg2mulc  22154  itg2splitlem  22155  itg2monolem1  22157  itg2i1fseqle  22161  itg2i1fseq  22162  itg2i1fseq2  22163  itg2addlem  22165  itg2cnlem1  22168  itg2cnlem2  22169  iblss  22211  itgle  22216  ibladdlem  22226  iblabs  22235  iblabsr  22236  iblmulc2  22237  itgabs  22241  bddmulibl  22245  dvfsumabs  22424  dvfsumlem2  22428  dvfsum2  22435  deg1suble  22508  deg1mul3le  22517  plyeq0lem  22607  dgrcolem2  22671  geolim3  22735  aaliou3lem2  22739  aaliou3lem8  22741  ulmdvlem1  22795  radcnvlem1  22808  radcnvlem2  22809  dvradcnv  22816  pserulm  22817  pserdvlem2  22823  abelthlem2  22827  abelthlem5  22830  abelthlem7  22833  abelth2  22837  tangtx  22898  tanabsge  22899  tanord1  22924  argregt0  22995  argrege0  22996  argimgt0  22997  abslogle  23003  logcnlem4  23026  logtayllem  23040  abscxpbnd  23127  ang180lem2  23142  atanlogsublem  23246  atans2  23262  leibpi  23273  birthdaylem3  23283  cxplim  23301  cxp2limlem  23305  cxploglim2  23308  jensenlem2  23317  jensen  23318  amgmlem  23319  emcllem2  23326  emcllem4  23328  emcllem7  23331  ftalem5  23350  basellem4  23357  basellem6  23359  basellem8  23361  basellem9  23362  chtwordi  23430  chpwordi  23431  ppiwordi  23436  ppiub  23479  vmalelog  23480  chtlepsi  23481  chtleppi  23485  chtublem  23486  chtub  23487  chpub  23495  logfaclbnd  23497  logfacrlim  23499  dchrptlem3  23541  bcmono  23552  bclbnd  23555  bposlem1  23559  bposlem6  23564  bposlem9  23567  lgsqrlem4  23619  chebbnd1lem1  23654  chebbnd1lem3  23656  chebbnd1  23657  chtppilimlem1  23658  vmadivsum  23667  rplogsumlem2  23670  dchrisumlema  23673  dchrisumlem3  23676  dchrmusum2  23679  dchrvmasumlem3  23684  dchrvmasumiflem1  23686  dchrisum0flblem1  23693  dchrisum0re  23698  dchrisum0lem2a  23702  mulogsumlem  23716  mulog2sumlem1  23719  mulog2sumlem2  23720  2vmadivsumlem  23725  selberg2lem  23735  selberg3lem1  23742  selberg4lem1  23745  pntrlog2bndlem3  23764  pntrlog2bndlem5  23766  pntrlog2bndlem6  23768  pntpbnd1  23771  pntlemc  23780  pntlemr  23787  pntlemk  23791  pntlemo  23792  abvcxp  23800  ostth2lem1  23803  padicabv  23815  ostth2lem2  23819  ostth2lem3  23820  ostth2lem4  23821  ostth2  23822  legso  23985  nvmtri  25574  imsmetlem  25596  vacn  25604  nmcvcn  25605  smcnlem  25607  blometi  25718  ipblnfi  25771  minvecolem2  25791  hhssnv  26180  nmcoplbi  26947  nmopcoi  27014  nmopcoadji  27020  idleop  27050  cdj1i  27352  isoun  27520  xlt2addrd  27578  omndmul  27704  ogrpsub  27707  archirngz  27733  gsumle  27770  ofldchr  27804  pstmxmet  27876  nexple  28005  esumpmono  28085  esumcvg  28092  meascnbl  28190  omsmon  28267  dstfrvinc  28415  zetacvg  28557  lgamgulmlem2  28572  lgamgulmlem5  28575  lgamcvg2  28597  derangenlem  28615  subfaclefac  28620  subfaclim  28632  erdszelem10  28644  sinccvglem  29038  iprodefisum  29124  itg2gt0cn  30070  ibladdnclem  30071  iblabsnc  30079  iblmulc2nc  30080  itgabsnc  30084  bddiblnc  30085  ftc1anclem7  30096  ftc1anclem8  30097  ftc1anc  30098  mettrifi  30250  equivbnd2  30288  heiborlem6  30312  bfplem1  30318  bfp  30320  rrnmet  30325  rrndstprj1  30326  rrndstprj2  30327  irrapxlem5  30762  pell1qrge1  30806  pell1qrgaplem  30809  pell14qrgapw  30812  pellqrex  30815  pellfund14  30834  expmordi  30883  jm2.17a  30898  jm2.17c  30900  acongeq  30921  jm2.19  30935  jm2.27a  30947  jm2.27c  30949  jm3.1lem2  30960  areaquad  31184  hashnzfzclim  31227  binomcxplemnotnn0  31261  ltmod  31644  dvbdfbdioolem2  31726  ioodvbdlimc1lem2  31729  ioodvbdlimc2lem  31731  stoweidlem3  31785  stoweidlem26  31808  wallispilem1  31847  wallispilem5  31851  stirlinglem1  31856  stirlinglem5  31860  stirlinglem8  31863  stirlinglem10  31865  stirlinglem12  31867  fourierdlem6  31895  fourierdlem7  31896  fourierdlem14  31903  fourierdlem19  31908  fourierdlem35  31924  fourierdlem39  31928  fourierdlem42  31931  fourierdlem50  31939  fourierdlem73  31962  fourierdlem76  31965  fourierdlem77  31966  fourierdlem81  31970  fourierdlem90  31979  fourierdlem92  31981  fourierdlem93  31982  fourierdlem111  32000  fouriersw  32014  etransclem38  32055  rnghmsubcsetc  32785  rhmsubcsetc  32831  rhmsubcrngc  32837  rhmsubc  32898  rhmsubcOLD  32917  dalawlem3  35597  dalawlem4  35598  dalawlem6  35600  dalawlem9  35603  dalawlem11  35605  dalawlem12  35606  dalawlem15  35609  cdleme3c  35955  cdleme7e  35972  cdleme26e  36085  cdleme26eALTN  36087  cdleme27a  36093  cdleme32c  36169  cdleme32e  36171  cdleme32le  36173  cdlemg9b  36359  cdlemg12b  36370  cdlemg12d  36372  trlcolem  36452  trlcone  36454  cdlemk7  36574  cdlemk7u  36596  cdlemk39  36642  cdlemk11ta  36655  cdlemk11tc  36671  mapdcnvatN  37393  rp-isfinite6  37744
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-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-rab 2816  df-v 3111  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-br 4453
  Copyright terms: Public domain W3C validator