Theorem breq2 4284

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 4048	. . 3 |- ( A = B -> <. C , A >. = <. C , B >. )
2	1	eleq1d 2499	. 2 |- ( A = B -> ( <. C , A >. e. R <-> <. C , B >. e. R ) )
3		df-br 4281	. 2 |- ( C R A <-> <. C , A >. e. R )
4		df-br 4281	. 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 1362   e. wcel 1755   <.cop 3871   class class class wbr 4280

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-rab 2714  df-v 2964  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-nul 3626  df-if 3780  df-sn 3866  df-pr 3868  df-op 3872  df-br 4281

This theorem is referenced by:  breq12  4285  breq2i  4288  breq2d  4292  nbrne1  4297  pocl  4635  swopolem  4637  swopo  4638  solin  4651  sotric  4654  sotrieq  4655  isso2i  4660  somo  4662  seex  4670  frirr  4684  fr2nr  4685  frminex  4687  wereu2  4704  vtoclr  4870  posn  4894  frsn  4896  brcog  4993  brcogw  4995  opelcnvg  5006  dfdmf  5020  breldmg  5032  dfrnf  5065  dmcoss  5086  resieq  5108  dfres2  5146  elimag  5161  elrelimasn  5181  elimasn  5182  asymref2  5203  intirr  5204  poirr2  5210  sotri3  5216  poltletr  5221  soltmin  5225  dffun3  5417  dffun6f  5420  fun11  5471  brprcneu  5672  fv3  5691  tz6.12c  5697  tz6.12i  5698  funbrfv  5718  fnbrfvb  5720  funfv2f  5748  dffv2  5752  fvopab5  5783  fndmdif  5795  dff3  5844  fmptco  5863  foeqcnvco  5985  isorel  6004  soisores  6005  soisoi  6006  isocnv  6008  isotr  6014  isopolem  6023  isosolem  6025  f1oiso  6029  f1oiso2  6030  caovordig  6257  caovordg  6259  caovord  6263  caofrss  6342  caoftrn  6344  fr3nr  6380  dfwe2  6382  f1oweALT  6550  frxp  6671  poxp  6673  suppimacnv  6690  tposoprab  6770  ertr  7104  ecopovsym  7190  ecopovtrn  7191  th3qlem2  7195  domeng  7312  eqeng  7331  snfi  7378  sbth  7419  domunsn  7449  domssex  7460  nneneq  7482  php2  7484  onfin  7489  1sdom  7503  unxpdom  7508  isinf  7514  fineqvlem  7515  pssnn  7519  ssnnfi  7520  dif1enOLD  7532  dif1en  7533  findcard  7539  findcard2  7540  findcard3  7543  frfi  7545  fisupg  7548  nnsdomg  7559  unfi  7567  fiint  7576  mapfien2  7646  supmo  7690  eqsup  7694  supub  7697  suplub  7698  suplub2  7699  supmaxlem  7702  fisup2g  7704  fisupcl  7705  suppr  7706  supisolem  7708  supisoex  7709  ordtypecbv  7719  ordtypelem3  7722  ordtypelem6  7725  ordtypelem7  7726  ordtypelem9  7728  wemaplem1  7748  wemaplem2  7749  harval  7765  wemapwe  7916  wemapweOLD  7917  r111  7970  cardf2  8101  isnum2  8103  cardval3  8110  cardnueq0  8122  carden2a  8124  cardlim  8130  isinffi  8150  onsdom  8154  harval2  8155  cardmin2  8156  ondomen  8195  alephnbtwn  8229  alephinit  8253  aceq3lem  8278  infmap2  8375  cfslb2n  8425  sornom  8434  isfin4  8454  fin23lem26  8482  fin23lem27  8485  fin1a2lem11  8567  fin1a2lem12  8568  hsmex  8589  domtriomlem  8599  dominf  8602  zorn2lem2  8654  zorn2lem7  8659  zorn2g  8660  axdclem  8676  axdc  8678  fodomg  8680  brdom7disj  8686  brdom6disj  8687  cardmin  8716  ficard  8717  alephval2  8724  dominfac  8725  cfpwsdom  8736  gchi  8779  fpwwe2lem12  8796  fpwwe2lem13  8797  canthp1lem1  8807  canthp1lem2  8808  pwfseqlem4a  8816  pwfseqlem4  8817  elina  8842  winainflem  8848  eltskg  8905  rankcf  8932  indpi  9064  nqereu  9086  nsmallnq  9134  ltbtwnnq  9135  ltrnq  9136  prcdnq  9150  genpcd  9163  genpnmax  9164  ltaddpr2  9192  ltexprlem4  9196  prlem936  9204  reclem2pr  9205  reclem3pr  9206  supexpr  9211  ltsosr  9249  ltasr  9255  recexsrlem  9258  mulgt0sr  9260  map2psrpr  9265  supsrlem  9266  axpre-lttri  9320  axpre-lttrn  9321  axpre-ltadd  9322  axpre-mulgt0  9323  axpre-sup  9324  ltletr  9454  letr  9456  ltne  9459  eqle  9465  dedekind  9521  dedekindle  9522  ltordlem  9853  elimgt0  10153  elimge0  10154  squeeze0  10223  fimaxre2  10266  lbreu  10268  lble  10270  sup2  10274  infm3  10277  suprlub  10280  supmul1  10283  supmullem1  10284  supmullem2  10285  supmul  10286  infmrcl  10297  infmrgelb  10298  nn2ge  10335  nnge1  10336  nnsub  10348  nominpos  10549  nnunb  10563  elnnnn0b  10612  nn0sub  10618  peano2uz2  10717  peano5uzi  10718  dfuzi  10720  uzind  10721  uzind3  10723  uzindOLD  10724  uzind3OLD  10725  eluz1  10853  uzind4  10900  uzwo  10905  uzwoOLD  10906  nnwof  10909  indstr2  10921  ublbneg  10927  zsupss  10932  uzsupss  10935  uzwo3  10936  zmin  10937  zmax  10938  zbtwnre  10939  rebtwnz  10940  rpnnen1lem1  10967  rpnnen1lem2  10968  rpnnen1lem3  10969  rpnnen1lem4  10970  rpnnen1lem5  10971  reexALT  10973  elrp  10981  mnfltxr  11095  nn0pnfge0  11100  xrltnsym  11102  xrlttri  11104  xrlttr  11105  xrltletr  11119  xrletr  11120  ngtmnft  11127  xrltmin  11142  xrlemin  11144  ifle  11155  z2ge  11156  qbtwnre  11157  qbtwnxr  11158  qextlt  11161  qextle  11162  xltnegi  11174  xmullem2  11216  xmulasslem2  11233  xmulasslem  11236  xlemul1a  11239  xrsupexmnf  11255  xrsupsslem  11257  xrinfmsslem  11258  xrub  11262  supxrpnf  11269  supxrunb1  11270  supxrunb2  11271  ixxval  11296  elixx1  11297  elioo2  11329  iccid  11333  icc0  11336  iccsupr  11370  repos  11374  supicc  11420  supiccub  11421  supicclub  11422  fzval  11426  elfz1  11429  flval  11628  flval2  11646  flval3  11647  dfceil2  11664  uzsup  11686  modid2  11719  fsequb  11781  serge0  11844  expge0  11884  expge1  11885  facdiv  12047  facwordi  12049  hashkf  12089  hashnnn0genn0  12098  hashv01gt1  12100  hashneq0  12116  hashdom  12126  hashnn0n0nn  12137  hashss  12150  hashgt12el  12157  hashgt12el2  12158  hashge2el2dif  12168  brfi1uzind  12203  fstwrdne0  12248  wrdeqswrdlsw  12327  2swrdeqwrdeq  12331  2swrd1eqwrdeq  12332  ccats1swrdeq  12347  swrdccatin12lem3  12365  2swrd2eqwrdeq  12537  shftfib  12545  shftfn  12546  2shfti  12553  sqrlem3  12718  resqrex  12724  cau3lem  12826  caubnd2  12829  caubnd  12830  sqreu  12832  limsuple  12940  limsupval2  12942  rlim2  12958  climi  12972  rlimi  12975  ello12r  12979  ello1mpt  12983  ello1d  12985  lo1bdd2  12986  lo1bddrp  12987  elo12r  12990  o1lo1  12999  rlimclim1  13007  rlimdm  13013  climeu  13017  climmo  13019  2clim  13034  o1co  13048  o1compt  13049  addcn2  13055  mulcn2  13057  reccn2  13058  cn1lem  13059  rlimo1  13078  lo1add  13088  lo1mul  13089  climsup  13131  caucvgrlem  13134  caucvgb  13141  summo  13178  zsum  13179  fsum  13181  o1fsum  13259  climcnds  13297  supcvg  13301  rpnnen2lem4  13483  rpnnen  13492  ruclem2  13497  ruclem12  13506  sqr2irr  13514  dvdsabsb  13535  0dvds  13536  dvdsle  13561  alzdvds  13566  dvdsext  13567  fzo0dvdseq  13569  divalglem10  13589  bitsinv1lem  13620  sadadd3  13640  bitsuz  13653  gcdval  13675  gcdcllem1  13678  gcdcllem2  13679  gcddvds  13682  bezoutlem4  13708  dvdsgcd  13710  dvdssq  13727  isprm  13748  isprm2lem  13753  dvdsprm  13768  coprmdvds2  13772  isprm6  13778  exprmfct  13779  maxprmfct  13782  prmexpb  13786  prmfac1  13787  rpexp  13789  iserodd  13885  pceu  13896  pczpre  13897  pcdiv  13902  pcdvdsb  13918  pcmpt  13937  pcmptdvds  13939  prmpwdvds  13948  unbenlem  13952  infpnlem2  13955  infpn2  13957  prmreclem1  13960  prmreclem2  13961  prmreclem3  13962  prmreclem5  13964  prmreclem6  13965  vdwlem9  14033  vdwlem10  14034  vdwlem13  14037  ramz  14069  imasleval  14462  mreexexlem3d  14567  mreexexlem4d  14568  mreexexd  14569  prslem  15084  drsdirfi  15091  posi  15103  posasymb  15105  pleval2  15118  plttr  15123  pltletr  15124  pospo  15126  lubprop  15139  lublecllem  15141  glbprop  15152  glble  15153  joinlem  15164  joinle  15167  meetval2lem  15175  meetlem  15178  isglbd  15270  lubl  15273  lubun  15276  pospropd  15287  poslubmo  15299  posglbmo  15300  poslubd  15301  tsrlin  15372  tsrlemax  15373  letsr  15380  eqgen  15714  odeq  16033  odmulg  16037  pgpssslw  16093  sylow2alem2  16097  sylow2blem3  16101  efgval2  16201  efgsfo  16216  efgred  16225  efgredeu  16229  efgcpbllemb  16232  gexex  16315  cyggex2  16353  pgpfaclem1  16556  pgpfaclem2  16557  pgpfaclem3  16558  ablfaclem2  16561  ablfaclem3  16562  lidldvgen  17259  psrass1lem  17381  psrmulval  17391  mplmonmul  17477  opsrtoslem2  17498  coe1mul2  17621  coe1tmmul2fv  17629  coe1pwmulfv  17631  zndvds  17824  znleval  17829  islinds  18080  ordtbaslem  18634  ordtbas2  18637  ordtopn1  18640  mnfnei  18667  ordtt1  18825  ordthauslem  18829  ordthmeolem  19216  trust  19646  ucncn  19702  imasdsf1olem  19790  comet  19930  stdbdxmet  19932  stdbdmet  19933  stdbdmopn  19935  metcnpi  19961  metcnpi2  19962  metcnpi3  19963  ngptgp  20064  nlmvscnlem1  20109  nrginvrcnlem  20113  nmogelb  20137  nmolb  20138  nghmcn  20166  xrsxmet  20228  icccmplem2  20242  icccmplem3  20243  reconnlem2  20246  xrge0tsms  20253  xmetdcn2  20256  metdsf  20266  metdsge  20267  metdscn  20274  metnrmlem1a  20276  addcnlem  20282  cncfi  20312  elcncf1di  20313  iccpnfhmeo  20359  xrhmeo  20360  cnllycmp  20370  evth  20373  ipcnlem1  20599  lmmcvg  20614  cfili  20621  cncmet  20675  minveclem1  20753  minveclem3b  20757  minveclem6  20763  pmltpclem1  20774  pmltpc  20776  ivthlem2  20778  ivthlem3  20779  cniccbdd  20787  ovolmge0  20802  ovolgelb  20805  ovolctb  20815  ovolunlem1  20822  ovoliunlem1  20827  ovoliun  20830  ovoliun2  20831  ovolshftlem1  20834  ovolscalem1  20838  ovolicc2lem3  20844  ovolicc2lem5  20846  ovolicc2  20847  voliunlem3  20875  ioombl1lem1  20881  ioombl1lem4  20884  uniioombllem2  20905  uniioombllem6  20910  volcn  20928  ismbfd  20960  mbfsup  20984  mbfinf  20985  mbflimsup  20986  itg1ge0  21006  itg1climres  21034  mbfi1fseqlem5  21039  itg2val  21048  itg2const  21060  itg2const2  21061  itg2seq  21062  itg2monolem1  21070  itg2i1fseq  21075  itg2i1fseq2  21076  itg2addlem  21078  itg2cnlem1  21081  itg2cnlem2  21082  itg2cn  21083  isibl  21085  ditgeq2  21166  dveflem  21293  dvferm1lem  21298  rolle  21304  c1lip1  21311  lhop1  21328  dvfsumlem2  21341  dvfsumlem4  21343  dvfsumrlim  21345  dvfsum2  21348  mdegmullem  21434  deg1leb  21451  deg1lt  21454  dvdsq1p  21517  plyeq0lem  21563  dgrco  21627  plydivex  21648  quotcan  21660  aannenlem1  21679  aannenlem2  21680  ulmi  21736  ulmcaulem  21744  ulmcau  21745  ulmbdd  21748  ulmdvlem3  21752  mtestbdd  21755  iblulm  21757  psercnlem1  21775  psercn  21776  abelthlem8  21789  sinhalfpilem  21810  logltb  21933  cxple2  22027  cxpcn3lem  22070  isosctrlem1  22101  leibpilem2  22221  cxploglim  22256  scvxcvx  22264  emcllem6  22279  ftalem3  22297  vmaval  22336  isppw2  22338  muval  22355  fsumdvdscom  22410  dvdsflf1o  22412  dvdsflsumcom  22413  musum  22416  muinv  22418  ppiublem1  22426  chtub  22436  logfac2  22441  bpos1lem  22506  bposlem9  22516  lgsdir  22554  lgsne0  22557  lgsqr  22570  lgsquadlem1  22578  lgsquadlem2  22579  lgsquadlem3  22580  2sqlem6  22593  2sqlem8  22596  2sqlem10  22598  dchrisumlema  22622  dchrisumlem2  22624  dchrisumlem3  22625  dchrvmasumiflem1  22635  dchrisum0fval  22639  dchrisum0ff  22641  dchrisum0flblem2  22643  logsqvma2  22677  pntrsumbnd2  22701  pntrlog2bndlem1  22711  pntpbnd1  22720  pntpbnd2  22721  pntibndlem2  22725  pntibndlem3  22726  pntibnd  22727  pntlemi  22738  pntlem3  22743  pntlemp  22744  pntleml  22745  pnt3  22746  tgldimor  22837  axcontlem10  23042  uhgra0v  23067  usgra0v  23113  usgra1v  23131  cusgraexg  23200  sizeusglecusg  23217  usgramaxsize  23218  3v3e3cycl1  23353  4cycl4v4e  23375  4cycl4dv  23376  gxval  23568  vacn  23912  nmcvcn  23913  smcnlem  23915  nmobndi  23998  blocni  24028  ubthlem1  24094  ubthlem2  24095  ubthlem3  24096  minvecolem1  24098  minvecolem5  24105  minvecolem6  24106  htthlem  24142  norm3lemt  24377  hcaucvg  24411  hlimconvi  24416  hlim2  24417  chlimi  24460  hlimreui  24465  occl  24530  cmbr3  24834  cmcm  24840  cmcm3  24841  lecm  24843  cnopc  25140  cnfnc  25157  0cnop  25206  0cnfn  25207  idcnop  25208  nmopun  25241  nmcexi  25253  lnconi  25260  branmfn  25332  opsqrlem1  25367  pjnmopi  25375  pjnormssi  25395  stge1i  25465  strlem5  25482  hstrlem5  25490  mddmd2  25536  csmdsymi  25561  cvmd  25563  ela  25566  cvbr4i  25594  chirredlem3  25619  chirredlem4  25620  chirred  25622  atmd  25626  mdsym  25639  mddmdin0i  25658  cdj1i  25660  cdj3i  25668  fmptcof2  25803  isoun  25821  ishashinf  25908  tleile  25945  toslublem  25951  tosglblem  25953  omndadd  25993  sgnsval  26015  isinftm  26022  xrnarchi  26025  archirng  26029  archiexdiv  26031  archiabllem1a  26032  archiabllem2a  26035  archiabl  26039  xrge0tsmsd  26106  orngmul  26124  isarchiofld  26138  ordtconlem1  26208  rge0scvg  26233  qqhcn  26274  qqhucn  26275  esumcst  26368  esumpinfval  26376  esumpcvgval  26381  esumcvg  26389  oddpwdc  26585  eulerpartlems  26591  eulerpartlemf  26601  eulerpartlemt  26602  eulerpartlemr  26605  eulerpartlemgvv  26607  eulerpartlemn  26612  dstfrvunirn  26705  ballotlemfcc  26724  sgnmulsgp  26781  signslema  26811  lgamgulmlem4  26866  lgamgulmlem5  26867  lgambdd  26871  subfacp1lem1  26915  relexpindlem  27188  relexpind  27189  rtrclreclem.trans  27195  ntrivcvgn0  27260  ntrivcvgmullem  27263  prodmo  27296  zprod  27297  fprod  27301  fprodntriv  27302  dfpo2  27412  fundmpss  27424  funbreq  27429  dfpred3g  27483  predbrg  27494  poseq  27561  wzel  27608  wsuclem  27609  wsuclb  27612  nodenselem4  27672  nodenselem5  27673  nodense  27677  nocvxminlem  27678  nobndup  27688  nofulllem5  27694  brtxp  27758  brtxp2  27759  brpprod3a  27764  elfix  27781  sscoid  27791  elfuns  27793  fnsingle  27797  brimageg  27805  fnimage  27807  brdomaing  27813  brrangeg  27814  funpartlem  27820  fvtransport  27910  fin2so  28260  supaddc  28261  supadd  28262  heicant  28270  mblfinlem1  28272  mblfinlem2  28273  mblfinlem3  28274  mblfinlem4  28275  ismblfin  28276  itg2addnclem  28287  itg2addnc  28290  itg2gt0cn  28291  ftc1anclem7  28317  ftc1anclem8  28318  ftc1anc  28319  trer  28355  elicc3  28356  finminlem  28357  nn0prpwlem  28361  nn0prpw  28362  fnessref  28409  refssfne  28410  fnemeet2  28432  filnetlem3  28445  frinfm  28473  fdc1  28486  nninfnub  28491  equivbnd  28533  heibor1lem  28552  heiborlem8  28561  iccbnd  28583  lzenom  28953  fphpdo  29001  rencldnfilem  29004  irrapxlem5  29012  irrapxlem6  29013  pellexlem3  29017  pellqrex  29065  pellfundre  29067  pellfundge  29068  pellfundlb  29070  pellfundglb  29071  monotoddzz  29129  oddcomabszz  29130  zindbi  29132  jm2.22  29189  jm2.23  29190  rpnnen3  29226  ttac  29230  fnwe2lem2  29249  aomclem8  29259  hbtlem1  29324  hbtlem5  29329  ubelsupr  29587  climinf  29625  stoweidlem14  29655  stoweidlem29  29670  stoweidlem31  29672  stoweidlem34  29675  stoweidlem49  29690  wallispilem3  29708  stirlinglem13  29727  stirlinglem14  29728  rlimdmafv  29929  wrdlen1  30096  ccats1swrdeqrex  30105  wwlknred  30201  wwlkextwrd  30206  wwlkextfun  30207  wwlkextinj  30208  clwlkisclwwlklem1  30295  clwwlkf1  30304  clwwlkext2edg  30310  wwlkext2clwwlk  30311  wwlksubclwwlk  30312  clwlkfclwwlk  30363  clwlkfoclwwlk  30364  wwlkextproplem2  30407  wwlkextproplem3  30408  rusgranumwlks  30420  isfrgra  30428  vdgfrgragt2  30466  frgrawopreglem2  30484  clwwlkextfrlem1  30515  numclwwlkovf2ex  30525  friendshipgt3  30560  0rngnnzr  30609  ldepsnlinc  30759  bnj1185  31489  bnj602  31610  bnj1228  31704  bj-seex  32013  oposlem  32400  lub0N  32407  glb0N  32411  omllaw  32461  cvrval  32487  cvrnbtwn  32489  cvrnbtwn2  32493  cvrnbtwn3  32494  cvrcon3b  32495  cvrnbtwn4  32497  cvrcmp  32501  isat  32504  atnlt  32531  atlex  32534  cvlexch1  32546  cvlexchb1  32548  cvlatexch1  32554  glbconN  32594  2llnne2N  32625  cvratlem  32638  cvrat4  32660  ps-1  32694  3at  32707  islln  32723  llncmp  32739  llnnlt  32740  islpln  32747  islpln5  32752  lvolex3N  32755  lplncmp  32779  lplnexllnN  32781  lplnnlt  32782  islvol  32790  lvoli3  32794  islvol5  32796  lvolcmp  32834  lvolnltN  32835  dalem-cly  32888  dalem44  32933  pmapval  32974  pmapglbx  32986  lncvrelatN  32998  lncmp  33000  cdlemblem  33010  llnexchb2  33086  lautle  33301  lautcvr  33309  ldilset  33326  ltrnset  33335  trlset  33378  cdlemc4  33411  cdleme11dN  33479  cdleme20k  33536  cdleme21ct  33546  cdleme22b  33558  tendoex  34192  diafval  34249  diaval  34250  dicfval  34393  dihfval  34449  dihglblem2N  34512