MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  breq2 Unicode version

Theorem breq2 4029
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
StepHypRef Expression
1 opeq2 3799 . . 3  |-  ( A  =  B  ->  <. C ,  A >.  =  <. C ,  B >. )
21eleq1d 2351 . 2  |-  ( A  =  B  ->  ( <. C ,  A >.  e.  R  <->  <. C ,  B >.  e.  R ) )
3 df-br 4026 . 2  |-  ( C R A  <->  <. C ,  A >.  e.  R )
4 df-br 4026 . 2  |-  ( C R B  <->  <. C ,  B >.  e.  R )
52, 3, 43bitr4g 279 1  |-  ( A  =  B  ->  ( C R A  <->  C R B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    = wceq 1625    e. wcel 1686   <.cop 3645   class class class wbr 4025
This theorem is referenced by:  breq12  4030  breq2i  4033  breq2d  4037  nbrne1  4042  pocl  4323  swopolem  4325  swopo  4326  solin  4339  sotric  4342  sotrieq  4343  isso2i  4348  somo  4350  seex  4358  frirr  4372  fr2nr  4373  frminex  4375  wereu2  4392  fr3nr  4573  dfwe2  4575  vtoclr  4735  posn  4760  frsn  4762  brcog  4852  opelcnvg  4863  dfdmf  4875  breldmg  4886  dfrnf  4919  dmcoss  4946  resieq  4967  dfres2  5004  elimag  5018  elrelimasn  5039  elimasn  5040  asymref2  5062  intirr  5063  poirr2  5069  sotri3  5075  poltletr  5080  soltmin  5084  dffun3  5268  dffun6f  5271  fun11  5317  brprcneu  5520  fv3  5543  tz6.12c  5549  tz6.12i  5550  funbrfv  5563  fnbrfvb  5565  funfv2f  5590  dffv2  5594  fndmdif  5631  dff3  5675  fmptco  5693  foeqcnvco  5806  isorel  5825  soisores  5826  soisoi  5827  isocnv  5829  isotr  5835  isopolem  5844  isosolem  5846  f1oiso  5850  f1oiso2  5851  f1oweALT  5853  caovordig  6027  caovordg  6029  caovord  6033  caofrss  6112  caoftrn  6114  frxp  6227  poxp  6229  tposoprab  6272  fvopab5  6291  ertr  6677  ecopovsym  6762  ecopovtrn  6763  th3qlem2  6767  domeng  6878  eqeng  6897  snfi  6943  sbth  6983  domunsn  7013  domssex  7024  nneneq  7046  php2  7048  onfin  7053  1sdom  7067  unxpdom  7072  isinf  7078  fineqvlem  7079  pssnn  7083  ssnnfi  7084  dif1enOLD  7092  dif1en  7093  findcard  7099  findcard2  7100  findcard3  7102  frfi  7104  fisupg  7107  nnsdomg  7118  unfi  7126  fiint  7135  supmo  7205  eqsup  7209  supub  7212  suplub  7213  suplub2  7214  supmaxlem  7217  fisup2g  7219  fisupcl  7220  suppr  7221  supisolem  7223  supisoex  7224  ordtypecbv  7234  ordtypelem3  7237  ordtypelem6  7240  ordtypelem7  7241  ordtypelem9  7243  wemaplem1  7263  wemaplem2  7264  harval  7278  wemapwe  7402  r111  7449  cardf2  7578  isnum2  7580  cardval3  7587  cardnueq0  7599  carden2a  7601  cardlim  7607  isinffi  7627  onsdom  7631  harval2  7632  cardmin2  7633  ondomen  7666  alephnbtwn  7700  alephinit  7724  aceq3lem  7749  infmap2  7846  cfslb2n  7896  sornom  7905  isfin4  7925  fin23lem26  7953  fin23lem27  7956  fin1a2lem11  8038  fin1a2lem12  8039  hsmex  8060  domtriomlem  8070  dominf  8073  zorn2lem2  8126  zorn2lem7  8131  zorn2g  8132  axdclem  8148  axdc  8150  fodomg  8152  brdom7disj  8158  brdom6disj  8159  cardmin  8188  ficard  8189  alephval2  8196  dominfac  8197  cfpwsdom  8208  gchi  8248  fpwwe2lem12  8265  fpwwe2lem13  8266  canthp1lem1  8276  canthp1lem2  8277  pwfseqlem4a  8285  pwfseqlem4  8286  elina  8311  winainflem  8317  eltskg  8374  rankcf  8401  indpi  8533  nqereu  8555  nsmallnq  8603  ltbtwnnq  8604  ltrnq  8605  prcdnq  8619  genpcd  8632  genpnmax  8633  ltaddpr2  8661  ltexprlem4  8665  prlem936  8673  reclem2pr  8674  reclem3pr  8675  supexpr  8680  ltsosr  8718  ltasr  8724  recexsrlem  8727  mulgt0sr  8729  map2psrpr  8734  supsrlem  8735  axpre-lttri  8789  axpre-lttrn  8790  axpre-ltadd  8791  axpre-mulgt0  8792  axpre-sup  8793  ltletr  8915  letr  8916  ltne  8919  eqle  8925  ltordlem  9300  elimgt0  9594  elimge0  9595  squeeze0  9661  fimaxre2  9704  lbreu  9706  lble  9708  lbinfm  9709  sup2  9712  infm3  9715  suprlub  9718  supmul1  9721  supmullem1  9722  supmullem2  9723  supmul  9724  infmrcl  9735  infmrgelb  9736  nn2ge  9773  nnge1  9774  nnsub  9786  nominpos  9950  nnunb  9963  elnnnn0b  10010  nn0sub  10016  peano2uz2  10101  peano5uzi  10102  dfuzi  10104  uzind  10105  uzind3  10107  uzindOLD  10108  uzind3OLD  10109  eluz1  10236  uzind4  10278  uzwo  10283  uzwoOLD  10284  nnwof  10287  indstr2  10298  ublbneg  10304  zsupss  10309  uzsupss  10312  uzwo3  10313  zmin  10314  zmax  10315  zbtwnre  10316  rebtwnz  10317  rpnnen1lem1  10344  rpnnen1lem2  10345  rpnnen1lem3  10346  rpnnen1lem4  10347  rpnnen1lem5  10348  reexALT  10350  elrp  10358  mnfltxr  10468  xrltnsym  10473  xrlttri  10475  xrlttr  10476  xrltletr  10490  xrletr  10491  ngtmnft  10498  xrltmin  10513  xrlemin  10515  ifle  10526  z2ge  10527  qbtwnre  10528  qbtwnxr  10529  qextlt  10532  qextle  10533  xltnegi  10545  xmullem2  10587  xmulasslem2  10604  xmulasslem  10607  xlemul1a  10610  xrsupexmnf  10625  xrsupsslem  10627  xrinfmsslem  10628  xrub  10632  supxrpnf  10639  supxrunb1  10640  supxrunb2  10641  ixxval  10666  elixx1  10667  elioo2  10699  iccid  10703  icc0  10706  iccsupr  10738  repos  10742  fzval  10786  elfz1  10789  flval  10928  flval2  10946  flval3  10947  uzsup  10969  modid2  10996  fsequb  11039  serge0  11102  expge0  11140  expge1  11141  facdiv  11302  facwordi  11304  hashkf  11341  hashdom  11363  shftfib  11569  shftfn  11570  2shfti  11577  sqrlem3  11732  resqrex  11738  cau3lem  11840  caubnd2  11843  caubnd  11844  sqreu  11846  limsuple  11954  limsupval2  11956  rlim2  11972  climi  11986  rlimi  11989  ello12r  11993  ello1mpt  11997  ello1d  11999  lo1bdd2  12000  lo1bddrp  12001  elo12r  12004  o1lo1  12013  rlimclim1  12021  rlimdm  12027  climeu  12031  climmo  12033  2clim  12048  o1co  12062  o1compt  12063  addcn2  12069  mulcn2  12071  reccn2  12072  cn1lem  12073  rlimo1  12092  lo1add  12102  lo1mul  12103  climsup  12145  caucvgrlem  12147  caucvgb  12154  summo  12192  zsum  12193  fsum  12195  o1fsum  12273  climcnds  12312  supcvg  12316  rpnnen2lem4  12498  rpnnen  12507  ruclem2  12512  ruclem12  12521  sqr2irr  12529  dvdsabsb  12550  0dvds  12551  dvdsle  12576  alzdvds  12580  dvdsext  12581  fzo0dvdseq  12583  divalglem10  12603  bitsinv1lem  12634  sadadd3  12654  bitsuz  12667  gcdval  12689  gcdcllem1  12692  gcdcllem2  12693  gcddvds  12696  bezoutlem4  12722  dvdsgcd  12724  dvdssq  12741  isprm  12762  isprm2lem  12767  dvdsprm  12780  coprmdvds2  12784  isprm6  12790  exprmfct  12791  maxprmfct  12794  prmexpb  12798  prmfac1  12799  rpexp  12801  iserodd  12890  pceu  12901  pczpre  12902  pcdiv  12907  pcdvdsb  12923  pcmpt  12942  pcmptdvds  12944  prmpwdvds  12953  unbenlem  12957  infpnlem2  12960  infpn2  12962  prmreclem1  12965  prmreclem2  12966  prmreclem3  12967  prmreclem5  12969  prmreclem6  12970  vdwlem9  13038  vdwlem10  13039  vdwlem13  13042  ramcl2lem  13058  ramz  13074  imasleval  13445  mreexexlem3d  13550  mreexexlem4d  13551  mreexexd  13552  prslem  14067  drsdirfi  14074  posi  14086  posasymb  14088  pleval2  14101  plttr  14106  pltletr  14107  pospo  14109  lubprop  14116  lubid  14118  glbprop  14121  glble  14122  joinlem  14126  joinle  14129  meetval2  14132  meetlem  14133  isglbd  14223  lubl  14226  lubun  14229  pospropd  14240  poslubmo  14252  poslubd  14253  tsrlin  14330  tsrlemax  14331  spwmo  14337  spwpr4  14342  letsr  14351  eqgen  14672  odeq  14867  odmulg  14871  pgpssslw  14927  sylow2alem2  14931  sylow2blem3  14935  efgval2  15035  efgsfo  15050  efgred  15059  efgredeu  15063  efgcpbllemb  15066  gexex  15147  cyggex2  15185  pgpfaclem1  15318  pgpfaclem2  15319  pgpfaclem3  15320  ablfaclem2  15323  ablfaclem3  15324  lidldvgen  16009  psrass1lem  16125  psrmulval  16133  mplmonmul  16210  opsrtoslem2  16228  coe1mul2  16348  coe1tmmul2fv  16356  coe1pwmulfv  16358  zndvds  16505  znleval  16510  ordtbaslem  16920  ordtbas2  16923  ordtopn1  16926  mnfnei  16953  ordtt1  17109  ordthauslem  17113  ordthmeolem  17494  imasdsf1olem  17939  comet  18061  stdbdxmet  18063  stdbdmet  18064  stdbdmopn  18066  metcnpi  18092  metcnpi2  18093  metcnpi3  18094  ngptgp  18154  nlmvscnlem1  18199  nrginvrcnlem  18203  nmogelb  18227  nmolb  18228  nghmcn  18256  xrsxmet  18317  icccmplem2  18330  icccmplem3  18331  reconnlem2  18334  xrge0tsms  18341  xmetdcn2  18344  metdsf  18354  metdsge  18355  metdscn  18362  metnrmlem1a  18364  addcnlem  18370  cncfi  18400  elcncf1di  18401  iccpnfhmeo  18445  xrhmeo  18446  cnllycmp  18456  evth  18459  ipcnlem1  18674  lmmcvg  18689  cfili  18696  cncmet  18746  minveclem1  18790  minveclem3b  18794  minveclem6  18800  pmltpclem1  18810  pmltpc  18812  ivthlem2  18814  ivthlem3  18815  cniccbdd  18823  ovolmge0  18838  ovolgelb  18841  ovolctb  18851  ovolunlem1  18858  ovoliunlem1  18863  ovoliun  18866  ovoliun2  18867  ovolshftlem1  18870  ovolscalem1  18874  ovolicc2lem3  18880  ovolicc2lem5  18882  ovolicc2  18883  voliunlem3  18911  ioombl1lem1  18917  ioombl1lem4  18920  uniioombllem2  18940  uniioombllem6  18945  volcn  18963  ismbfd  18997  mbfsup  19021  mbfinf  19022  mbflimsup  19023  itg1ge0  19043  itg1climres  19071  mbfi1fseqlem5  19076  itg2val  19085  itg2const  19097  itg2const2  19098  itg2seq  19099  itg2monolem1  19107  itg2i1fseq  19112  itg2i1fseq2  19113  itg2addlem  19115  itg2cnlem1  19118  itg2cnlem2  19119  itg2cn  19120  isibl  19122  ditgeq2  19201  dveflem  19328  dvferm1lem  19333  rolle  19339  c1lip1  19346  lhop1  19363  dvfsumlem2  19376  dvfsumlem4  19378  dvfsumrlim  19380  dvfsum2  19383  mdegmullem  19466  deg1leb  19483  deg1lt  19485  dvdsq1p  19548  plyeq0lem  19594  dgrco  19658  plydivex  19679  quotcan  19691  aannenlem1  19710  aannenlem2  19711  ulmi  19767  ulmcaulem  19773  ulmcau  19774  ulmbdd  19777  ulmdvlem3  19781  iblulm  19785  psercnlem1  19803  psercn  19804  abelthlem8  19817  sinhalfpilem  19836  logltb  19955  cxple2  20046  cxpcn3lem  20089  isosctrlem1  20120  leibpilem2  20239  cxploglim  20274  scvxcvx  20282  emcllem6  20296  ftalem3  20314  vmaval  20353  isppw2  20355  muval  20372  fsumdvdscom  20427  dvdsflf1o  20429  dvdsflsumcom  20430  musum  20433  muinv  20435  ppiublem1  20443  chtub  20453  logfac2  20458  bpos1lem  20523  bposlem9  20533  lgsdir  20571  lgsne0  20574  lgsqr  20587  lgsquadlem1  20595  lgsquadlem2  20596  lgsquadlem3  20597  2sqlem6  20610  2sqlem8  20613  2sqlem10  20615  dchrisumlema  20639  dchrisumlem2  20641  dchrisumlem3  20642  dchrvmasumiflem1  20652  dchrisum0fval  20656  dchrisum0ff  20658  dchrisum0flblem2  20660  logsqvma2  20694  pntrsumbnd2  20718  pntrlog2bndlem1  20728  pntpbnd1  20737  pntpbnd2  20738  pntibndlem2  20742  pntibndlem3  20743  pntibnd  20744  pntlemi  20755  pntlem3  20760  pntlemp  20761  pntleml  20762  pnt3  20763  gxval  20927  vacn  21269  nmcvcn  21270  smcnlem  21272  nmobndi  21355  blocni  21385  ubthlem1  21451  ubthlem2  21452  ubthlem3  21453  minvecolem1  21455  minvecolem5  21462  minvecolem6  21463  htthlem  21499  norm3lemt  21733  hcaucvg  21767  hlimconvi  21772  hlim2  21773  chlimi  21816  hlimreui  21821  occl  21885  cmbr3  22189  cmcm  22195  cmcm3  22196  lecm  22198  cnopc  22495  cnfnc  22512  0cnop  22561  0cnfn  22562  idcnop  22563  nmopun  22596  nmcexi  22608  lnconi  22615  branmfn  22687  opsqrlem1  22722  pjnmopi  22730  pjnormssi  22750  stge1i  22820  strlem5  22837  hstrlem5  22845  mddmd2  22891  csmdsymi  22916  cvmd  22918  ela  22921  cvbr4i  22949  chirredlem3  22974  chirredlem4  22975  chirred  22977  atmd  22981  mdsym  22994  mddmdin0i  23013  cdj1i  23015  cdj3i  23023  ballotlemfcc  23054  fmptcof2  23231  isoun  23244  rge0scvg  23375  xrge0tsmsd  23384  ishashinf  23391  esumcst  23438  esumpinfval  23443  esumpcvgval  23448  esumcvg  23456  dstfrvunirn  23677  subfacp1lem1  23712  relexpindlem  24038  relexpind  24039  rtrclreclem.trans  24045  dedekind  24084  dedekindle  24085  dfpo2  24114  fundmpss  24124  funbreq  24129  predbrg  24188  poseq  24255  nodenselem4  24340  nodenselem5  24341  nodense  24345  nocvxminlem  24346  nobndup  24356  nofulllem5  24362  brtxp  24422  brtxp2  24423  brpprod3a  24428  elfix  24445  dffun10  24455  fnsingle  24460  brimageg  24468  fnimage  24470  brdomaing  24476  brrangeg  24477  brcup  24480  brcap  24481  funpartfv  24485  axcontlem10  24603  fvtransport  24657  supaddc  24927  supadd  24928  itg2addnclem  24933  itg2addnc  24935  srefwref  25078  oriso  25225  puub2  25269  puub  25270  supdef  25273  ismnl2  25279  defge3  25282  inposet  25289  cntrset  25613  lvsovso  25637  trer  26238  elicc3  26239  finminlem  26242  nn0prpwlem  26249  nn0prpw  26250  fnessref  26304  refssfne  26305  fnemeet2  26327  filnetlem3  26340  frinfm  26427  fdc1  26467  nninfnub  26472  equivbnd  26525  heibor1lem  26544  heiborlem8  26553  iccbnd  26575  lzenom  26860  fphpdo  26911  rencldnfilem  26914  irrapxlem5  26922  irrapxlem6  26923  pellexlem3  26927  pellqrex  26975  pellfundre  26977  pellfundge  26978  pellfundlb  26980  pellfundglb  26981  monotoddzz  27039  oddcomabszz  27040  zindbi  27042  jm2.22  27099  jm2.23  27100  rpnnen3  27136  ttac  27140  fnwe2lem2  27159  aomclem8  27170  islinds  27290  hbtlem1  27338  hbtlem5  27343  xrltneNEW  27668  ubelsupr  27702  climinf  27743  stoweidlem14  27774  stoweidlem29  27789  stoweidlem31  27791  stoweidlem34  27794  stoweidlem49  27809  wallispilem3  27827  stirlinglem13  27846  stirlinglem14  27847  usgra0v  28128  usgra1v  28137  isfrgra  28182  bnj1185  28899  bnj602  29020  bnj1228  29114  lubunNEW  29236  oposlem  29446  lub0N  29452  glb0N  29456  omllaw  29506  cvrval  29532  cvrnbtwn  29534  cvrnbtwn2  29538  cvrnbtwn3  29539  cvrcon3b  29540  cvrnbtwn4  29542  cvrcmp  29546  isat  29549  atnlt  29576  atlex  29579  cvlexch1  29591  cvlexchb1  29593  cvlatexch1  29599  glbconN  29639  2llnne2N  29670  cvratlem  29683  cvrat4  29705  ps-1  29739  3at  29752  islln  29768  llncmp  29784  llnnlt  29785  islpln  29792  islpln5  29797  lvolex3N  29800  lplncmp  29824  lplnexllnN  29826  lplnnlt  29827  islvol  29835  lvoli3  29839  islvol5  29841  lvolcmp  29879  lvolnltN  29880  dalem-cly  29933  dalem44  29978  pmapval  30019  pmapglbx  30031  lncvrelatN  30043  lncmp  30045  cdlemblem  30055  llnexchb2  30131  lautle  30346  lautcvr  30354  ldilset  30371  ltrnset  30380  trlset  30423  cdlemc4  30456  cdleme11dN  30524  cdleme20k  30581  cdleme21ct  30591  cdleme22b  30603  tendoex  31237  diafval  31294  diaval  31295  dicfval  31438  dihfval  31494  dihglblem2N  31557
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-6 1705  ax-7 1710  ax-11 1717  ax-12 1868  ax-ext 2266
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1531  df-nf 1534  df-sb 1632  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-rab 2554  df-v 2792  df-dif 3157  df-un 3159  df-in 3161  df-ss 3168  df-nul 3458  df-if 3568  df-sn 3648  df-pr 3649  df-op 3651  df-br 4026
  Copyright terms: Public domain W3C validator