Theorem breq2 4176

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 3945	. . 3 |- ( A = B -> <. C , A >. = <. C , B >. )
2	1	eleq1d 2470	. 2 |- ( A = B -> ( <. C , A >. e. R <-> <. C , B >. e. R ) )
3		df-br 4173	. 2 |- ( C R A <-> <. C , A >. e. R )
4		df-br 4173	. 2 |- ( C R B <-> <. C , B >. e. R )
5	2, 3, 4	3bitr4g 280	1 |- ( A = B -> ( C R A <-> C R B ) )

Syntax hints:   -> wi 4   <-> wb 177   = wceq 1649   e. wcel 1721   <.cop 3777   class class class wbr 4172

This theorem is referenced by:  breq12  4177  breq2i  4180  breq2d  4184  nbrne1  4189  pocl  4470  swopolem  4472  swopo  4473  solin  4486  sotric  4489  sotrieq  4490  isso2i  4495  somo  4497  seex  4505  frirr  4519  fr2nr  4520  frminex  4522  wereu2  4539  fr3nr  4719  dfwe2  4721  vtoclr  4881  posn  4905  frsn  4907  brcog  4998  brcogw  5000  opelcnvg  5011  dfdmf  5023  breldmg  5034  dfrnf  5067  dmcoss  5094  resieq  5115  dfres2  5152  elimag  5166  elrelimasn  5187  elimasn  5188  asymref2  5210  intirr  5211  poirr2  5217  sotri3  5223  poltletr  5228  soltmin  5232  dffun3  5424  dffun6f  5427  fun11  5475  brprcneu  5680  fv3  5703  tz6.12c  5709  tz6.12i  5710  funbrfv  5724  fnbrfvb  5726  funfv2f  5751  dffv2  5755  fndmdif  5793  dff3  5841  fmptco  5860  foeqcnvco  5986  isorel  6005  soisores  6006  soisoi  6007  isocnv  6009  isotr  6015  isopolem  6024  isosolem  6026  f1oiso  6030  f1oiso2  6031  f1oweALT  6033  caovordig  6211  caovordg  6213  caovord  6217  caofrss  6296  caoftrn  6298  frxp  6415  poxp  6417  tposoprab  6474  fvopab5  6493  ertr  6879  ecopovsym  6965  ecopovtrn  6966  th3qlem2  6970  domeng  7081  eqeng  7100  snfi  7146  sbth  7186  domunsn  7216  domssex  7227  nneneq  7249  php2  7251  onfin  7256  1sdom  7270  unxpdom  7275  isinf  7281  fineqvlem  7282  pssnn  7286  ssnnfi  7287  dif1enOLD  7299  dif1en  7300  findcard  7306  findcard2  7307  findcard3  7309  frfi  7311  fisupg  7314  nnsdomg  7325  unfi  7333  fiint  7342  supmo  7413  eqsup  7417  supub  7420  suplub  7421  suplub2  7422  supmaxlem  7425  fisup2g  7427  fisupcl  7428  suppr  7429  supisolem  7431  supisoex  7432  ordtypecbv  7442  ordtypelem3  7445  ordtypelem6  7448  ordtypelem7  7449  ordtypelem9  7451  wemaplem1  7471  wemaplem2  7472  harval  7486  wemapwe  7610  r111  7657  cardf2  7786  isnum2  7788  cardval3  7795  cardnueq0  7807  carden2a  7809  cardlim  7815  isinffi  7835  onsdom  7839  harval2  7840  cardmin2  7841  ondomen  7874  alephnbtwn  7908  alephinit  7932  aceq3lem  7957  infmap2  8054  cfslb2n  8104  sornom  8113  isfin4  8133  fin23lem26  8161  fin23lem27  8164  fin1a2lem11  8246  fin1a2lem12  8247  hsmex  8268  domtriomlem  8278  dominf  8281  zorn2lem2  8333  zorn2lem7  8338  zorn2g  8339  axdclem  8355  axdc  8357  fodomg  8359  brdom7disj  8365  brdom6disj  8366  cardmin  8395  ficard  8396  alephval2  8403  dominfac  8404  cfpwsdom  8415  gchi  8455  fpwwe2lem12  8472  fpwwe2lem13  8473  canthp1lem1  8483  canthp1lem2  8484  pwfseqlem4a  8492  pwfseqlem4  8493  elina  8518  winainflem  8524  eltskg  8581  rankcf  8608  indpi  8740  nqereu  8762  nsmallnq  8810  ltbtwnnq  8811  ltrnq  8812  prcdnq  8826  genpcd  8839  genpnmax  8840  ltaddpr2  8868  ltexprlem4  8872  prlem936  8880  reclem2pr  8881  reclem3pr  8882  supexpr  8887  ltsosr  8925  ltasr  8931  recexsrlem  8934  mulgt0sr  8936  map2psrpr  8941  supsrlem  8942  axpre-lttri  8996  axpre-lttrn  8997  axpre-ltadd  8998  axpre-mulgt0  8999  axpre-sup  9000  ltletr  9122  letr  9123  ltne  9126  eqle  9132  ltordlem  9508  elimgt0  9802  elimge0  9803  squeeze0  9869  fimaxre2  9912  lbreu  9914  lble  9916  sup2  9920  infm3  9923  suprlub  9926  supmul1  9929  supmullem1  9930  supmullem2  9931  supmul  9932  infmrcl  9943  infmrgelb  9944  nn2ge  9981  nnge1  9982  nnsub  9994  nominpos  10160  nnunb  10173  elnnnn0b  10220  nn0sub  10226  peano2uz2  10313  peano5uzi  10314  dfuzi  10316  uzind  10317  uzind3  10319  uzindOLD  10320  uzind3OLD  10321  eluz1  10448  uzind4  10490  uzwo  10495  uzwoOLD  10496  nnwof  10499  indstr2  10510  ublbneg  10516  zsupss  10521  uzsupss  10524  uzwo3  10525  zmin  10526  zmax  10527  zbtwnre  10528  rebtwnz  10529  rpnnen1lem1  10556  rpnnen1lem2  10557  rpnnen1lem3  10558  rpnnen1lem4  10559  rpnnen1lem5  10560  reexALT  10562  elrp  10570  mnfltxr  10680  nn0pnfge0  10684  xrltnsym  10686  xrlttri  10688  xrlttr  10689  xrltletr  10703  xrletr  10704  ngtmnft  10711  xrltmin  10726  xrlemin  10728  ifle  10739  z2ge  10740  qbtwnre  10741  qbtwnxr  10742  qextlt  10745  qextle  10746  xltnegi  10758  xmullem2  10800  xmulasslem2  10817  xmulasslem  10820  xlemul1a  10823  xrsupexmnf  10839  xrsupsslem  10841  xrinfmsslem  10842  xrub  10846  supxrpnf  10853  supxrunb1  10854  supxrunb2  10855  ixxval  10880  elixx1  10881  elioo2  10913  iccid  10917  icc0  10920  iccsupr  10953  repos  10957  fzval  11001  elfz1  11004  flval  11158  flval2  11176  flval3  11177  uzsup  11199  modid2  11226  fsequb  11269  serge0  11332  expge0  11371  expge1  11372  facdiv  11533  facwordi  11535  hashkf  11575  hashnnn0genn0  11582  hashv01gt1  11584  hashdom  11608  hashnn0n0nn  11619  hashgt12el  11637  hashgt12el2  11638  brfi1uzind  11670  shftfib  11842  shftfn  11843  2shfti  11850  sqrlem3  12005  resqrex  12011  cau3lem  12113  caubnd2  12116  caubnd  12117  sqreu  12119  limsuple  12227  limsupval2  12229  rlim2  12245  climi  12259  rlimi  12262  ello12r  12266  ello1mpt  12270  ello1d  12272  lo1bdd2  12273  lo1bddrp  12274  elo12r  12277  o1lo1  12286  rlimclim1  12294  rlimdm  12300  climeu  12304  climmo  12306  2clim  12321  o1co  12335  o1compt  12336  addcn2  12342  mulcn2  12344  reccn2  12345  cn1lem  12346  rlimo1  12365  lo1add  12375  lo1mul  12376  climsup  12418  caucvgrlem  12421  caucvgb  12428  summo  12466  zsum  12467  fsum  12469  o1fsum  12547  climcnds  12586  supcvg  12590  rpnnen2lem4  12772  rpnnen  12781  ruclem2  12786  ruclem12  12795  sqr2irr  12803  dvdsabsb  12824  0dvds  12825  dvdsle  12850  alzdvds  12854  dvdsext  12855  fzo0dvdseq  12857  divalglem10  12877  bitsinv1lem  12908  sadadd3  12928  bitsuz  12941  gcdval  12963  gcdcllem1  12966  gcdcllem2  12967  gcddvds  12970  bezoutlem4  12996  dvdsgcd  12998  dvdssq  13015  isprm  13036  isprm2lem  13041  dvdsprm  13054  coprmdvds2  13058  isprm6  13064  exprmfct  13065  maxprmfct  13068  prmexpb  13072  prmfac1  13073  rpexp  13075  iserodd  13164  pceu  13175  pczpre  13176  pcdiv  13181  pcdvdsb  13197  pcmpt  13216  pcmptdvds  13218  prmpwdvds  13227  unbenlem  13231  infpnlem2  13234  infpn2  13236  prmreclem1  13239  prmreclem2  13240  prmreclem3  13241  prmreclem5  13243  prmreclem6  13244  vdwlem9  13312  vdwlem10  13313  vdwlem13  13316  ramz  13348  imasleval  13721  mreexexlem3d  13826  mreexexlem4d  13827  mreexexd  13828  prslem  14343  drsdirfi  14350  posi  14362  posasymb  14364  pleval2  14377  plttr  14382  pltletr  14383  pospo  14385  lubprop  14392  lubid  14394  glbprop  14397  glble  14398  joinlem  14402  joinle  14405  meetval2  14408  meetlem  14409  isglbd  14499  lubl  14502  lubun  14505  pospropd  14516  poslubmo  14528  poslubd  14529  tsrlin  14606  tsrlemax  14607  spwmo  14613  spwpr4  14618  letsr  14627  eqgen  14948  odeq  15143  odmulg  15147  pgpssslw  15203  sylow2alem2  15207  sylow2blem3  15211  efgval2  15311  efgsfo  15326  efgred  15335  efgredeu  15339  efgcpbllemb  15342  gexex  15423  cyggex2  15461  pgpfaclem1  15594  pgpfaclem2  15595  pgpfaclem3  15596  ablfaclem2  15599  ablfaclem3  15600  lidldvgen  16281  psrass1lem  16397  psrmulval  16405  mplmonmul  16482  opsrtoslem2  16500  coe1mul2  16617  coe1tmmul2fv  16625  coe1pwmulfv  16627  zndvds  16785  znleval  16790  ordtbaslem  17206  ordtbas2  17209  ordtopn1  17212  mnfnei  17239  ordtt1  17397  ordthauslem  17401  ordthmeolem  17786  trust  18212  ucncn  18268  imasdsf1olem  18356  comet  18496  stdbdxmet  18498  stdbdmet  18499  stdbdmopn  18501  metcnpi  18527  metcnpi2  18528  metcnpi3  18529  ngptgp  18630  nlmvscnlem1  18675  nrginvrcnlem  18679  nmogelb  18703  nmolb  18704  nghmcn  18732  xrsxmet  18793  icccmplem2  18807  icccmplem3  18808  reconnlem2  18811  xrge0tsms  18818  xmetdcn2  18821  metdsf  18831  metdsge  18832  metdscn  18839  metnrmlem1a  18841  addcnlem  18847  cncfi  18877  elcncf1di  18878  iccpnfhmeo  18923  xrhmeo  18924  cnllycmp  18934  evth  18937  ipcnlem1  19152  lmmcvg  19167  cfili  19174  cncmet  19228  minveclem1  19278  minveclem3b  19282  minveclem6  19288  pmltpclem1  19298  pmltpc  19300  ivthlem2  19302  ivthlem3  19303  cniccbdd  19311  ovolmge0  19326  ovolgelb  19329  ovolctb  19339  ovolunlem1  19346  ovoliunlem1  19351  ovoliun  19354  ovoliun2  19355  ovolshftlem1  19358  ovolscalem1  19362  ovolicc2lem3  19368  ovolicc2lem5  19370  ovolicc2  19371  voliunlem3  19399  ioombl1lem1  19405  ioombl1lem4  19408  uniioombllem2  19428  uniioombllem6  19433  volcn  19451  ismbfd  19485  mbfsup  19509  mbfinf  19510  mbflimsup  19511  itg1ge0  19531  itg1climres  19559  mbfi1fseqlem5  19564  itg2val  19573  itg2const  19585  itg2const2  19586  itg2seq  19587  itg2monolem1  19595  itg2i1fseq  19600  itg2i1fseq2  19601  itg2addlem  19603  itg2cnlem1  19606  itg2cnlem2  19607  itg2cn  19608  isibl  19610  ditgeq2  19689  dveflem  19816  dvferm1lem  19821  rolle  19827  c1lip1  19834  lhop1  19851  dvfsumlem2  19864  dvfsumlem4  19866  dvfsumrlim  19868  dvfsum2  19871  mdegmullem  19954  deg1leb  19971  deg1lt  19973  dvdsq1p  20036  plyeq0lem  20082  dgrco  20146  plydivex  20167  quotcan  20179  aannenlem1  20198  aannenlem2  20199  ulmi  20255  ulmcaulem  20263  ulmcau  20264  ulmbdd  20267  ulmdvlem3  20271  mtestbdd  20274  iblulm  20276  psercnlem1  20294  psercn  20295  abelthlem8  20308  sinhalfpilem  20327  logltb  20447  cxple2  20541  cxpcn3lem  20584  isosctrlem1  20615  leibpilem2  20734  cxploglim  20769  scvxcvx  20777  emcllem6  20792  ftalem3  20810  vmaval  20849  isppw2  20851  muval  20868  fsumdvdscom  20923  dvdsflf1o  20925  dvdsflsumcom  20926  musum  20929  muinv  20931  ppiublem1  20939  chtub  20949  logfac2  20954  bpos1lem  21019  bposlem9  21029  lgsdir  21067  lgsne0  21070  lgsqr  21083  lgsquadlem1  21091  lgsquadlem2  21092  lgsquadlem3  21093  2sqlem6  21106  2sqlem8  21109  2sqlem10  21111  dchrisumlema  21135  dchrisumlem2  21137  dchrisumlem3  21138  dchrvmasumiflem1  21148  dchrisum0fval  21152  dchrisum0ff  21154  dchrisum0flblem2  21156  logsqvma2  21190  pntrsumbnd2  21214  pntrlog2bndlem1  21224  pntpbnd1  21233  pntpbnd2  21234  pntibndlem2  21238  pntibndlem3  21239  pntibnd  21240  pntlemi  21251  pntlem3  21256  pntlemp  21257  pntleml  21258  pnt3  21259  uhgra0v  21298  usgra0v  21344  usgra1v  21362  cusgraexg  21431  sizeusglecusg  21448  usgramaxsize  21449  3v3e3cycl1  21584  4cycl4v4e  21606  4cycl4dv  21607  gxval  21799  vacn  22143  nmcvcn  22144  smcnlem  22146  nmobndi  22229  blocni  22259  ubthlem1  22325  ubthlem2  22326  ubthlem3  22327  minvecolem1  22329  minvecolem5  22336  minvecolem6  22337  htthlem  22373  norm3lemt  22607  hcaucvg  22641  hlimconvi  22646  hlim2  22647  chlimi  22690  hlimreui  22695  occl  22759  cmbr3  23063  cmcm  23069  cmcm3  23070  lecm  23072  cnopc  23369  cnfnc  23386  0cnop  23435  0cnfn  23436  idcnop  23437  nmopun  23470  nmcexi  23482  lnconi  23489  branmfn  23561  opsqrlem1  23596  pjnmopi  23604  pjnormssi  23624  stge1i  23694  strlem5  23711  hstrlem5  23719  mddmd2  23765  csmdsymi  23790  cvmd  23792  ela  23795  cvbr4i  23823  chirredlem3  23848  chirredlem4  23849  chirred  23851  atmd  23855  mdsym  23868  mddmdin0i  23887  cdj1i  23889  cdj3i  23897  fmptcof2  24029  isoun  24042  ishashinf  24112  tleile  24142  toslub  24144  tosglb  24145  xrge0tsmsd  24176  ofldadd  24191  ofldmul  24192  isinftm  24204  xrnarchi  24207  rge0scvg  24288  qqhcn  24328  qqhucn  24329  esumcst  24408  esumpinfval  24416  esumpcvgval  24421  esumcvg  24429  dstfrvunirn  24685  ballotlemfcc  24704  lgamgulmlem4  24769  lgamgulmlem5  24770  lgambdd  24774  subfacp1lem1  24818  relexpindlem  25092  relexpind  25093  rtrclreclem.trans  25099  dedekind  25140  dedekindle  25141  ntrivcvgn0  25179  ntrivcvgmullem  25182  prodmo  25215  zprod  25216  fprod  25220  fprodntriv  25221  dfpo2  25326  fundmpss  25336  funbreq  25341  predbrg  25400  poseq  25467  nodenselem4  25552  nodenselem5  25553  nodense  25557  nocvxminlem  25558  nobndup  25568  nofulllem5  25574  brtxp  25634  brtxp2  25635  brpprod3a  25640  elfix  25657  dffun10  25667  fnsingle  25672  brimageg  25680  fnimage  25682  brdomaing  25688  brrangeg  25689  brcup  25692  brcap  25693  funpartlem  25695  axcontlem10  25816  fvtransport  25870  supaddc  26137  supadd  26138  mblfinlem  26143  mblfinlem2  26144  mblfinlem3  26145  ismblfin  26146  itg2addnclem  26155  itg2addnc  26158  itg2gt0cn  26159  trer  26209  elicc3  26210  finminlem  26211  nn0prpwlem  26215  nn0prpw  26216  fnessref  26263  refssfne  26264  fnemeet2  26286  filnetlem3  26299  frinfm  26327  fdc1  26340  nninfnub  26345  equivbnd  26389  heibor1lem  26408  heiborlem8  26417  iccbnd  26439  lzenom  26718  fphpdo  26768  rencldnfilem  26771  irrapxlem5  26779  irrapxlem6  26780  pellexlem3  26784  pellqrex  26832  pellfundre  26834  pellfundge  26835  pellfundlb  26837  pellfundglb  26838  monotoddzz  26896  oddcomabszz  26897  zindbi  26899  jm2.22  26956  jm2.23  26957  rpnnen3  26993  ttac  26997  fnwe2lem2  27016  aomclem8  27027  islinds  27147  hbtlem1  27195  hbtlem5  27200  xrltneNEW  27524  ubelsupr  27558  climinf  27599  stoweidlem14  27630  stoweidlem29  27645  stoweidlem31  27647  stoweidlem34  27650  stoweidlem49  27665  wallispilem3  27683  stirlinglem13  27702  stirlinglem14  27703  rlimdmafv  27908  swrdccatin12lem4  28025  swrdccat3  28029  isfrgra  28094  vdgfrgragt2  28132  frgrawopreglem2  28148  bnj1185  28871  bnj602  28992  bnj1228  29086  lubunNEW  29456  oposlem  29666  lub0N  29672  glb0N  29676  omllaw  29726  cvrval  29752  cvrnbtwn  29754  cvrnbtwn2  29758  cvrnbtwn3  29759  cvrcon3b  29760  cvrnbtwn4  29762  cvrcmp  29766  isat  29769  atnlt  29796  atlex  29799  cvlexch1  29811  cvlexchb1  29813  cvlatexch1  29819  glbconN  29859  2llnne2N  29890  cvratlem  29903  cvrat4  29925  ps-1  29959  3at  29972  islln  29988  llncmp  30004  llnnlt  30005  islpln  30012  islpln5  30017  lvolex3N  30020  lplncmp  30044  lplnexllnN  30046  lplnnlt  30047  islvol  30055  lvoli3  30059  islvol5  30061  lvolcmp  30099  lvolnltN  30100  dalem-cly  30153  dalem44  30198  pmapval  30239  pmapglbx  30251  lncvrelatN  30263  lncmp  30265  cdlemblem  30275  llnexchb2  30351  lautle  30566  lautcvr  30574  ldilset  30591  ltrnset  30600  trlset  30643  cdlemc4  30676  cdleme11dN  30744  cdleme20k  30801  cdleme21ct  30811  cdleme22b  30823  tendoex  31457  diafval  31514  diaval  31515  dicfval  31658  dihfval  31714  dihglblem2N  31777

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 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385

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 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-rab 2675  df-v 2918  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-sn 3780  df-pr 3781  df-op 3783  df-br 4173