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

Theorem breq2 4159
Description: Equality theorem for a binary relation. (Contributed by NM, 31-Dec-1993.)
Assertion
Ref Expression
breq2  |-  ( A  =  B  ->  ( C R A  <->  C R B ) )

Proof of Theorem breq2
StepHypRef Expression
1 opeq2 3929 . . 3  |-  ( A  =  B  ->  <. C ,  A >.  =  <. C ,  B >. )
21eleq1d 2455 . 2  |-  ( A  =  B  ->  ( <. C ,  A >.  e.  R  <->  <. C ,  B >.  e.  R ) )
3 df-br 4156 . 2  |-  ( C R A  <->  <. C ,  A >.  e.  R )
4 df-br 4156 . 2  |-  ( C R B  <->  <. C ,  B >.  e.  R )
52, 3, 43bitr4g 280 1  |-  ( A  =  B  ->  ( C R A  <->  C R B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    = wceq 1649    e. wcel 1717   <.cop 3762   class class class wbr 4155
This theorem is referenced by:  breq12  4160  breq2i  4163  breq2d  4167  nbrne1  4172  pocl  4453  swopolem  4455  swopo  4456  solin  4469  sotric  4472  sotrieq  4473  isso2i  4478  somo  4480  seex  4488  frirr  4502  fr2nr  4503  frminex  4505  wereu2  4522  fr3nr  4702  dfwe2  4704  vtoclr  4864  posn  4888  frsn  4890  brcog  4981  brcogw  4983  opelcnvg  4994  dfdmf  5006  breldmg  5017  dfrnf  5050  dmcoss  5077  resieq  5098  dfres2  5135  elimag  5149  elrelimasn  5170  elimasn  5171  asymref2  5193  intirr  5194  poirr2  5200  sotri3  5206  poltletr  5211  soltmin  5215  dffun3  5407  dffun6f  5410  fun11  5458  brprcneu  5663  fv3  5686  tz6.12c  5692  tz6.12i  5693  funbrfv  5706  fnbrfvb  5708  funfv2f  5733  dffv2  5737  fndmdif  5775  dff3  5823  fmptco  5842  foeqcnvco  5968  isorel  5987  soisores  5988  soisoi  5989  isocnv  5991  isotr  5997  isopolem  6006  isosolem  6008  f1oiso  6012  f1oiso2  6013  f1oweALT  6015  caovordig  6193  caovordg  6195  caovord  6199  caofrss  6278  caoftrn  6280  frxp  6394  poxp  6396  tposoprab  6453  fvopab5  6472  ertr  6858  ecopovsym  6944  ecopovtrn  6945  th3qlem2  6949  domeng  7060  eqeng  7079  snfi  7125  sbth  7165  domunsn  7195  domssex  7206  nneneq  7228  php2  7230  onfin  7235  1sdom  7249  unxpdom  7254  isinf  7260  fineqvlem  7261  pssnn  7265  ssnnfi  7266  dif1enOLD  7278  dif1en  7279  findcard  7285  findcard2  7286  findcard3  7288  frfi  7290  fisupg  7293  nnsdomg  7304  unfi  7312  fiint  7321  supmo  7392  eqsup  7396  supub  7399  suplub  7400  suplub2  7401  supmaxlem  7404  fisup2g  7406  fisupcl  7407  suppr  7408  supisolem  7410  supisoex  7411  ordtypecbv  7421  ordtypelem3  7424  ordtypelem6  7427  ordtypelem7  7428  ordtypelem9  7430  wemaplem1  7450  wemaplem2  7451  harval  7465  wemapwe  7589  r111  7636  cardf2  7765  isnum2  7767  cardval3  7774  cardnueq0  7786  carden2a  7788  cardlim  7794  isinffi  7814  onsdom  7818  harval2  7819  cardmin2  7820  ondomen  7853  alephnbtwn  7887  alephinit  7911  aceq3lem  7936  infmap2  8033  cfslb2n  8083  sornom  8092  isfin4  8112  fin23lem26  8140  fin23lem27  8143  fin1a2lem11  8225  fin1a2lem12  8226  hsmex  8247  domtriomlem  8257  dominf  8260  zorn2lem2  8312  zorn2lem7  8317  zorn2g  8318  axdclem  8334  axdc  8336  fodomg  8338  brdom7disj  8344  brdom6disj  8345  cardmin  8374  ficard  8375  alephval2  8382  dominfac  8383  cfpwsdom  8394  gchi  8434  fpwwe2lem12  8451  fpwwe2lem13  8452  canthp1lem1  8462  canthp1lem2  8463  pwfseqlem4a  8471  pwfseqlem4  8472  elina  8497  winainflem  8503  eltskg  8560  rankcf  8587  indpi  8719  nqereu  8741  nsmallnq  8789  ltbtwnnq  8790  ltrnq  8791  prcdnq  8805  genpcd  8818  genpnmax  8819  ltaddpr2  8847  ltexprlem4  8851  prlem936  8859  reclem2pr  8860  reclem3pr  8861  supexpr  8866  ltsosr  8904  ltasr  8910  recexsrlem  8913  mulgt0sr  8915  map2psrpr  8920  supsrlem  8921  axpre-lttri  8975  axpre-lttrn  8976  axpre-ltadd  8977  axpre-mulgt0  8978  axpre-sup  8979  ltletr  9101  letr  9102  ltne  9105  eqle  9111  ltordlem  9486  elimgt0  9780  elimge0  9781  squeeze0  9847  fimaxre2  9890  lbreu  9892  lble  9894  sup2  9898  infm3  9901  suprlub  9904  supmul1  9907  supmullem1  9908  supmullem2  9909  supmul  9910  infmrcl  9921  infmrgelb  9922  nn2ge  9959  nnge1  9960  nnsub  9972  nominpos  10138  nnunb  10151  elnnnn0b  10198  nn0sub  10204  peano2uz2  10291  peano5uzi  10292  dfuzi  10294  uzind  10295  uzind3  10297  uzindOLD  10298  uzind3OLD  10299  eluz1  10426  uzind4  10468  uzwo  10473  uzwoOLD  10474  nnwof  10477  indstr2  10488  ublbneg  10494  zsupss  10499  uzsupss  10502  uzwo3  10503  zmin  10504  zmax  10505  zbtwnre  10506  rebtwnz  10507  rpnnen1lem1  10534  rpnnen1lem2  10535  rpnnen1lem3  10536  rpnnen1lem4  10537  rpnnen1lem5  10538  reexALT  10540  elrp  10548  mnfltxr  10658  nn0pnfge0  10662  xrltnsym  10664  xrlttri  10666  xrlttr  10667  xrltletr  10681  xrletr  10682  ngtmnft  10689  xrltmin  10704  xrlemin  10706  ifle  10717  z2ge  10718  qbtwnre  10719  qbtwnxr  10720  qextlt  10723  qextle  10724  xltnegi  10736  xmullem2  10778  xmulasslem2  10795  xmulasslem  10798  xlemul1a  10801  xrsupexmnf  10817  xrsupsslem  10819  xrinfmsslem  10820  xrub  10824  supxrpnf  10831  supxrunb1  10832  supxrunb2  10833  ixxval  10858  elixx1  10859  elioo2  10891  iccid  10895  icc0  10898  iccsupr  10931  repos  10935  fzval  10979  elfz1  10982  flval  11132  flval2  11150  flval3  11151  uzsup  11173  modid2  11200  fsequb  11243  serge0  11306  expge0  11345  expge1  11346  facdiv  11507  facwordi  11509  hashkf  11549  hashnnn0genn0  11556  hashv01gt1  11558  hashdom  11582  hashnn0n0nn  11593  hashgt12el  11611  hashgt12el2  11612  brfi1uzind  11644  shftfib  11816  shftfn  11817  2shfti  11824  sqrlem3  11979  resqrex  11985  cau3lem  12087  caubnd2  12090  caubnd  12091  sqreu  12093  limsuple  12201  limsupval2  12203  rlim2  12219  climi  12233  rlimi  12236  ello12r  12240  ello1mpt  12244  ello1d  12246  lo1bdd2  12247  lo1bddrp  12248  elo12r  12251  o1lo1  12260  rlimclim1  12268  rlimdm  12274  climeu  12278  climmo  12280  2clim  12295  o1co  12309  o1compt  12310  addcn2  12316  mulcn2  12318  reccn2  12319  cn1lem  12320  rlimo1  12339  lo1add  12349  lo1mul  12350  climsup  12392  caucvgrlem  12395  caucvgb  12402  summo  12440  zsum  12441  fsum  12443  o1fsum  12521  climcnds  12560  supcvg  12564  rpnnen2lem4  12746  rpnnen  12755  ruclem2  12760  ruclem12  12769  sqr2irr  12777  dvdsabsb  12798  0dvds  12799  dvdsle  12824  alzdvds  12828  dvdsext  12829  fzo0dvdseq  12831  divalglem10  12851  bitsinv1lem  12882  sadadd3  12902  bitsuz  12915  gcdval  12937  gcdcllem1  12940  gcdcllem2  12941  gcddvds  12944  bezoutlem4  12970  dvdsgcd  12972  dvdssq  12989  isprm  13010  isprm2lem  13015  dvdsprm  13028  coprmdvds2  13032  isprm6  13038  exprmfct  13039  maxprmfct  13042  prmexpb  13046  prmfac1  13047  rpexp  13049  iserodd  13138  pceu  13149  pczpre  13150  pcdiv  13155  pcdvdsb  13171  pcmpt  13190  pcmptdvds  13192  prmpwdvds  13201  unbenlem  13205  infpnlem2  13208  infpn2  13210  prmreclem1  13213  prmreclem2  13214  prmreclem3  13215  prmreclem5  13217  prmreclem6  13218  vdwlem9  13286  vdwlem10  13287  vdwlem13  13290  ramz  13322  imasleval  13695  mreexexlem3d  13800  mreexexlem4d  13801  mreexexd  13802  prslem  14317  drsdirfi  14324  posi  14336  posasymb  14338  pleval2  14351  plttr  14356  pltletr  14357  pospo  14359  lubprop  14366  lubid  14368  glbprop  14371  glble  14372  joinlem  14376  joinle  14379  meetval2  14382  meetlem  14383  isglbd  14473  lubl  14476  lubun  14479  pospropd  14490  poslubmo  14502  poslubd  14503  tsrlin  14580  tsrlemax  14581  spwmo  14587  spwpr4  14592  letsr  14601  eqgen  14922  odeq  15117  odmulg  15121  pgpssslw  15177  sylow2alem2  15181  sylow2blem3  15185  efgval2  15285  efgsfo  15300  efgred  15309  efgredeu  15313  efgcpbllemb  15316  gexex  15397  cyggex2  15435  pgpfaclem1  15568  pgpfaclem2  15569  pgpfaclem3  15570  ablfaclem2  15573  ablfaclem3  15574  lidldvgen  16255  psrass1lem  16371  psrmulval  16379  mplmonmul  16456  opsrtoslem2  16474  coe1mul2  16591  coe1tmmul2fv  16599  coe1pwmulfv  16601  zndvds  16755  znleval  16760  ordtbaslem  17176  ordtbas2  17179  ordtopn1  17182  mnfnei  17209  ordtt1  17367  ordthauslem  17371  ordthmeolem  17756  trust  18182  ucncn  18238  imasdsf1olem  18313  comet  18435  stdbdxmet  18437  stdbdmet  18438  stdbdmopn  18440  metcnpi  18466  metcnpi2  18467  metcnpi3  18468  ngptgp  18550  nlmvscnlem1  18595  nrginvrcnlem  18599  nmogelb  18623  nmolb  18624  nghmcn  18652  xrsxmet  18713  icccmplem2  18727  icccmplem3  18728  reconnlem2  18731  xrge0tsms  18738  xmetdcn2  18741  metdsf  18751  metdsge  18752  metdscn  18759  metnrmlem1a  18761  addcnlem  18767  cncfi  18797  elcncf1di  18798  iccpnfhmeo  18843  xrhmeo  18844  cnllycmp  18854  evth  18857  ipcnlem1  19072  lmmcvg  19087  cfili  19094  cncmet  19146  minveclem1  19194  minveclem3b  19198  minveclem6  19204  pmltpclem1  19214  pmltpc  19216  ivthlem2  19218  ivthlem3  19219  cniccbdd  19227  ovolmge0  19242  ovolgelb  19245  ovolctb  19255  ovolunlem1  19262  ovoliunlem1  19267  ovoliun  19270  ovoliun2  19271  ovolshftlem1  19274  ovolscalem1  19278  ovolicc2lem3  19284  ovolicc2lem5  19286  ovolicc2  19287  voliunlem3  19315  ioombl1lem1  19321  ioombl1lem4  19324  uniioombllem2  19344  uniioombllem6  19349  volcn  19367  ismbfd  19401  mbfsup  19425  mbfinf  19426  mbflimsup  19427  itg1ge0  19447  itg1climres  19475  mbfi1fseqlem5  19480  itg2val  19489  itg2const  19501  itg2const2  19502  itg2seq  19503  itg2monolem1  19511  itg2i1fseq  19516  itg2i1fseq2  19517  itg2addlem  19519  itg2cnlem1  19522  itg2cnlem2  19523  itg2cn  19524  isibl  19526  ditgeq2  19605  dveflem  19732  dvferm1lem  19737  rolle  19743  c1lip1  19750  lhop1  19767  dvfsumlem2  19780  dvfsumlem4  19782  dvfsumrlim  19784  dvfsum2  19787  mdegmullem  19870  deg1leb  19887  deg1lt  19889  dvdsq1p  19952  plyeq0lem  19998  dgrco  20062  plydivex  20083  quotcan  20095  aannenlem1  20114  aannenlem2  20115  ulmi  20171  ulmcaulem  20179  ulmcau  20180  ulmbdd  20183  ulmdvlem3  20187  mtestbdd  20190  iblulm  20192  psercnlem1  20210  psercn  20211  abelthlem8  20224  sinhalfpilem  20243  logltb  20363  cxple2  20457  cxpcn3lem  20500  isosctrlem1  20531  leibpilem2  20650  cxploglim  20685  scvxcvx  20693  emcllem6  20708  ftalem3  20726  vmaval  20765  isppw2  20767  muval  20784  fsumdvdscom  20839  dvdsflf1o  20841  dvdsflsumcom  20842  musum  20845  muinv  20847  ppiublem1  20855  chtub  20865  logfac2  20870  bpos1lem  20935  bposlem9  20945  lgsdir  20983  lgsne0  20986  lgsqr  20999  lgsquadlem1  21007  lgsquadlem2  21008  lgsquadlem3  21009  2sqlem6  21022  2sqlem8  21025  2sqlem10  21027  dchrisumlema  21051  dchrisumlem2  21053  dchrisumlem3  21054  dchrvmasumiflem1  21064  dchrisum0fval  21068  dchrisum0ff  21070  dchrisum0flblem2  21072  logsqvma2  21106  pntrsumbnd2  21130  pntrlog2bndlem1  21140  pntpbnd1  21149  pntpbnd2  21150  pntibndlem2  21154  pntibndlem3  21155  pntibnd  21156  pntlemi  21167  pntlem3  21172  pntlemp  21173  pntleml  21174  pnt3  21175  uhgra0v  21214  usgra0v  21260  usgra1v  21277  cusgraexg  21346  sizeusglecusg  21363  usgramaxsize  21364  3v3e3cycl1  21481  4cycl4v4e  21503  4cycl4dv  21504  gxval  21696  vacn  22040  nmcvcn  22041  smcnlem  22043  nmobndi  22126  blocni  22156  ubthlem1  22222  ubthlem2  22223  ubthlem3  22224  minvecolem1  22226  minvecolem5  22233  minvecolem6  22234  htthlem  22270  norm3lemt  22504  hcaucvg  22538  hlimconvi  22543  hlim2  22544  chlimi  22587  hlimreui  22592  occl  22656  cmbr3  22960  cmcm  22966  cmcm3  22967  lecm  22969  cnopc  23266  cnfnc  23283  0cnop  23332  0cnfn  23333  idcnop  23334  nmopun  23367  nmcexi  23379  lnconi  23386  branmfn  23458  opsqrlem1  23493  pjnmopi  23501  pjnormssi  23521  stge1i  23591  strlem5  23608  hstrlem5  23616  mddmd2  23662  csmdsymi  23687  cvmd  23689  ela  23692  cvbr4i  23720  chirredlem3  23745  chirredlem4  23746  chirred  23748  atmd  23752  mdsym  23765  mddmdin0i  23784  cdj1i  23786  cdj3i  23794  fmptcof2  23920  isoun  23932  ishashinf  23999  xrge0tsmsd  24054  ofldadd  24066  ofldmul  24067  rge0scvg  24141  qqhcn  24176  qqhucn  24177  esumcst  24253  esumpinfval  24261  esumpcvgval  24266  esumcvg  24274  dstfrvunirn  24513  ballotlemfcc  24532  lgamgulmlem4  24597  lgamgulmlem5  24598  lgambdd  24602  subfacp1lem1  24646  relexpindlem  24920  relexpind  24921  rtrclreclem.trans  24927  dedekind  24968  dedekindle  24969  ntrivcvgn0  25007  ntrivcvgmullem  25010  prodmo  25043  zprod  25044  fprod  25048  fprodntriv  25049  dfpo2  25138  fundmpss  25148  funbreq  25153  predbrg  25212  poseq  25279  nodenselem4  25364  nodenselem5  25365  nodense  25369  nocvxminlem  25370  nobndup  25380  nofulllem5  25386  brtxp  25446  brtxp2  25447  brpprod3a  25452  elfix  25469  dffun10  25479  fnsingle  25484  brimageg  25492  fnimage  25494  brdomaing  25500  brrangeg  25501  brcup  25504  brcap  25505  funpartlem  25507  axcontlem10  25628  fvtransport  25682  supaddc  25949  supadd  25950  itg2addnclem  25959  itg2addnc  25961  itg2gt0cn  25962  trer  26012  elicc3  26013  finminlem  26014  nn0prpwlem  26018  nn0prpw  26019  fnessref  26066  refssfne  26067  fnemeet2  26089  filnetlem3  26102  frinfm  26130  fdc1  26143  nninfnub  26148  equivbnd  26192  heibor1lem  26211  heiborlem8  26220  iccbnd  26242  lzenom  26521  fphpdo  26571  rencldnfilem  26574  irrapxlem5  26582  irrapxlem6  26583  pellexlem3  26587  pellqrex  26635  pellfundre  26637  pellfundge  26638  pellfundlb  26640  pellfundglb  26641  monotoddzz  26699  oddcomabszz  26700  zindbi  26702  jm2.22  26759  jm2.23  26760  rpnnen3  26796  ttac  26800  fnwe2lem2  26819  aomclem8  26830  islinds  26950  hbtlem1  26998  hbtlem5  27003  xrltneNEW  27327  ubelsupr  27361  climinf  27402  stoweidlem14  27433  stoweidlem29  27448  stoweidlem31  27450  stoweidlem34  27453  stoweidlem49  27468  wallispilem3  27486  stirlinglem13  27505  stirlinglem14  27506  rlimdmafv  27712  isfrgra  27745  vdgfrgragt2  27783  frgrawopreglem2  27799  bnj1185  28505  bnj602  28626  bnj1228  28720  lubunNEW  29090  oposlem  29300  lub0N  29306  glb0N  29310  omllaw  29360  cvrval  29386  cvrnbtwn  29388  cvrnbtwn2  29392  cvrnbtwn3  29393  cvrcon3b  29394  cvrnbtwn4  29396  cvrcmp  29400  isat  29403  atnlt  29430  atlex  29433  cvlexch1  29445  cvlexchb1  29447  cvlatexch1  29453  glbconN  29493  2llnne2N  29524  cvratlem  29537  cvrat4  29559  ps-1  29593  3at  29606  islln  29622  llncmp  29638  llnnlt  29639  islpln  29646  islpln5  29651  lvolex3N  29654  lplncmp  29678  lplnexllnN  29680  lplnnlt  29681  islvol  29689  lvoli3  29693  islvol5  29695  lvolcmp  29733  lvolnltN  29734  dalem-cly  29787  dalem44  29832  pmapval  29873  pmapglbx  29885  lncvrelatN  29897  lncmp  29899  cdlemblem  29909  llnexchb2  29985  lautle  30200  lautcvr  30208  ldilset  30225  ltrnset  30234  trlset  30277  cdlemc4  30310  cdleme11dN  30378  cdleme20k  30435  cdleme21ct  30445  cdleme22b  30457  tendoex  31091  diafval  31148  diaval  31149  dicfval  31292  dihfval  31348  dihglblem2N  31411
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2370
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2376  df-cleq 2382  df-clel 2385  df-nfc 2514  df-rab 2660  df-v 2903  df-dif 3268  df-un 3270  df-in 3272  df-ss 3279  df-nul 3574  df-if 3685  df-sn 3765  df-pr 3766  df-op 3768  df-br 4156
  Copyright terms: Public domain W3C validator