Theorem breq2 4394

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 4158	. . 3 |- ( A = B -> <. C , A >. = <. C , B >. )
2	1	eleq1d 2520	. 2 |- ( A = B -> ( <. C , A >. e. R <-> <. C , B >. e. R ) )
3		df-br 4391	. 2 |- ( C R A <-> <. C , A >. e. R )
4		df-br 4391	. 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 1370   e. wcel 1758   <.cop 3981   class class class wbr 4390

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-rab 2804  df-v 3070  df-dif 3429  df-un 3431  df-in 3433  df-ss 3440  df-nul 3736  df-if 3890  df-sn 3976  df-pr 3978  df-op 3982  df-br 4391

This theorem is referenced by:  breq12  4395  breq2i  4398  breq2d  4402  nbrne1  4407  pocl  4746  swopolem  4748  swopo  4749  solin  4762  sotric  4765  sotrieq  4766  isso2i  4771  somo  4773  seex  4781  frirr  4795  fr2nr  4796  frminex  4798  wereu2  4815  vtoclr  4981  posn  5005  frsn  5007  brcog  5104  brcogw  5106  opelcnvg  5117  dfdmf  5131  breldmg  5143  dfrnf  5176  dmcoss  5197  resieq  5219  dfres2  5256  elimag  5271  elrelimasn  5291  elimasn  5292  asymref2  5313  intirr  5314  poirr2  5320  sotri3  5326  poltletr  5331  soltmin  5335  dffun3  5527  dffun6f  5530  fun11  5581  brprcneu  5782  fv3  5802  tz6.12c  5808  tz6.12i  5809  funbrfv  5829  fnbrfvb  5831  funfv2f  5859  dffv2  5863  fvopab5  5894  fndmdif  5906  dff3  5955  fmptco  5975  foeqcnvco  6097  isorel  6116  soisores  6117  soisoi  6118  isocnv  6120  isotr  6126  isopolem  6135  isosolem  6137  f1oiso  6141  f1oiso2  6142  caovordig  6368  caovordg  6370  caovord  6374  caofrss  6453  caoftrn  6455  fr3nr  6491  dfwe2  6493  f1oweALT  6661  frxp  6782  poxp  6784  suppimacnv  6801  tposoprab  6881  ertr  7216  ecopovsym  7302  ecopovtrn  7303  th3qlem2  7307  domeng  7424  eqeng  7443  snfi  7490  sbth  7531  domunsn  7561  domssex  7572  nneneq  7594  php2  7596  onfin  7602  1sdom  7616  unxpdom  7621  isinf  7627  fineqvlem  7628  pssnn  7632  ssnnfi  7633  dif1enOLD  7645  dif1en  7646  findcard  7652  findcard2  7653  findcard3  7656  frfi  7658  fisupg  7661  nnsdomg  7672  unfi  7680  fiint  7689  mapfien2  7759  supmo  7803  eqsup  7807  supub  7810  suplub  7811  suplub2  7812  supmaxlem  7815  fisup2g  7817  fisupcl  7818  suppr  7819  supisolem  7821  supisoex  7822  ordtypecbv  7832  ordtypelem3  7835  ordtypelem6  7838  ordtypelem7  7839  ordtypelem9  7841  wemaplem1  7861  wemaplem2  7862  harval  7878  wemapwe  8029  wemapweOLD  8030  r111  8083  cardf2  8214  isnum2  8216  cardval3  8223  cardnueq0  8235  carden2a  8237  cardlim  8243  isinffi  8263  onsdom  8267  harval2  8268  cardmin2  8269  ondomen  8308  alephnbtwn  8342  alephinit  8366  aceq3lem  8391  infmap2  8488  cfslb2n  8538  sornom  8547  isfin4  8567  fin23lem26  8595  fin23lem27  8598  fin1a2lem11  8680  fin1a2lem12  8681  hsmex  8702  domtriomlem  8712  dominf  8715  zorn2lem2  8767  zorn2lem7  8772  zorn2g  8773  axdclem  8789  axdc  8791  fodomg  8793  brdom7disj  8799  brdom6disj  8800  cardmin  8829  ficard  8830  alephval2  8837  dominfac  8838  cfpwsdom  8849  gchi  8892  fpwwe2lem12  8909  fpwwe2lem13  8910  canthp1lem1  8920  canthp1lem2  8921  pwfseqlem4a  8929  pwfseqlem4  8930  elina  8955  winainflem  8961  eltskg  9018  rankcf  9045  indpi  9177  nqereu  9199  nsmallnq  9247  ltbtwnnq  9248  ltrnq  9249  prcdnq  9263  genpcd  9276  genpnmax  9277  ltaddpr2  9305  ltexprlem4  9309  prlem936  9317  reclem2pr  9318  reclem3pr  9319  supexpr  9324  ltsosr  9362  ltasr  9368  recexsrlem  9371  mulgt0sr  9373  map2psrpr  9378  supsrlem  9379  axpre-lttri  9433  axpre-lttrn  9434  axpre-ltadd  9435  axpre-mulgt0  9436  axpre-sup  9437  ltletr  9567  letr  9569  ltne  9572  eqle  9578  dedekind  9634  dedekindle  9635  ltordlem  9966  elimgt0  10266  elimge0  10267  squeeze0  10336  fimaxre2  10379  lbreu  10381  lble  10383  sup2  10387  infm3  10390  suprlub  10393  supmul1  10396  supmullem1  10397  supmullem2  10398  supmul  10399  infmrcl  10410  infmrgelb  10411  nn2ge  10448  nnge1  10449  nnsub  10461  nominpos  10662  nnunb  10676  elnnnn0b  10725  nn0sub  10731  peano2uz2  10830  peano5uzi  10831  dfuzi  10833  uzind  10834  uzind3  10836  uzindOLD  10837  uzind3OLD  10838  eluz1  10966  uzind4  11013  uzwo  11018  uzwoOLD  11019  nnwof  11022  indstr2  11034  ublbneg  11040  zsupss  11045  uzsupss  11048  uzwo3  11049  zmin  11050  zmax  11051  zbtwnre  11052  rebtwnz  11053  rpnnen1lem1  11080  rpnnen1lem2  11081  rpnnen1lem3  11082  rpnnen1lem4  11083  rpnnen1lem5  11084  reexALT  11086  elrp  11094  mnfltxr  11208  nn0pnfge0  11213  xrltnsym  11215  xrlttri  11217  xrlttr  11218  xrltletr  11232  xrletr  11233  ngtmnft  11240  xrltmin  11255  xrlemin  11257  ifle  11268  z2ge  11269  qbtwnre  11270  qbtwnxr  11271  qextlt  11274  qextle  11275  xltnegi  11287  xmullem2  11329  xmulasslem2  11346  xmulasslem  11349  xlemul1a  11352  xrsupexmnf  11368  xrsupsslem  11370  xrinfmsslem  11371  xrub  11375  supxrpnf  11382  supxrunb1  11383  supxrunb2  11384  ixxval  11409  elixx1  11410  elioo2  11442  iccid  11446  icc0  11449  iccsupr  11483  repos  11487  supicc  11534  supiccub  11535  supicclub  11536  fzval  11540  elfz1  11543  flval  11745  flval2  11763  flval3  11764  dfceil2  11781  uzsup  11803  modid2  11836  fsequb  11898  serge0  11961  expge0  12001  expge1  12002  facdiv  12164  facwordi  12166  hashkf  12206  hashnnn0genn0  12215  hashv01gt1  12217  hashneq0  12233  hashdom  12244  hashnn0n0nn  12255  hashss  12268  hashgt12el  12275  hashgt12el2  12276  hashge2el2dif  12286  brfi1uzind  12321  fstwrdne0  12366  wrdeqswrdlsw  12445  2swrdeqwrdeq  12449  2swrd1eqwrdeq  12450  ccats1swrdeq  12465  swrdccatin12lem3  12483  2swrd2eqwrdeq  12655  shftfib  12663  shftfn  12664  2shfti  12671  sqrlem3  12836  resqrex  12842  cau3lem  12944  caubnd2  12947  caubnd  12948  sqreu  12950  limsuple  13058  limsupval2  13060  rlim2  13076  climi  13090  rlimi  13093  ello12r  13097  ello1mpt  13101  ello1d  13103  lo1bdd2  13104  lo1bddrp  13105  elo12r  13108  o1lo1  13117  rlimclim1  13125  rlimdm  13131  climeu  13135  climmo  13137  2clim  13152  o1co  13166  o1compt  13167  addcn2  13173  mulcn2  13175  reccn2  13176  cn1lem  13177  rlimo1  13196  lo1add  13206  lo1mul  13207  climsup  13249  caucvgrlem  13252  caucvgb  13259  summo  13296  zsum  13297  fsum  13299  o1fsum  13378  climcnds  13416  supcvg  13420  rpnnen2lem4  13602  rpnnen  13611  ruclem2  13616  ruclem12  13625  sqr2irr  13633  dvdsabsb  13654  0dvds  13655  dvdsle  13680  alzdvds  13685  dvdsext  13686  fzo0dvdseq  13688  divalglem10  13708  bitsinv1lem  13739  sadadd3  13759  bitsuz  13772  gcdval  13794  gcdcllem1  13797  gcdcllem2  13798  gcddvds  13801  bezoutlem4  13827  dvdsgcd  13829  dvdssq  13846  isprm  13867  isprm2lem  13872  dvdsprm  13887  coprmdvds2  13891  isprm6  13897  exprmfct  13898  maxprmfct  13901  prmexpb  13905  prmfac1  13906  rpexp  13908  iserodd  14004  pceu  14015  pczpre  14016  pcdiv  14021  pcdvdsb  14037  pcmpt  14056  pcmptdvds  14058  prmpwdvds  14067  unbenlem  14071  infpnlem2  14074  infpn2  14076  prmreclem1  14079  prmreclem2  14080  prmreclem3  14081  prmreclem5  14083  prmreclem6  14084  vdwlem9  14152  vdwlem10  14153  vdwlem13  14156  ramz  14188  imasleval  14581  mreexexlem3d  14686  mreexexlem4d  14687  mreexexd  14688  prslem  15203  drsdirfi  15210  posi  15222  posasymb  15224  pleval2  15237  plttr  15242  pltletr  15243  pospo  15245  lubprop  15258  lublecllem  15260  glbprop  15271  glble  15272  joinlem  15283  joinle  15286  meetval2lem  15294  meetlem  15297  isglbd  15389  lubl  15392  lubun  15395  pospropd  15406  poslubmo  15418  posglbmo  15419  poslubd  15420  tsrlin  15491  tsrlemax  15492  letsr  15499  eqgen  15836  odeq  16157  odmulg  16161  pgpssslw  16217  sylow2alem2  16221  sylow2blem3  16225  efgval2  16325  efgsfo  16340  efgred  16349  efgredeu  16353  efgcpbllemb  16356  gexex  16439  cyggex2  16477  pgpfaclem1  16687  pgpfaclem2  16688  pgpfaclem3  16689  ablfaclem2  16692  ablfaclem3  16693  lidldvgen  17443  psrass1lem  17553  psrmulval  17563  mplmonmul  17650  opsrtoslem2  17673  coe1mul2  17830  coe1tmmul2fv  17839  coe1pwmulfv  17841  zndvds  18091  znleval  18096  islinds  18347  ordtbaslem  18908  ordtbas2  18911  ordtopn1  18914  mnfnei  18941  ordtt1  19099  ordthauslem  19103  ordthmeolem  19490  trust  19920  ucncn  19976  imasdsf1olem  20064  comet  20204  stdbdxmet  20206  stdbdmet  20207  stdbdmopn  20209  metcnpi  20235  metcnpi2  20236  metcnpi3  20237  ngptgp  20338  nlmvscnlem1  20383  nrginvrcnlem  20387  nmogelb  20411  nmolb  20412  nghmcn  20440  xrsxmet  20502  icccmplem2  20516  icccmplem3  20517  reconnlem2  20520  xrge0tsms  20527  xmetdcn2  20530  metdsf  20540  metdsge  20541  metdscn  20548  metnrmlem1a  20550  addcnlem  20556  cncfi  20586  elcncf1di  20587  iccpnfhmeo  20633  xrhmeo  20634  cnllycmp  20644  evth  20647  ipcnlem1  20873  lmmcvg  20888  cfili  20895  cncmet  20949  minveclem1  21027  minveclem3b  21031  minveclem6  21037  pmltpclem1  21048  pmltpc  21050  ivthlem2  21052  ivthlem3  21053  cniccbdd  21061  ovolmge0  21076  ovolgelb  21079  ovolctb  21089  ovolunlem1  21096  ovoliunlem1  21101  ovoliun  21104  ovoliun2  21105  ovolshftlem1  21108  ovolscalem1  21112  ovolicc2lem3  21118  ovolicc2lem5  21120  ovolicc2  21121  voliunlem3  21149  ioombl1lem1  21155  ioombl1lem4  21158  uniioombllem2  21179  uniioombllem6  21184  volcn  21202  ismbfd  21234  mbfsup  21258  mbfinf  21259  mbflimsup  21260  itg1ge0  21280  itg1climres  21308  mbfi1fseqlem5  21313  itg2val  21322  itg2const  21334  itg2const2  21335  itg2seq  21336  itg2monolem1  21344  itg2i1fseq  21349  itg2i1fseq2  21350  itg2addlem  21352  itg2cnlem1  21355  itg2cnlem2  21356  itg2cn  21357  isibl  21359  ditgeq2  21440  dveflem  21567  dvferm1lem  21572  rolle  21578  c1lip1  21585  lhop1  21602  dvfsumlem2  21615  dvfsumlem4  21617  dvfsumrlim  21619  dvfsum2  21622  mdegmullem  21665  deg1leb  21682  deg1lt  21685  dvdsq1p  21748  plyeq0lem  21794  dgrco  21858  plydivex  21879  quotcan  21891  aannenlem1  21910  aannenlem2  21911  ulmi  21967  ulmcaulem  21975  ulmcau  21976  ulmbdd  21979  ulmdvlem3  21983  mtestbdd  21986  iblulm  21988  psercnlem1  22006  psercn  22007  abelthlem8  22020  sinhalfpilem  22041  logltb  22164  cxple2  22258  cxpcn3lem  22301  isosctrlem1  22332  leibpilem2  22452  cxploglim  22487  scvxcvx  22495  emcllem6  22510  ftalem3  22528  vmaval  22567  isppw2  22569  muval  22586  fsumdvdscom  22641  dvdsflf1o  22643  dvdsflsumcom  22644  musum  22647  muinv  22649  ppiublem1  22657  chtub  22667  logfac2  22672  bpos1lem  22737  bposlem9  22747  lgsdir  22785  lgsne0  22788  lgsqr  22801  lgsquadlem1  22809  lgsquadlem2  22810  lgsquadlem3  22811  2sqlem6  22824  2sqlem8  22827  2sqlem10  22829  dchrisumlema  22853  dchrisumlem2  22855  dchrisumlem3  22856  dchrvmasumiflem1  22866  dchrisum0fval  22870  dchrisum0ff  22872  dchrisum0flblem2  22874  logsqvma2  22908  pntrsumbnd2  22932  pntrlog2bndlem1  22942  pntpbnd1  22951  pntpbnd2  22952  pntibndlem2  22956  pntibndlem3  22957  pntibnd  22958  pntlemi  22969  pntlem3  22974  pntlemp  22975  pntleml  22976  pnt3  22977  tgldimor  23073  axcontlem10  23354  uhgra0v  23379  usgra0v  23425  usgra1v  23443  cusgraexg  23512  sizeusglecusg  23529  usgramaxsize  23530  3v3e3cycl1  23665  4cycl4v4e  23687  4cycl4dv  23688  gxval  23880  vacn  24224  nmcvcn  24225  smcnlem  24227  nmobndi  24310  blocni  24340  ubthlem1  24406  ubthlem2  24407  ubthlem3  24408  minvecolem1  24410  minvecolem5  24417  minvecolem6  24418  htthlem  24454  norm3lemt  24689  hcaucvg  24723  hlimconvi  24728  hlim2  24729  chlimi  24772  hlimreui  24777  occl  24842  cmbr3  25146  cmcm  25152  cmcm3  25153  lecm  25155  cnopc  25452  cnfnc  25469  0cnop  25518  0cnfn  25519  idcnop  25520  nmopun  25553  nmcexi  25565  lnconi  25572  branmfn  25644  opsqrlem1  25679  pjnmopi  25687  pjnormssi  25707  stge1i  25777  strlem5  25794  hstrlem5  25802  mddmd2  25848  csmdsymi  25873  cvmd  25875  ela  25878  cvbr4i  25906  chirredlem3  25931  chirredlem4  25932  chirred  25934  atmd  25938  mdsym  25951  mddmdin0i  25970  cdj1i  25972  cdj3i  25980  fmptcof2  26113  isoun  26131  xrge0infss  26187  ishashinf  26219  tleile  26256  toslublem  26262  tosglblem  26264  omndadd  26303  sgnsval  26325  isinftm  26332  xrnarchi  26335  archirng  26339  archiexdiv  26341  archiabllem1a  26342  archiabllem2a  26345  archiabl  26349  xrge0tsmsd  26387  orngmul  26405  isarchiofld  26419  ordtconlem1  26488  rge0scvg  26513  qqhcn  26554  qqhucn  26555  esumcst  26648  esumpinfval  26656  esumpcvgval  26661  esumcvg  26669  oddpwdc  26871  eulerpartlems  26877  eulerpartlemf  26887  eulerpartlemt  26888  eulerpartlemr  26891  eulerpartlemgvv  26893  eulerpartlemn  26898  dstfrvunirn  26991  ballotlemfcc  27010  sgnmulsgp  27067  signslema  27097  lgamgulmlem4  27152  lgamgulmlem5  27153  lgambdd  27157  subfacp1lem1  27201  relexpindlem  27475  relexpind  27476  rtrclreclem.trans  27482  ntrivcvgn0  27547  ntrivcvgmullem  27550  prodmo  27583  zprod  27584  fprod  27588  fprodntriv  27589  dfpo2  27699  fundmpss  27711  funbreq  27716  dfpred3g  27770  predbrg  27781  poseq  27848  wzel  27895  wsuclem  27896  wsuclb  27899  nodenselem4  27959  nodenselem5  27960  nodense  27964  nocvxminlem  27965  nobndup  27975  nofulllem5  27981  brtxp  28045  brtxp2  28046  brpprod3a  28051  elfix  28068  sscoid  28078  elfuns  28080  fnsingle  28084  brimageg  28092  fnimage  28094  brdomaing  28100  brrangeg  28101  funpartlem  28107  fvtransport  28197  fin2so  28554  supaddc  28555  supadd  28556  heicant  28564  mblfinlem1  28566  mblfinlem2  28567  mblfinlem3  28568  mblfinlem4  28569  ismblfin  28570  itg2addnclem  28581  itg2addnc  28584  itg2gt0cn  28585  ftc1anclem7  28611  ftc1anclem8  28612  ftc1anc  28613  trer  28649  elicc3  28650  finminlem  28651  nn0prpwlem  28655  nn0prpw  28656  fnessref  28703  refssfne  28704  fnemeet2  28726  filnetlem3  28739  frinfm  28767  fdc1  28780  nninfnub  28785  equivbnd  28827  heibor1lem  28846  heiborlem8  28855  iccbnd  28877  lzenom  29246  fphpdo  29294  rencldnfilem  29297  irrapxlem5  29305  irrapxlem6  29306  pellexlem3  29310  pellqrex  29358  pellfundre  29360  pellfundge  29361  pellfundlb  29363  pellfundglb  29364  monotoddzz  29422  oddcomabszz  29423  zindbi  29425  jm2.22  29482  jm2.23  29483  rpnnen3  29519  ttac  29523  fnwe2lem2  29542  aomclem8  29552  hbtlem1  29617  hbtlem5  29622  ubelsupr  29880  climinf  29917  stoweidlem14  29947  stoweidlem29  29962  stoweidlem31  29964  stoweidlem34  29967  stoweidlem49  29982  wallispilem3  30000  stirlinglem13  30019  stirlinglem14  30020  rlimdmafv  30221  wrdlen1  30388  ccats1swrdeqrex  30397  wwlknred  30493  wwlkextwrd  30498  wwlkextfun  30499  wwlkextinj  30500  clwlkisclwwlklem1  30587  clwwlkf1  30596  clwwlkext2edg  30602  wwlkext2clwwlk  30603  wwlksubclwwlk  30604  clwlkfclwwlk  30655  clwlkfoclwwlk  30656  wwlkextproplem2  30699  wwlkextproplem3  30700  rusgranumwlks  30712  isfrgra  30720  vdgfrgragt2  30758  frgrawopreglem2  30776  clwwlkextfrlem1  30807  numclwwlkovf2ex  30817  friendshipgt3  30852  ssnn0fi  30884  rabssnn0fi  30885  0rngnnzr  30916  suppssfz  30924  gsummptnn0fz  30947  gsummptnn0fzfv  30949  gsummoncoe1  30985  ply1mulgsumlem2  30987  ldepsnlinc  31157  pmatcoe1fsupp  31167  mp2pm2mplem4  31264  fvmptnn04ifa  31304  fvmptnn04ifd  31307  chfacffsupp  31310  chfacfscmul0  31312  chfacfpmmul0  31316  cpmadumatpoly  31338  cayleyhamilton  31345  cayleyhamiltonALT  31346  bnj1185  32087  bnj602  32208  bnj1228  32302  bj-seex  32726  oposlem  33133  lub0N  33140  glb0N  33144  omllaw  33194  cvrval  33220  cvrnbtwn  33222  cvrnbtwn2  33226  cvrnbtwn3  33227  cvrcon3b  33228  cvrnbtwn4  33230  cvrcmp  33234  isat  33237  atnlt  33264  atlex  33267  cvlexch1  33279  cvlexchb1  33281  cvlatexch1  33287  glbconN  33327  2llnne2N  33358  cvratlem  33371  cvrat4  33393  ps-1  33427  3at  33440  islln  33456  llncmp  33472  llnnlt  33473  islpln  33480  islpln5  33485  lvolex3N  33488  lplncmp  33512  lplnexllnN  33514  lplnnlt  33515  islvol  33523  lvoli3  33527  islvol5  33529  lvolcmp  33567  lvolnltN  33568  dalem-cly  33621  dalem44  33666  pmapval  33707  pmapglbx  33719  lncvrelatN  33731  lncmp  33733  cdlemblem  33743  llnexchb2  33819  lautle  34034  lautcvr  34042  ldilset  34059  ltrnset  34068  trlset  34111  cdlemc4  34144  cdleme11dN  34212  cdleme20k  34269  cdleme21ct  34279  cdleme22b  34291  tendoex  34925  diafval  34982  diaval  34983  dicfval  35126  dihfval  35182  dihglblem2N  35245