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

Theorem breqtrrd 4713
Description: Substitution of equal classes into a binary relation. (Contributed by NM, 24-Oct-1999.)
Hypotheses
Ref Expression
breqtrrd.1 (𝜑𝐴𝑅𝐵)
breqtrrd.2 (𝜑𝐶 = 𝐵)
Assertion
Ref Expression
breqtrrd (𝜑𝐴𝑅𝐶)

Proof of Theorem breqtrrd
StepHypRef Expression
1 breqtrrd.1 . 2 (𝜑𝐴𝑅𝐵)
2 breqtrrd.2 . . 3 (𝜑𝐶 = 𝐵)
32eqcomd 2657 . 2 (𝜑𝐵 = 𝐶)
41, 3breqtrd 4711 1 (𝜑𝐴𝑅𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1523   class class class wbr 4685
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-rab 2950  df-v 3233  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-br 4686
This theorem is referenced by:  marypha1lem  8380  marypha2  8386  unxpwdom  8535  uncdadom  9031  cdacomen  9041  cdaassen  9042  xpcdaen  9043  onacda  9057  infcdaabs  9066  cfss  9125  tskuni  9643  ltexnq  9835  lt2addmuld  11320  div4p1lem1div2  11325  mul2lt0rgt0  11971  xrmax1  12044  xrmax2  12045  max1ALT  12055  qbtwnxr  12069  xleadd1a  12121  xlt2add  12128  xlesubadd  12131  xmulgt0  12151  xlemul1a  12156  xov1plusxeqvd  12356  uzsubsubfz  12401  fzctr  12490  subfzo0  12630  flflp1  12648  fldiv4lem1div2uz2  12677  ceilge  12685  modge0  12718  modlt  12719  modid  12735  m1modge3gt1  12757  modaddmodup  12773  sermono  12873  seqf1olem1  12880  seqf1olem2  12881  leexp1a  12959  sqgt0  12972  sqge0  12980  nnlesq  13008  expnbnd  13033  expmulnbnd  13036  discr1  13040  facwordi  13116  faclbnd5  13125  nfile  13188  hashdom  13206  fi1uzind  13317  brfi1indALT  13320  ccatws1n0  13453  ccatws1n0OLD  13454  swrds2  13731  cjmulge0  13930  resqrtcl  14038  absge0  14071  sqreulem  14143  amgm2  14153  rlimdm  14326  rlimge0  14356  reccn2  14371  climle  14414  climserle  14437  isercoll2  14443  iseraltlem1  14456  iseralt  14459  isumclim2  14533  isumclim3  14534  isumge0  14541  fsumless  14572  cvgcmp  14592  cvgcmpce  14594  abscvgcvg  14595  isumsup2  14622  isumltss  14624  climcndslem1  14625  climcnds  14627  supcvg  14632  harmonic  14635  expcnv  14640  explecnv  14641  cvgrat  14659  mertenslem1  14660  mertenslem2  14661  clim2div  14665  ntrivcvgtail  14676  iprodclim2  14774  iprodclim3  14775  efcvg  14859  ege2le3  14864  efaddlem  14867  eftlub  14883  effsumlt  14885  tanhlt1  14934  ef01bndlem  14958  sin02gt0  14966  rpnnen2lem4  14990  ruclem2  15005  ruclem3  15006  ruclem9  15011  iddvdsexp  15052  dvdsadd  15071  dvdsfac  15095  dvdsmod  15097  3dvds  15099  3dvdsOLD  15100  omoe  15135  sumeven  15157  divalglem1  15164  flodddiv4t2lthalf  15187  bitsfzo  15204  bitsmod  15205  bitscmp  15207  bitsinv1lem  15210  sadcaddlem  15226  sadadd3  15230  sadaddlem  15235  dvdssqim  15320  dvdsmulgcd  15321  nn0seqcvgd  15330  dvdslcm  15358  lcmgcdlem  15366  dvdslcmf  15391  lcmfunsnlem2lem2  15399  mulgcddvds  15416  qredeq  15418  cncongr2  15429  sqnprm  15461  isprm6  15473  nonsq  15514  hashdvds  15527  prmdiv  15537  odzdvds  15547  pythagtriplem4  15571  pcpre1  15594  pcdvdsb  15620  pcz  15632  pcprmpw2  15633  pcaddlem  15639  pcadd  15640  pcadd2  15641  pcmpt  15643  pcmptdvds  15645  fldivp1  15648  pcfaclem  15649  pockthlem  15656  prmreclem1  15667  prmreclem3  15669  prmreclem5  15671  prmreclem6  15672  4sqlem6  15694  4sqlem8  15696  4sqlem11  15706  4sqlem12  15707  4sqlem14  15709  4sqlem16  15711  vdwlem3  15734  vdwlem9  15740  vdwlem10  15741  vdwlem12  15743  ramub1lem2  15778  prmgap  15810  prmgaplcm  15811  prmgapprmo  15813  mreexexd  16355  invfuc  16681  ple1  17091  eqgen  17694  lagsubg  17703  pgpfi  18066  sylow2alem2  18079  sylow2a  18080  sylow3lem4  18091  efgsrel  18193  odadd1  18297  odadd2  18298  gexex  18302  lt6abl  18342  dprd2d2  18489  dmdprdpr  18494  ablfacrp2  18512  ablfac1c  18516  pgpfaclem1  18526  ablfac2  18534  dvdsrmul1  18699  unitmulclb  18711  subrguss  18843  abvres  18887  ply1coefsupp  19713  evl1gsumadd  19770  znfld  19957  znunit  19960  frlmisfrlm  20235  matgsum  20291  pm2mpcl  20650  psmetxrge0  22165  isxmet2d  22179  mettri  22204  xmettri3  22205  mettri3  22206  xmetrtri2  22208  prdsxmetlem  22220  imasdsf1olem  22225  xblss2ps  22253  blss2ps  22255  blss2  22256  blssps  22276  blss  22277  prdsbl  22343  dscmet  22424  nmge0  22468  nmmtri  22473  tngngp3  22507  nlmvscnlem2  22536  nrginvrcnlem  22542  nmoix  22580  nmoleub  22582  blcvx  22648  xrsxmet  22659  opnreen  22681  xrge0tsms  22684  icopnfcnv  22788  xrhmeo  22792  lebnumii  22812  pcophtb  22875  pi1grplem  22895  nmoleub2lem  22960  ipcau2  23079  tchcphlem1  23080  ipcau  23083  ipcnlem2  23089  rrxcph  23226  minveclem2  23243  minveclem3b  23245  pjthlem1  23254  pjthlem2  23255  ivthlem3  23268  ivth2  23270  ovolfsf  23286  ovolsslem  23298  ovollb2lem  23302  ovollb2  23303  ovolctb  23304  ovolfiniun  23315  ovolicc1  23330  ovolicc2lem4  23334  ovolicc2  23336  nulmbl2  23350  unmbl  23351  ioombl1lem4  23375  uniioombllem4  23400  uniioombllem6  23402  volivth  23421  vitalilem4  23425  itg1ge0  23498  itg1ge0a  23523  itg1lea  23524  itg1climres  23526  mbfi1fseqlem5  23531  itg2ub  23545  itg2seq  23554  itg2uba  23555  itg2splitlem  23560  itg2split  23561  itg2monolem3  23564  itg2mono  23565  itg2i1fseq2  23568  itg2addlem  23570  iblss  23616  itggt0  23653  dvferm2lem  23794  dvlip  23801  dvivthlem1  23816  dvfsumlem2  23835  dvfsumlem3  23836  ftc1lem4  23847  ply1divmo  23940  ply1remlem  23967  fta1glem2  23971  ig1pdvds  23981  plyeq0lem  24011  plydiveu  24098  fta1lem  24107  vieta1lem2  24111  aaliou3lem2  24143  aaliou3lem8  24145  ulmcn  24198  mtest  24203  itgulm  24207  radcnvlem1  24212  radcnvlt1  24217  dvradcnv  24220  pserdvlem2  24227  abelthlem2  24231  abelthlem6  24235  abelthlem7  24237  abelthlem9  24239  tangtx  24302  sinq12gt0  24304  sineq0  24318  cosordlem  24322  tanord  24329  tanregt0  24330  logrnaddcl  24366  logcj  24397  argregt0  24401  argrege0  24402  argimgt0  24403  argimlt0  24404  logimul  24405  logneg2  24406  logdivlti  24411  divlogrlim  24426  logcnlem3  24435  logcnlem4  24436  dvlog2lem  24443  logtayl  24451  rpcxpcl  24467  cxpsqrtlem  24493  cxpaddle  24538  isosctrlem1  24593  asinlem3a  24642  asinlem3  24643  asinneg  24658  asinsinlem  24663  asinsin  24664  atanlogaddlem  24685  atanlogadd  24686  atanlogsublem  24687  atanlogsub  24688  atantan  24695  atanbndlem  24697  atantayl  24709  leibpi  24714  birthdaylem3  24725  areaf  24733  cxploglim  24749  jensenlem2  24759  jensen  24760  logdiflbnd  24766  harmonicbnd4  24782  fsumharmonic  24783  zetacvg  24786  lgamgulmlem2  24801  lgamgulmlem3  24802  lgamcvg2  24826  wilthlem2  24840  wilthimp  24843  ftalem1  24844  ftalem2  24845  ftalem5  24848  basellem6  24857  basellem8  24859  basellem9  24860  chtge0  24883  chtublem  24981  logexprlim  24995  perfectlem1  24999  bcmax  25048  bposlem1  25054  bposlem2  25055  bposlem6  25059  bposlem7  25060  lgsdilem2  25103  lgsqrlem4  25119  lgsquadlem1  25150  2lgsoddprmlem2  25179  2sqlem3  25190  2sqlem8  25196  2sqblem  25201  chebbnd1lem2  25204  chtppilimlem1  25207  chtppilim  25209  chto1ub  25210  vmadivsum  25216  rplogsumlem1  25218  rplogsumlem2  25219  dchrisum0lem1a  25220  rpvmasumlem  25221  dchrisumlem1  25223  dchrisumlem2  25224  dchrvmasumlem2  25232  dchrisum0flblem1  25242  dchrisum0flblem2  25243  dchrisum0lem1b  25249  dchrisum0lem1  25250  dchrisum0lem2a  25251  dchrisum0lem3  25253  dchrisum0  25254  mudivsum  25264  mulogsumlem  25265  mulog2sumlem1  25268  mulog2sumlem2  25269  2vmadivsumlem  25274  chpdifbndlem1  25287  selberg3lem1  25291  selberg4lem1  25294  pntrlog2bndlem1  25311  pntrlog2bndlem2  25312  pntrlog2bndlem3  25313  pntrlog2bndlem4  25314  pntpbnd1a  25319  pntpbnd1  25320  pntpbnd2  25321  pntibndlem2  25325  pntibndlem3  25326  pntlemd  25328  pntlemc  25329  pntlemb  25331  pntlemg  25332  pntlemh  25333  pntlemr  25336  pntlemf  25339  pntlemo  25341  abvcxp  25349  ostth2lem1  25352  padicabv  25364  ostth2lem2  25368  ostth2lem3  25369  ostth2lem4  25370  ostth2  25371  ostth3  25372  tgcgr4  25471  legso  25539  krippenlem  25630  midex  25674  oppperpex  25690  ttgcontlem1  25810  axpaschlem  25865  axcontlem8  25896  upgrex  26032  nbfusgrlevtxm1  26323  finsumvtxdgeven  26504  wwlksnextproplem3  26874  clwlkclwwlk2  26969  clwwlkndivn  27044  clwlksf1clwwlklem1  27052  ex-ind-dvds  27448  nvabs  27655  nmooge0  27750  nmoolb  27754  siii  27836  minvecolem2  27859  minvecolem4  27864  minvecolem5  27865  hlipgt0  27898  normge0  28111  normpyc  28131  pjhthlem1  28378  pjige0i  28677  nmoplb  28894  nmfnlb  28911  branmfn  29092  pjssdif2i  29161  stlei  29227  xlt2addrd  29651  eliccelico  29667  elicoelioo  29668  bcm1n  29682  fsumiunle  29703  2sqmod  29776  omndmul2  29840  archirngz  29871  archiabllem2c  29877  xrge0tsmsd  29913  ofldchr  29942  psgnfzto1stlem  29978  madjusmdetlem2  30022  locfinreflem  30035  xrge0iifiso  30109  nexple  30199  gsumesum  30249  esumcst  30253  esumpcvgval  30268  esumcvg  30276  esumiun  30284  measssd  30406  measunl  30407  omssubadd  30490  carsgclctunlem3  30510  pmeasmono  30514  sibfof  30530  oddpwdc  30544  eulerpartlemgc  30552  iwrdsplit  30577  ballotlemsgt1  30700  ballotlemsel1i  30702  sgnmul  30732  signsply0  30756  signstfvc  30779  signsvtp  30788  signsvfpn  30790  fdvposlt  30805  fdvneggt  30806  fdvnegge  30808  logdivsqrle  30856  hgt750lemf  30859  tgoldbachgtde  30866  subfaclim  31296  erdszelem7  31305  erdszelem8  31306  cvmliftlem2  31394  snmlff  31437  sinccvglem  31692  climlec3  31745  faclim  31758  dvdspw  31762  nodense  31967  nosupbnd2lem1  31986  noetalem2  31989  fnejoin1  32488  poimirlem12  33551  poimirlem17  33556  poimirlem19  33558  poimirlem20  33559  poimirlem23  33562  poimirlem28  33567  broucube  33573  mblfinlem2  33577  mblfinlem3  33578  mblfinlem4  33579  ismblfin  33580  itg2addnclem  33591  itg2addnclem3  33593  itg2gt0cn  33595  itggt0cn  33612  ftc1anclem5  33619  ftc1anclem7  33621  ftc1anclem8  33622  isbnd3  33713  ssbnd  33717  heiborlem8  33747  bfplem2  33752  rrncmslem  33761  rrnequiv  33764  rrntotbnd  33765  lcv1  34646  lsatcv0eq  34652  lsatcvat3  34657  cvlsupr2  34948  hlatlej2  34980  cvrval4N  35018  cvratlem  35025  atcvr0eq  35030  2atlt  35043  atbtwnex  35052  athgt  35060  1cvrat  35080  ps-1  35081  hlatexch3N  35084  hlatexch4  35085  3atlem2  35088  atcvrlln2  35123  lplnexllnN  35168  4atlem3a  35201  4atlem10b  35209  4atlem11b  35212  4atlem12b  35215  2lplnja  35223  dalemply  35258  dalemsly  35259  dalem1  35263  dalem6  35272  dalem7  35273  dalem-cly  35275  dalem11  35278  dalem12  35279  dalem16  35283  dalem17  35284  dalem38  35314  dalem44  35320  dalem61  35337  lnatexN  35383  lncvrat  35386  lncmp  35387  paddasslem2  35425  dalawlem3  35477  dalawlem6  35480  dalawlem11  35485  lhpmcvr  35627  lhp2atne  35638  lhp2at0ne  35640  lautj  35697  trlval4  35793  cdlemc2  35797  cdlemc5  35800  cdleme3b  35834  cdleme11c  35866  cdleme19a  35908  cdleme20j  35923  cdleme22f  35951  cdleme23c  35956  cdleme26f2ALTN  35969  cdleme26f2  35970  cdleme35fnpq  36054  cdleme48bw  36107  cdlemg10a  36245  cdlemg11b  36247  cdlemg17g  36272  cdlemg18c  36285  cdlemi1  36423  cdlemk52  36559  dia2dimlem1  36670  dihord1  36824  dihjatcclem4  37027  eldioph2lem1  37640  lzenom  37650  irrapxlem1  37703  irrapxlem4  37706  irrapxlem5  37707  pell14qrgt0  37740  pell1qrge1  37751  pell1qrgap  37755  pellfundge  37763  pellfundex  37767  pellfund14  37779  rmspecsqrtnq  37787  rmspecsqrtnqOLD  37788  rmxypos  37831  ltrmynn0  37832  ltrmxnn0  37833  jm2.24nn  37843  jm2.17b  37845  jm2.17c  37846  jm2.24  37847  congadd  37850  congsym  37852  congneg  37853  congid  37855  mzpcong  37856  acongrep  37864  acongeq  37867  jm2.18  37872  jm2.19  37877  jm2.23  37880  jm2.25  37883  jm2.26lem3  37885  jm2.15nn0  37887  jm2.16nn0  37888  jm2.27a  37889  jm2.27c  37891  jm3.1lem1  37901  idomrootle  38090  idomsubgmo  38093  inductionexd  38770  imo72b2  38792  dvgrat  38828  radcnvrat  38830  binomcxplemnn0  38865  binomcxplemnotnn0  38872  cncmpmax  39505  rnmptlb  39767  zltlesub  39811  infxrpnf  39987  xrpnf  40029  fmul01  40130  fmul01lt1lem1  40134  climdivf  40162  sumnnodd  40180  climinf2lem  40256  limsup10exlem  40322  climliminf  40356  dfxlim2v  40391  dvdivbd  40456  volge0  40495  stoweidlem1  40536  stoweidlem16  40551  stoweidlem18  40553  stoweidlem24  40559  stoweidlem26  40561  stoweidlem36  40571  stoweidlem38  40573  stoweidlem41  40576  stoweidlem42  40577  stoweidlem44  40579  stoweidlem45  40580  stoweidlem48  40583  stoweidlem62  40597  wallispilem5  40604  stirlinglem1  40609  stirlinglem5  40613  stirlinglem7  40615  stirlinglem8  40616  stirlinglem9  40617  stirlinglem11  40619  fourierdlem4  40646  fourierdlem10  40652  fourierdlem37  40679  fourierdlem47  40688  fourierdlem72  40713  fourierdlem74  40715  fourierdlem79  40720  fourierdlem82  40723  fourierdlem89  40730  fourierdlem91  40732  fourierdlem93  40734  fourierdlem103  40744  fourierdlem104  40745  fourierdlem112  40753  etransclem24  40793  etransclem25  40794  etransclem28  40797  etransclem37  40806  etransclem38  40807  etransclem44  40813  meaiuninc3v  41019  vonicclem1  41218  pimconstlt0  41235  smfsuplem1  41338  rlimdmafv  41578  2elfz2melfz  41653  iccpartgtprec  41681  iccpartlt  41685  iccpartgtl  41687  sqrtpwpw2p  41775  fmtnodvds  41781  goldbachthlem1  41782  lighneallem4a  41850  perfectALTVlem1  41955  cznnring  42281  rhmsubcrngc  42354  altgsumbcALT  42456  expnegico01  42633  flnn0div2ge  42652  rege1logbrege0  42677  fllogbd  42679  fllog2  42687  nnpw2blen  42699  nnolog2flm1  42709  dignn0ldlem  42721  dignn0flhalflem1  42734  dignn0flhalflem2  42735
  Copyright terms: Public domain W3C validator