Theorem breq2 4291

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 4055	. . 3 |- ( A = B -> <. C , A >. = <. C , B >. )
2	1	eleq1d 2504	. 2 |- ( A = B -> ( <. C , A >. e. R <-> <. C , B >. e. R ) )
3		df-br 4288	. 2 |- ( C R A <-> <. C , A >. e. R )
4		df-br 4288	. 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 1369   e. wcel 1756   <.cop 3878   class class class wbr 4287

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-rab 2719  df-v 2969  df-dif 3326  df-un 3328  df-in 3330  df-ss 3337  df-nul 3633  df-if 3787  df-sn 3873  df-pr 3875  df-op 3879  df-br 4288

This theorem is referenced by:  breq12  4292  breq2i  4295  breq2d  4299  nbrne1  4304  pocl  4643  swopolem  4645  swopo  4646  solin  4659  sotric  4662  sotrieq  4663  isso2i  4668  somo  4670  seex  4678  frirr  4692  fr2nr  4693  frminex  4695  wereu2  4712  vtoclr  4878  posn  4902  frsn  4904  brcog  5001  brcogw  5003  opelcnvg  5014  dfdmf  5028  breldmg  5040  dfrnf  5073  dmcoss  5094  resieq  5116  dfres2  5153  elimag  5168  elrelimasn  5188  elimasn  5189  asymref2  5210  intirr  5211  poirr2  5217  sotri3  5223  poltletr  5228  soltmin  5232  dffun3  5424  dffun6f  5427  fun11  5478  brprcneu  5679  fv3  5698  tz6.12c  5704  tz6.12i  5705  funbrfv  5725  fnbrfvb  5727  funfv2f  5755  dffv2  5759  fvopab5  5790  fndmdif  5802  dff3  5851  fmptco  5871  foeqcnvco  5993  isorel  6012  soisores  6013  soisoi  6014  isocnv  6016  isotr  6022  isopolem  6031  isosolem  6033  f1oiso  6037  f1oiso2  6038  caovordig  6263  caovordg  6265  caovord  6269  caofrss  6348  caoftrn  6350  fr3nr  6386  dfwe2  6388  f1oweALT  6556  frxp  6677  poxp  6679  suppimacnv  6696  tposoprab  6776  ertr  7108  ecopovsym  7194  ecopovtrn  7195  th3qlem2  7199  domeng  7316  eqeng  7335  snfi  7382  sbth  7423  domunsn  7453  domssex  7464  nneneq  7486  php2  7488  onfin  7493  1sdom  7507  unxpdom  7512  isinf  7518  fineqvlem  7519  pssnn  7523  ssnnfi  7524  dif1enOLD  7536  dif1en  7537  findcard  7543  findcard2  7544  findcard3  7547  frfi  7549  fisupg  7552  nnsdomg  7563  unfi  7571  fiint  7580  mapfien2  7650  supmo  7694  eqsup  7698  supub  7701  suplub  7702  suplub2  7703  supmaxlem  7706  fisup2g  7708  fisupcl  7709  suppr  7710  supisolem  7712  supisoex  7713  ordtypecbv  7723  ordtypelem3  7726  ordtypelem6  7729  ordtypelem7  7730  ordtypelem9  7732  wemaplem1  7752  wemaplem2  7753  harval  7769  wemapwe  7920  wemapweOLD  7921  r111  7974  cardf2  8105  isnum2  8107  cardval3  8114  cardnueq0  8126  carden2a  8128  cardlim  8134  isinffi  8154  onsdom  8158  harval2  8159  cardmin2  8160  ondomen  8199  alephnbtwn  8233  alephinit  8257  aceq3lem  8282  infmap2  8379  cfslb2n  8429  sornom  8438  isfin4  8458  fin23lem26  8486  fin23lem27  8489  fin1a2lem11  8571  fin1a2lem12  8572  hsmex  8593  domtriomlem  8603  dominf  8606  zorn2lem2  8658  zorn2lem7  8663  zorn2g  8664  axdclem  8680  axdc  8682  fodomg  8684  brdom7disj  8690  brdom6disj  8691  cardmin  8720  ficard  8721  alephval2  8728  dominfac  8729  cfpwsdom  8740  gchi  8783  fpwwe2lem12  8800  fpwwe2lem13  8801  canthp1lem1  8811  canthp1lem2  8812  pwfseqlem4a  8820  pwfseqlem4  8821  elina  8846  winainflem  8852  eltskg  8909  rankcf  8936  indpi  9068  nqereu  9090  nsmallnq  9138  ltbtwnnq  9139  ltrnq  9140  prcdnq  9154  genpcd  9167  genpnmax  9168  ltaddpr2  9196  ltexprlem4  9200  prlem936  9208  reclem2pr  9209  reclem3pr  9210  supexpr  9215  ltsosr  9253  ltasr  9259  recexsrlem  9262  mulgt0sr  9264  map2psrpr  9269  supsrlem  9270  axpre-lttri  9324  axpre-lttrn  9325  axpre-ltadd  9326  axpre-mulgt0  9327  axpre-sup  9328  ltletr  9458  letr  9460  ltne  9463  eqle  9469  dedekind  9525  dedekindle  9526  ltordlem  9857  elimgt0  10157  elimge0  10158  squeeze0  10227  fimaxre2  10270  lbreu  10272  lble  10274  sup2  10278  infm3  10281  suprlub  10284  supmul1  10287  supmullem1  10288  supmullem2  10289  supmul  10290  infmrcl  10301  infmrgelb  10302  nn2ge  10339  nnge1  10340  nnsub  10352  nominpos  10553  nnunb  10567  elnnnn0b  10616  nn0sub  10622  peano2uz2  10721  peano5uzi  10722  dfuzi  10724  uzind  10725  uzind3  10727  uzindOLD  10728  uzind3OLD  10729  eluz1  10857  uzind4  10904  uzwo  10909  uzwoOLD  10910  nnwof  10913  indstr2  10925  ublbneg  10931  zsupss  10936  uzsupss  10939  uzwo3  10940  zmin  10941  zmax  10942  zbtwnre  10943  rebtwnz  10944  rpnnen1lem1  10971  rpnnen1lem2  10972  rpnnen1lem3  10973  rpnnen1lem4  10974  rpnnen1lem5  10975  reexALT  10977  elrp  10985  mnfltxr  11099  nn0pnfge0  11104  xrltnsym  11106  xrlttri  11108  xrlttr  11109  xrltletr  11123  xrletr  11124  ngtmnft  11131  xrltmin  11146  xrlemin  11148  ifle  11159  z2ge  11160  qbtwnre  11161  qbtwnxr  11162  qextlt  11165  qextle  11166  xltnegi  11178  xmullem2  11220  xmulasslem2  11237  xmulasslem  11240  xlemul1a  11243  xrsupexmnf  11259  xrsupsslem  11261  xrinfmsslem  11262  xrub  11266  supxrpnf  11273  supxrunb1  11274  supxrunb2  11275  ixxval  11300  elixx1  11301  elioo2  11333  iccid  11337  icc0  11340  iccsupr  11374  repos  11378  supicc  11425  supiccub  11426  supicclub  11427  fzval  11431  elfz1  11434  flval  11636  flval2  11654  flval3  11655  dfceil2  11672  uzsup  11694  modid2  11727  fsequb  11789  serge0  11852  expge0  11892  expge1  11893  facdiv  12055  facwordi  12057  hashkf  12097  hashnnn0genn0  12106  hashv01gt1  12108  hashneq0  12124  hashdom  12134  hashnn0n0nn  12145  hashss  12158  hashgt12el  12165  hashgt12el2  12166  hashge2el2dif  12176  brfi1uzind  12211  fstwrdne0  12256  wrdeqswrdlsw  12335  2swrdeqwrdeq  12339  2swrd1eqwrdeq  12340  ccats1swrdeq  12355  swrdccatin12lem3  12373  2swrd2eqwrdeq  12545  shftfib  12553  shftfn  12554  2shfti  12561  sqrlem3  12726  resqrex  12732  cau3lem  12834  caubnd2  12837  caubnd  12838  sqreu  12840  limsuple  12948  limsupval2  12950  rlim2  12966  climi  12980  rlimi  12983  ello12r  12987  ello1mpt  12991  ello1d  12993  lo1bdd2  12994  lo1bddrp  12995  elo12r  12998  o1lo1  13007  rlimclim1  13015  rlimdm  13021  climeu  13025  climmo  13027  2clim  13042  o1co  13056  o1compt  13057  addcn2  13063  mulcn2  13065  reccn2  13066  cn1lem  13067  rlimo1  13086  lo1add  13096  lo1mul  13097  climsup  13139  caucvgrlem  13142  caucvgb  13149  summo  13186  zsum  13187  fsum  13189  o1fsum  13268  climcnds  13306  supcvg  13310  rpnnen2lem4  13492  rpnnen  13501  ruclem2  13506  ruclem12  13515  sqr2irr  13523  dvdsabsb  13544  0dvds  13545  dvdsle  13570  alzdvds  13575  dvdsext  13576  fzo0dvdseq  13578  divalglem10  13598  bitsinv1lem  13629  sadadd3  13649  bitsuz  13662  gcdval  13684  gcdcllem1  13687  gcdcllem2  13688  gcddvds  13691  bezoutlem4  13717  dvdsgcd  13719  dvdssq  13736  isprm  13757  isprm2lem  13762  dvdsprm  13777  coprmdvds2  13781  isprm6  13787  exprmfct  13788  maxprmfct  13791  prmexpb  13795  prmfac1  13796  rpexp  13798  iserodd  13894  pceu  13905  pczpre  13906  pcdiv  13911  pcdvdsb  13927  pcmpt  13946  pcmptdvds  13948  prmpwdvds  13957  unbenlem  13961  infpnlem2  13964  infpn2  13966  prmreclem1  13969  prmreclem2  13970  prmreclem3  13971  prmreclem5  13973  prmreclem6  13974  vdwlem9  14042  vdwlem10  14043  vdwlem13  14046  ramz  14078  imasleval  14471  mreexexlem3d  14576  mreexexlem4d  14577  mreexexd  14578  prslem  15093  drsdirfi  15100  posi  15112  posasymb  15114  pleval2  15127  plttr  15132  pltletr  15133  pospo  15135  lubprop  15148  lublecllem  15150  glbprop  15161  glble  15162  joinlem  15173  joinle  15176  meetval2lem  15184  meetlem  15187  isglbd  15279  lubl  15282  lubun  15285  pospropd  15296  poslubmo  15308  posglbmo  15309  poslubd  15310  tsrlin  15381  tsrlemax  15382  letsr  15389  eqgen  15725  odeq  16044  odmulg  16048  pgpssslw  16104  sylow2alem2  16108  sylow2blem3  16112  efgval2  16212  efgsfo  16227  efgred  16236  efgredeu  16240  efgcpbllemb  16243  gexex  16326  cyggex2  16364  pgpfaclem1  16570  pgpfaclem2  16571  pgpfaclem3  16572  ablfaclem2  16575  ablfaclem3  16576  lidldvgen  17314  psrass1lem  17424  psrmulval  17434  mplmonmul  17520  opsrtoslem2  17541  coe1mul2  17698  coe1tmmul2fv  17706  coe1pwmulfv  17708  zndvds  17957  znleval  17962  islinds  18213  ordtbaslem  18767  ordtbas2  18770  ordtopn1  18773  mnfnei  18800  ordtt1  18958  ordthauslem  18962  ordthmeolem  19349  trust  19779  ucncn  19835  imasdsf1olem  19923  comet  20063  stdbdxmet  20065  stdbdmet  20066  stdbdmopn  20068  metcnpi  20094  metcnpi2  20095  metcnpi3  20096  ngptgp  20197  nlmvscnlem1  20242  nrginvrcnlem  20246  nmogelb  20270  nmolb  20271  nghmcn  20299  xrsxmet  20361  icccmplem2  20375  icccmplem3  20376  reconnlem2  20379  xrge0tsms  20386  xmetdcn2  20389  metdsf  20399  metdsge  20400  metdscn  20407  metnrmlem1a  20409  addcnlem  20415  cncfi  20445  elcncf1di  20446  iccpnfhmeo  20492  xrhmeo  20493  cnllycmp  20503  evth  20506  ipcnlem1  20732  lmmcvg  20747  cfili  20754  cncmet  20808  minveclem1  20886  minveclem3b  20890  minveclem6  20896  pmltpclem1  20907  pmltpc  20909  ivthlem2  20911  ivthlem3  20912  cniccbdd  20920  ovolmge0  20935  ovolgelb  20938  ovolctb  20948  ovolunlem1  20955  ovoliunlem1  20960  ovoliun  20963  ovoliun2  20964  ovolshftlem1  20967  ovolscalem1  20971  ovolicc2lem3  20977  ovolicc2lem5  20979  ovolicc2  20980  voliunlem3  21008  ioombl1lem1  21014  ioombl1lem4  21017  uniioombllem2  21038  uniioombllem6  21043  volcn  21061  ismbfd  21093  mbfsup  21117  mbfinf  21118  mbflimsup  21119  itg1ge0  21139  itg1climres  21167  mbfi1fseqlem5  21172  itg2val  21181  itg2const  21193  itg2const2  21194  itg2seq  21195  itg2monolem1  21203  itg2i1fseq  21208  itg2i1fseq2  21209  itg2addlem  21211  itg2cnlem1  21214  itg2cnlem2  21215  itg2cn  21216  isibl  21218  ditgeq2  21299  dveflem  21426  dvferm1lem  21431  rolle  21437  c1lip1  21444  lhop1  21461  dvfsumlem2  21474  dvfsumlem4  21476  dvfsumrlim  21478  dvfsum2  21481  mdegmullem  21524  deg1leb  21541  deg1lt  21544  dvdsq1p  21607  plyeq0lem  21653  dgrco  21717  plydivex  21738  quotcan  21750  aannenlem1  21769  aannenlem2  21770  ulmi  21826  ulmcaulem  21834  ulmcau  21835  ulmbdd  21838  ulmdvlem3  21842  mtestbdd  21845  iblulm  21847  psercnlem1  21865  psercn  21866  abelthlem8  21879  sinhalfpilem  21900  logltb  22023  cxple2  22117  cxpcn3lem  22160  isosctrlem1  22191  leibpilem2  22311  cxploglim  22346  scvxcvx  22354  emcllem6  22369  ftalem3  22387  vmaval  22426  isppw2  22428  muval  22445  fsumdvdscom  22500  dvdsflf1o  22502  dvdsflsumcom  22503  musum  22506  muinv  22508  ppiublem1  22516  chtub  22526  logfac2  22531  bpos1lem  22596  bposlem9  22606  lgsdir  22644  lgsne0  22647  lgsqr  22660  lgsquadlem1  22668  lgsquadlem2  22669  lgsquadlem3  22670  2sqlem6  22683  2sqlem8  22686  2sqlem10  22688  dchrisumlema  22712  dchrisumlem2  22714  dchrisumlem3  22715  dchrvmasumiflem1  22725  dchrisum0fval  22729  dchrisum0ff  22731  dchrisum0flblem2  22733  logsqvma2  22767  pntrsumbnd2  22791  pntrlog2bndlem1  22801  pntpbnd1  22810  pntpbnd2  22811  pntibndlem2  22815  pntibndlem3  22816  pntibnd  22817  pntlemi  22828  pntlem3  22833  pntlemp  22834  pntleml  22835  pnt3  22836  tgldimor  22930  axcontlem10  23170  uhgra0v  23195  usgra0v  23241  usgra1v  23259  cusgraexg  23328  sizeusglecusg  23345  usgramaxsize  23346  3v3e3cycl1  23481  4cycl4v4e  23503  4cycl4dv  23504  gxval  23696  vacn  24040  nmcvcn  24041  smcnlem  24043  nmobndi  24126  blocni  24156  ubthlem1  24222  ubthlem2  24223  ubthlem3  24224  minvecolem1  24226  minvecolem5  24233  minvecolem6  24234  htthlem  24270  norm3lemt  24505  hcaucvg  24539  hlimconvi  24544  hlim2  24545  chlimi  24588  hlimreui  24593  occl  24658  cmbr3  24962  cmcm  24968  cmcm3  24969  lecm  24971  cnopc  25268  cnfnc  25285  0cnop  25334  0cnfn  25335  idcnop  25336  nmopun  25369  nmcexi  25381  lnconi  25388  branmfn  25460  opsqrlem1  25495  pjnmopi  25503  pjnormssi  25523  stge1i  25593  strlem5  25610  hstrlem5  25618  mddmd2  25664  csmdsymi  25689  cvmd  25691  ela  25694  cvbr4i  25722  chirredlem3  25747  chirredlem4  25748  chirred  25750  atmd  25754  mdsym  25767  mddmdin0i  25786  cdj1i  25788  cdj3i  25796  fmptcof2  25930  isoun  25948  xrge0infss  26004  ishashinf  26036  tleile  26073  toslublem  26079  tosglblem  26081  omndadd  26120  sgnsval  26142  isinftm  26149  xrnarchi  26152  archirng  26156  archiexdiv  26158  archiabllem1a  26159  archiabllem2a  26162  archiabl  26166  xrge0tsmsd  26204  orngmul  26222  isarchiofld  26236  ordtconlem1  26306  rge0scvg  26331  qqhcn  26372  qqhucn  26373  esumcst  26466  esumpinfval  26474  esumpcvgval  26479  esumcvg  26487  oddpwdc  26689  eulerpartlems  26695  eulerpartlemf  26705  eulerpartlemt  26706  eulerpartlemr  26709  eulerpartlemgvv  26711  eulerpartlemn  26716  dstfrvunirn  26809  ballotlemfcc  26828  sgnmulsgp  26885  signslema  26915  lgamgulmlem4  26970  lgamgulmlem5  26971  lgambdd  26975  subfacp1lem1  27019  relexpindlem  27292  relexpind  27293  rtrclreclem.trans  27299  ntrivcvgn0  27364  ntrivcvgmullem  27367  prodmo  27400  zprod  27401  fprod  27405  fprodntriv  27406  dfpo2  27516  fundmpss  27528  funbreq  27533  dfpred3g  27587  predbrg  27598  poseq  27665  wzel  27712  wsuclem  27713  wsuclb  27716  nodenselem4  27776  nodenselem5  27777  nodense  27781  nocvxminlem  27782  nobndup  27792  nofulllem5  27798  brtxp  27862  brtxp2  27863  brpprod3a  27868  elfix  27885  sscoid  27895  elfuns  27897  fnsingle  27901  brimageg  27909  fnimage  27911  brdomaing  27917  brrangeg  27918  funpartlem  27924  fvtransport  28014  fin2so  28369  supaddc  28370  supadd  28371  heicant  28379  mblfinlem1  28381  mblfinlem2  28382  mblfinlem3  28383  mblfinlem4  28384  ismblfin  28385  itg2addnclem  28396  itg2addnc  28399  itg2gt0cn  28400  ftc1anclem7  28426  ftc1anclem8  28427  ftc1anc  28428  trer  28464  elicc3  28465  finminlem  28466  nn0prpwlem  28470  nn0prpw  28471  fnessref  28518  refssfne  28519  fnemeet2  28541  filnetlem3  28554  frinfm  28582  fdc1  28595  nninfnub  28600  equivbnd  28642  heibor1lem  28661  heiborlem8  28670  iccbnd  28692  lzenom  29061  fphpdo  29109  rencldnfilem  29112  irrapxlem5  29120  irrapxlem6  29121  pellexlem3  29125  pellqrex  29173  pellfundre  29175  pellfundge  29176  pellfundlb  29178  pellfundglb  29179  monotoddzz  29237  oddcomabszz  29238  zindbi  29240  jm2.22  29297  jm2.23  29298  rpnnen3  29334  ttac  29338  fnwe2lem2  29357  aomclem8  29367  hbtlem1  29432  hbtlem5  29437  ubelsupr  29695  climinf  29732  stoweidlem14  29762  stoweidlem29  29777  stoweidlem31  29779  stoweidlem34  29782  stoweidlem49  29797  wallispilem3  29815  stirlinglem13  29834  stirlinglem14  29835  rlimdmafv  30036  wrdlen1  30203  ccats1swrdeqrex  30212  wwlknred  30308  wwlkextwrd  30313  wwlkextfun  30314  wwlkextinj  30315  clwlkisclwwlklem1  30402  clwwlkf1  30411  clwwlkext2edg  30417  wwlkext2clwwlk  30418  wwlksubclwwlk  30419  clwlkfclwwlk  30470  clwlkfoclwwlk  30471  wwlkextproplem2  30514  wwlkextproplem3  30515  rusgranumwlks  30527  isfrgra  30535  vdgfrgragt2  30573  frgrawopreglem2  30591  clwwlkextfrlem1  30622  numclwwlkovf2ex  30632  friendshipgt3  30667  ssnn0fi  30697  rabssnn0fi  30698  0rngnnzr  30729  pmatcollpw2lem  30820  ldepsnlinc  30939  bnj1185  31674  bnj602  31795  bnj1228  31889  bj-seex  32275  oposlem  32667  lub0N  32674  glb0N  32678  omllaw  32728  cvrval  32754  cvrnbtwn  32756  cvrnbtwn2  32760  cvrnbtwn3  32761  cvrcon3b  32762  cvrnbtwn4  32764  cvrcmp  32768  isat  32771  atnlt  32798  atlex  32801  cvlexch1  32813  cvlexchb1  32815  cvlatexch1  32821  glbconN  32861  2llnne2N  32892  cvratlem  32905  cvrat4  32927  ps-1  32961  3at  32974  islln  32990  llncmp  33006  llnnlt  33007  islpln  33014  islpln5  33019  lvolex3N  33022  lplncmp  33046  lplnexllnN  33048  lplnnlt  33049  islvol  33057  lvoli3  33061  islvol5  33063  lvolcmp  33101  lvolnltN  33102  dalem-cly  33155  dalem44  33200  pmapval  33241  pmapglbx  33253  lncvrelatN  33265  lncmp  33267  cdlemblem  33277  llnexchb2  33353  lautle  33568  lautcvr  33576  ldilset  33593  ltrnset  33602  trlset  33645  cdlemc4  33678  cdleme11dN  33746  cdleme20k  33803  cdleme21ct  33813  cdleme22b  33825  tendoex  34459  diafval  34516  diaval  34517  dicfval  34660  dihfval  34716  dihglblem2N  34779