Theorem breq2 4451

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

Step	Hyp	Ref	Expression
1		opeq2 4214	. . 3 |- ( A = B -> <. C , A >. = <. C , B >. )
2	1	eleq1d 2536	. 2 |- ( A = B -> ( <. C , A >. e. R <-> <. C , B >. e. R ) )
3		df-br 4448	. 2 |- ( C R A <-> <. C , A >. e. R )
4		df-br 4448	. 2 |- ( C R B <-> <. C , B >. e. R )
5	2, 3, 4	3bitr4g 288	1 |- ( A = B -> ( C R A <-> C R B ) )

Syntax hints:   -> wi 4   <-> wb 184   = wceq 1379   e. wcel 1767   <.cop 4033   class class class wbr 4447

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-rab 2823  df-v 3115  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-sn 4028  df-pr 4030  df-op 4034  df-br 4448

This theorem is referenced by:  breq12  4452  breq2i  4455  breq2d  4459  nbrne1  4464  pocl  4807  swopolem  4809  swopo  4810  solin  4823  sotric  4826  sotrieq  4827  isso2i  4832  somo  4834  seex  4842  frirr  4856  fr2nr  4857  frminex  4859  wereu2  4876  vtoclr  5043  posn  5067  frsn  5069  brcog  5167  brcogw  5169  opelcnvg  5180  dfdmf  5194  breldmg  5206  dfrnf  5239  dmcoss  5260  resieq  5282  dfres2  5324  elimag  5339  elrelimasn  5359  elimasn  5360  asymref2  5382  intirr  5383  poirr2  5389  sotri3  5395  poltletr  5400  soltmin  5404  dffun3  5597  dffun6f  5600  fun11  5651  brprcneu  5857  fv3  5877  tz6.12c  5883  tz6.12i  5884  funbrfv  5904  fnbrfvb  5906  funfv2f  5934  dffv2  5938  fvopab5  5971  fndmdif  5983  dff3  6032  fmptco  6052  foeqcnvco  6189  isorel  6208  soisores  6209  soisoi  6210  isocnv  6212  isotr  6218  isopolem  6227  isosolem  6229  f1oiso  6233  f1oiso2  6234  caovordig  6462  caovordg  6464  caovord  6468  caofrss  6555  caoftrn  6557  fr3nr  6593  dfwe2  6595  f1oweALT  6765  frxp  6890  poxp  6892  suppimacnv  6909  tposoprab  6988  ertr  7323  ecopovsym  7410  ecopovtrn  7411  domeng  7527  eqeng  7546  snfi  7593  sbth  7634  domunsn  7664  domssex  7675  nneneq  7697  php2  7699  onfin  7705  1sdom  7719  unxpdom  7724  isinf  7730  fineqvlem  7731  pssnn  7735  ssnnfi  7736  dif1enOLD  7748  dif1en  7749  findcard  7755  findcard2  7756  findcard3  7759  frfi  7761  fisupg  7764  nnsdomg  7775  unfi  7783  fiint  7793  mapfien2  7864  supmo  7908  eqsup  7912  supub  7915  suplub  7916  suplub2  7917  supmaxlem  7920  fisup2g  7922  fisupcl  7923  suppr  7925  supisolem  7927  supisoex  7928  ordtypecbv  7938  ordtypelem3  7941  ordtypelem6  7944  ordtypelem7  7945  ordtypelem9  7947  wemaplem1  7967  wemaplem2  7968  harval  7984  wemapwe  8135  wemapweOLD  8136  r111  8189  cardf2  8320  isnum2  8322  cardval3  8329  cardnueq0  8341  carden2a  8343  cardlim  8349  isinffi  8369  onsdom  8373  harval2  8374  cardmin2  8375  ondomen  8414  alephnbtwn  8448  alephinit  8472  aceq3lem  8497  infmap2  8594  cfslb2n  8644  sornom  8653  isfin4  8673  fin23lem26  8701  fin23lem27  8704  fin1a2lem11  8786  fin1a2lem12  8787  hsmex  8808  domtriomlem  8818  dominf  8821  zorn2lem2  8873  zorn2lem7  8878  zorn2g  8879  axdclem  8895  axdc  8897  fodomg  8899  brdom7disj  8905  brdom6disj  8906  cardmin  8935  ficard  8936  alephval2  8943  dominfac  8944  cfpwsdom  8955  gchi  8998  fpwwe2lem12  9015  fpwwe2lem13  9016  canthp1lem1  9026  canthp1lem2  9027  pwfseqlem4a  9035  pwfseqlem4  9036  elina  9061  winainflem  9067  eltskg  9124  rankcf  9151  indpi  9281  nqereu  9303  nsmallnq  9351  ltbtwnnq  9352  ltrnq  9353  prcdnq  9367  genpcd  9380  genpnmax  9381  ltaddpr2  9409  ltexprlem4  9413  prlem936  9421  reclem2pr  9422  reclem3pr  9423  supexpr  9428  ltsosr  9467  ltasr  9473  recexsrlem  9476  mulgt0sr  9478  map2psrpr  9483  supsrlem  9484  axpre-lttri  9538  axpre-lttrn  9539  axpre-ltadd  9540  axpre-mulgt0  9541  axpre-sup  9542  ltletr  9672  letr  9674  ltne  9677  eqle  9683  dedekind  9739  dedekindle  9740  ltordlem  10074  elimgt0  10374  elimge0  10375  squeeze0  10444  fimaxre2  10487  lbreu  10489  lble  10491  sup2  10495  infm3  10498  suprlub  10501  supmul1  10504  supmullem1  10505  supmullem2  10506  supmul  10507  infmrcl  10518  infmrgelb  10519  nn2ge  10557  nnge1  10558  nnsub  10570  nominpos  10771  nnunb  10787  elnnnn0b  10836  nn0sub  10842  nn0ge2m1nn  10857  peano2uz2  10944  peano5uzi  10945  dfuzi  10947  uzind  10948  uzind3  10950  uzindOLD  10951  uzind3OLD  10952  eluz1  11082  uzind4  11135  uzwo  11140  uzwoOLD  11141  nnwof  11144  indstr2  11156  ublbneg  11162  zsupss  11167  uzsupss  11170  uzwo3  11173  zmin  11174  zmax  11175  zbtwnre  11176  rebtwnz  11177  rpnnen1lem1  11204  rpnnen1lem2  11205  rpnnen1lem3  11206  rpnnen1lem4  11207  rpnnen1lem5  11208  reexALT  11210  elrp  11218  mnfltxr  11332  nn0pnfge0  11337  xrltnsym  11339  xrlttri  11341  xrlttr  11342  xrltletr  11356  xrletr  11357  ngtmnft  11364  xrltmin  11379  xrlemin  11381  ifle  11392  z2ge  11393  qbtwnre  11394  qbtwnxr  11395  qextlt  11398  qextle  11399  xltnegi  11411  xmullem2  11453  xmulasslem2  11470  xmulasslem  11473  xlemul1a  11476  xrsupexmnf  11492  xrsupsslem  11494  xrinfmsslem  11495  xrub  11499  supxrpnf  11506  supxrunb1  11507  supxrunb2  11508  ixxval  11533  elixx1  11534  elioo2  11566  iccid  11570  icc0  11573  iccsupr  11613  repos  11617  supicc  11664  supiccub  11665  supicclub  11666  fzval  11670  elfz1  11673  flval  11895  flval2  11913  flval3  11914  dfceil2  11931  uzsup  11953  modid2  11986  fsequb  12048  ssnn0fi  12057  rabssnn0fi  12058  suppssfz  12063  serge0  12124  expge0  12164  expge1  12165  facdiv  12327  facwordi  12329  hashkf  12369  hashnnn0genn0  12378  hashv01gt1  12380  hashneq0  12396  hashdom  12409  hashnn0n0nn  12420  hashss  12433  hashgt12el  12440  hashgt12el2  12441  hashge2el2dif  12481  brfi1uzind  12492  wrdlen1  12538  fstwrdne0  12540  wrdeqswrdlsw  12631  2swrdeqwrdeq  12635  2swrd1eqwrdeq  12636  ccats1swrdeq  12651  ccats1swrdeqrex  12661  swrdccatin12lem3  12672  2swrd2eqwrdeq  12848  shftfib  12862  shftfn  12863  2shfti  12870  sqrlem3  13035  resqrex  13041  cau3lem  13143  caubnd2  13146  caubnd  13147  sqreu  13149  limsuple  13257  limsupval2  13259  rlim2  13275  climi  13289  rlimi  13292  ello12r  13296  ello1mpt  13300  ello1d  13302  lo1bdd2  13303  lo1bddrp  13304  elo12r  13307  o1lo1  13316  rlimclim1  13324  rlimdm  13330  climeu  13334  climmo  13336  2clim  13351  o1co  13365  o1compt  13366  addcn2  13372  mulcn2  13374  reccn2  13375  cn1lem  13376  rlimo1  13395  lo1add  13405  lo1mul  13406  climsup  13448  caucvgrlem  13451  caucvgb  13458  summo  13495  zsum  13496  fsum  13498  o1fsum  13583  climcnds  13619  supcvg  13623  rpnnen2lem4  13805  rpnnen  13814  ruclem2  13819  ruclem12  13828  sqrt2irr  13836  dvdsabsb  13857  0dvds  13858  dvdsle  13883  alzdvds  13888  dvdsext  13889  fzo0dvdseq  13891  divalglem10  13912  bitsinv1lem  13943  sadadd3  13963  bitsuz  13976  gcdval  13998  gcdcllem1  14001  gcdcllem2  14002  gcddvds  14005  bezoutlem4  14031  dvdsgcd  14033  dvdssq  14050  isprm  14071  isprm2lem  14076  dvdsprm  14092  coprmdvds2  14096  isprm6  14102  exprmfct  14103  maxprmfct  14106  prmexpb  14110  prmfac1  14111  rpexp  14113  iserodd  14211  pceu  14222  pczpre  14223  pcdiv  14228  pcdvdsb  14244  pcmpt  14263  pcmptdvds  14265  prmpwdvds  14274  unbenlem  14278  infpnlem2  14281  infpn2  14283  prmreclem1  14286  prmreclem2  14287  prmreclem3  14288  prmreclem5  14290  prmreclem6  14291  vdwlem9  14359  vdwlem10  14360  vdwlem13  14363  ramz  14395  imasleval  14789  mreexexlem3d  14894  mreexexlem4d  14895  mreexexd  14896  prslem  15411  drsdirfi  15418  posi  15430  posasymb  15432  pleval2  15445  plttr  15450  pltletr  15451  pospo  15453  lubprop  15466  lublecllem  15468  glbprop  15479  glble  15480  joinlem  15491  joinle  15494  meetval2lem  15502  meetlem  15505  isglbd  15597  lubl  15600  lubun  15603  pospropd  15614  poslubmo  15626  posglbmo  15627  poslubd  15628  tsrlin  15699  tsrlemax  15700  letsr  15707  eqgen  16046  odeq  16367  odmulg  16371  pgpssslw  16427  sylow2alem2  16431  sylow2blem3  16435  efgval2  16535  efgsfo  16550  efgred  16559  efgredeu  16563  efgcpbllemb  16566  gexex  16649  cyggex2  16687  gsummptnn0fz  16802  gsummptnn0fzfv  16804  pgpfaclem1  16919  pgpfaclem2  16920  pgpfaclem3  16921  ablfaclem2  16924  ablfaclem3  16925  lidldvgen  17682  psrass1lem  17797  psrmulval  17807  mplmonmul  17894  opsrtoslem2  17917  coe1mul2  18078  coe1tmmul2fv  18087  coe1pwmulfv  18089  gsummoncoe1  18114  zndvds  18352  znleval  18357  islinds  18608  pmatcoe1fsupp  18966  mp2pm2mplem4  19074  fvmptnn04ifa  19115  fvmptnn04ifd  19118  chfacffsupp  19121  chfacfscmul0  19123  chfacfpmmul0  19127  cpmadumatpoly  19148  cayleyhamilton  19155  cayleyhamiltonALT  19156  ordtbaslem  19452  ordtbas2  19455  ordtopn1  19458  mnfnei  19485  ordtt1  19643  ordthauslem  19647  ordthmeolem  20034  trust  20464  ucncn  20520  imasdsf1olem  20608  comet  20748  stdbdxmet  20750  stdbdmet  20751  stdbdmopn  20753  metcnpi  20779  metcnpi2  20780  metcnpi3  20781  ngptgp  20882  nlmvscnlem1  20927  nrginvrcnlem  20931  nmogelb  20955  nmolb  20956  nghmcn  20984  xrsxmet  21046  icccmplem2  21060  icccmplem3  21061  reconnlem2  21064  xrge0tsms  21071  xmetdcn2  21074  metdsf  21084  metdsge  21085  metdscn  21092  metnrmlem1a  21094  addcnlem  21100  cncfi  21130  elcncf1di  21131  iccpnfhmeo  21177  xrhmeo  21178  cnllycmp  21188  evth  21191  ipcnlem1  21417  lmmcvg  21432  cfili  21439  cncmet  21493  minveclem1  21571  minveclem3b  21575  minveclem6  21581  pmltpclem1  21592  pmltpc  21594  ivthlem2  21596  ivthlem3  21597  cniccbdd  21605  ovolmge0  21620  ovolgelb  21623  ovolctb  21633  ovolunlem1  21640  ovoliunlem1  21645  ovoliun  21648  ovoliun2  21649  ovolshftlem1  21652  ovolscalem1  21656  ovolicc2lem3  21662  ovolicc2lem5  21664  ovolicc2  21665  voliunlem3  21694  ioombl1lem1  21700  ioombl1lem4  21703  uniioombllem2  21724  uniioombllem6  21729  volcn  21747  ismbfd  21779  mbfsup  21803  mbfinf  21804  mbflimsup  21805  itg1ge0  21825  itg1climres  21853  mbfi1fseqlem5  21858  itg2val  21867  itg2const  21879  itg2const2  21880  itg2seq  21881  itg2monolem1  21889  itg2i1fseq  21894  itg2i1fseq2  21895  itg2addlem  21897  itg2cnlem1  21900  itg2cnlem2  21901  itg2cn  21902  isibl  21904  ditgeq2  21985  dveflem  22112  dvferm1lem  22117  rolle  22123  c1lip1  22130  lhop1  22147  dvfsumlem2  22160  dvfsumlem4  22162  dvfsumrlim  22164  dvfsum2  22167  mdegmullem  22210  deg1leb  22227  deg1lt  22230  dvdsq1p  22293  plyeq0lem  22339  dgrco  22403  plydivex  22424  quotcan  22436  aannenlem1  22455  aannenlem2  22456  ulmi  22512  ulmcaulem  22520  ulmcau  22521  ulmbdd  22524  ulmdvlem3  22528  mtestbdd  22531  iblulm  22533  psercnlem1  22551  psercn  22552  abelthlem8  22565  sinhalfpilem  22586  logltb  22709  cxple2  22803  cxpcn3lem  22846  isosctrlem1  22877  leibpilem2  22997  cxploglim  23032  scvxcvx  23040  emcllem6  23055  ftalem3  23073  vmaval  23112  isppw2  23114  muval  23131  fsumdvdscom  23186  dvdsflf1o  23188  dvdsflsumcom  23189  musum  23192  muinv  23194  ppiublem1  23202  chtub  23212  logfac2  23217  bpos1lem  23282  bposlem9  23292  lgsdir  23330  lgsne0  23333  lgsqr  23346  lgsquadlem1  23354  lgsquadlem2  23355  lgsquadlem3  23356  2sqlem6  23369  2sqlem8  23372  2sqlem10  23374  dchrisumlema  23398  dchrisumlem2  23400  dchrisumlem3  23401  dchrvmasumiflem1  23411  dchrisum0fval  23415  dchrisum0ff  23417  dchrisum0flblem2  23419  logsqvma2  23453  pntrsumbnd2  23477  pntrlog2bndlem1  23487  pntpbnd1  23496  pntpbnd2  23497  pntibndlem2  23501  pntibndlem3  23502  pntibnd  23503  pntlemi  23514  pntlem3  23519  pntlemp  23520  pntleml  23521  pnt3  23522  tgldimor  23618  axcontlem10  23949  uhgra0v  23983  usgra0v  24044  usgra1v  24063  cusgraexg  24142  sizeusglecusg  24159  usgramaxsize  24160  3v3e3cycl1  24317  4cycl4v4e  24339  4cycl4dv  24340  wwlknred  24396  wwlkextwrd  24401  wwlkextfun  24402  wwlkextinj  24403  wwlkextproplem2  24415  wwlkextproplem3  24416  clwlkisclwwlklem1  24460  clwwlkf1  24469  clwwlkext2edg  24475  wwlkext2clwwlk  24476  wwlksubclwwlk  24477  clwlkfclwwlk  24517  clwlkfoclwwlk  24518  rusgranumwlks  24629  isfrgra  24663  vdgfrgragt2  24701  frgrawopreglem2  24719  clwwlkextfrlem1  24750  numclwwlkovf2ex  24760  friendshipgt3  24795  gxval  24933  vacn  25277  nmcvcn  25278  smcnlem  25280  nmobndi  25363  blocni  25393  ubthlem1  25459  ubthlem2  25460  ubthlem3  25461  minvecolem1  25463  minvecolem5  25470  minvecolem6  25471  htthlem  25507  norm3lemt  25742  hcaucvg  25776  hlimconvi  25781  hlim2  25782  chlimi  25825  hlimreui  25830  occl  25895  cmbr3  26199  cmcm  26205  cmcm3  26206  lecm  26208  cnopc  26505  cnfnc  26522  0cnop  26571  0cnfn  26572  idcnop  26573  nmopun  26606  nmcexi  26618  lnconi  26625  branmfn  26697  opsqrlem1  26732  pjnmopi  26740  pjnormssi  26760  stge1i  26830  strlem5  26847  hstrlem5  26855  mddmd2  26901  csmdsymi  26926  cvmd  26928  ela  26931  cvbr4i  26959  chirredlem3  26984  chirredlem4  26985  chirred  26987  atmd  26991  mdsym  27004  mddmdin0i  27023  cdj1i  27025  cdj3i  27033  fmptcof2  27171  isoun  27189  xrge0infss  27245  ishashinf  27271  tleile  27308  toslublem  27314  tosglblem  27316  omndadd  27355  sgnsval  27377  isinftm  27384  xrnarchi  27387  archirng  27391  archiexdiv  27393  archiabllem1a  27394  archiabllem2a  27397  archiabl  27401  xrge0tsmsd  27435  orngmul  27453  isarchiofld  27467  ordtconlem1  27539  rge0scvg  27564  qqhcn  27605  qqhucn  27606  esumcst  27708  esumpinfval  27716  esumpcvgval  27721  esumcvg  27729  oddpwdc  27930  eulerpartlems  27936  eulerpartlemf  27946  eulerpartlemt  27947  eulerpartlemr  27950  eulerpartlemgvv  27952  eulerpartlemn  27957  dstfrvunirn  28050  ballotlemfcc  28069  sgnmulsgp  28126  signslema  28156  lgamgulmlem4  28211  lgamgulmlem5  28212  lgambdd  28216  subfacp1lem1  28260  relexpindlem  28534  relexpind  28535  rtrclreclem.trans  28541  ntrivcvgn0  28606  ntrivcvgmullem  28609  prodmo  28642  zprod  28643  fprod  28647  fprodntriv  28648  dfpo2  28758  fundmpss  28770  funbreq  28775  dfpred3g  28829  predbrg  28840  poseq  28907  wzel  28954  wsuclem  28955  wsuclb  28958  nodenselem4  29018  nodenselem5  29019  nodense  29023  nocvxminlem  29024  nobndup  29034  nofulllem5  29040  brtxp  29104  brtxp2  29105  brpprod3a  29110  elfix  29127  sscoid  29137  elfuns  29139  fnsingle  29143  brimageg  29151  fnimage  29153  brdomaing  29159  brrangeg  29160  funpartlem  29166  fvtransport  29256  fin2so  29614  supaddc  29615  supadd  29616  heicant  29624  mblfinlem1  29626  mblfinlem2  29627  mblfinlem3  29628  mblfinlem4  29629  ismblfin  29630  itg2addnclem  29641  itg2addnc  29644  itg2gt0cn  29645  ftc1anclem7  29671  ftc1anclem8  29672  ftc1anc  29673  trer  29709  elicc3  29710  finminlem  29711  nn0prpwlem  29715  nn0prpw  29716  fnessref  29763  refssfne  29764  fnemeet2  29786  filnetlem3  29799  frinfm  29827  fdc1  29840  nninfnub  29845  equivbnd  29887  heibor1lem  29906  heiborlem8  29915  iccbnd  29937  lzenom  30305  fphpdo  30353  rencldnfilem  30356  irrapxlem5  30364  irrapxlem6  30365  pellexlem3  30369  pellqrex  30417  pellfundre  30419  pellfundge  30420  pellfundlb  30422  pellfundglb  30423  monotoddzz  30481  oddcomabszz  30482  zindbi  30484  jm2.22  30541  jm2.23  30542  rpnnen3  30578  ttac  30582  fnwe2lem2  30601  aomclem8  30611  hbtlem1  30676  hbtlem5  30681  lcmcllem  30802  dvdslcm  30804  lcmledvds  30805  lcmgcdlem  30812  lcmdvds  30814  nzss  30822  ubelsupr  30973  climinf  31148  mullimc  31158  limcdm0  31160  mullimcf  31165  constlimc  31166  idlimc  31168  limsupre  31183  limcleqr  31186  addlimc  31190  0ellimcdiv  31191  limclner  31193  fperdvper  31248  dvdivbd  31253  dvbdfbdioo  31260  ioodvbdlimc1lem1  31261  ioodvbdlimc1lem2  31262  ioodvbdlimc2lem  31264  stoweidlem14  31314  stoweidlem29  31329  stoweidlem31  31331  stoweidlem34  31334  stoweidlem49  31349  wallispilem3  31367  stirlinglem13  31386  stirlinglem14  31387  fourierdlem16  31423  fourierdlem20  31427  fourierdlem21  31428  fourierdlem22  31429  fourierdlem25  31432  fourierdlem39  31446  fourierdlem41  31448  fourierdlem42  31449  fourierdlem45  31452  fourierdlem51  31458  fourierdlem54  31461  fourierdlem64  31471  fourierdlem77  31484  fourierdlem83  31490  fourierdlem87  31494  fourierdlem103  31510  fourierdlem104  31511  fourierdlem112  31519  fouriersw  31532  rlimdmafv  31729  assintopval  31953  0rngnnzr  32031  ply1mulgsumlem2  32060  ldepsnlinc  32190  bnj1185  32931  bnj602  33052  bnj1228  33146  bj-seex  33572  oposlem  33979  lub0N  33986  glb0N  33990  omllaw  34040  cvrval  34066  cvrnbtwn  34068  cvrnbtwn2  34072  cvrnbtwn3  34073  cvrcon3b  34074  cvrnbtwn4  34076  cvrcmp  34080  isat  34083  atnlt  34110  atlex  34113  cvlexch1  34125  cvlexchb1  34127  cvlatexch1  34133  glbconN  34173  2llnne2N  34204  cvratlem  34217  cvrat4  34239  ps-1  34273  3at  34286  islln  34302  llncmp  34318  llnnlt  34319  islpln  34326  islpln5  34331  lvolex3N  34334  lplncmp  34358  lplnexllnN  34360  lplnnlt  34361  islvol  34369  lvoli3  34373  islvol5  34375  lvolcmp  34413  lvolnltN  34414  dalem-cly  34467  dalem44  34512  pmapval  34553  pmapglbx  34565  lncvrelatN  34577  lncmp  34579  cdlemblem  34589  llnexchb2  34665  lautle  34880  lautcvr  34888  ldilset  34905  ltrnset  34914  trlset  34957  cdlemc4  34990  cdleme11dN  35058  cdleme20k  35115  cdleme21ct  35125  cdleme22b  35137  tendoex  35771  diafval  35828  diaval  35829  dicfval  35972  dihfval  36028  dihglblem2N  36091