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

Theorem breq2 4043
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 3813 . . 3  |-  ( A  =  B  ->  <. C ,  A >.  =  <. C ,  B >. )
21eleq1d 2362 . 2  |-  ( A  =  B  ->  ( <. C ,  A >.  e.  R  <->  <. C ,  B >.  e.  R ) )
3 df-br 4040 . 2  |-  ( C R A  <->  <. C ,  A >.  e.  R )
4 df-br 4040 . 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 1632    e. wcel 1696   <.cop 3656   class class class wbr 4039
This theorem is referenced by:  breq12  4044  breq2i  4047  breq2d  4051  nbrne1  4056  pocl  4337  swopolem  4339  swopo  4340  solin  4353  sotric  4356  sotrieq  4357  isso2i  4362  somo  4364  seex  4372  frirr  4386  fr2nr  4387  frminex  4389  wereu2  4406  fr3nr  4587  dfwe2  4589  vtoclr  4749  posn  4774  frsn  4776  brcog  4866  opelcnvg  4877  dfdmf  4889  breldmg  4900  dfrnf  4933  dmcoss  4960  resieq  4981  dfres2  5018  elimag  5032  elrelimasn  5053  elimasn  5054  asymref2  5076  intirr  5077  poirr2  5083  sotri3  5089  poltletr  5094  soltmin  5098  dffun3  5282  dffun6f  5285  fun11  5331  brprcneu  5534  fv3  5557  tz6.12c  5563  tz6.12i  5564  funbrfv  5577  fnbrfvb  5579  funfv2f  5604  dffv2  5608  fndmdif  5645  dff3  5689  fmptco  5707  foeqcnvco  5820  isorel  5839  soisores  5840  soisoi  5841  isocnv  5843  isotr  5849  isopolem  5858  isosolem  5860  f1oiso  5864  f1oiso2  5865  f1oweALT  5867  caovordig  6041  caovordg  6043  caovord  6047  caofrss  6126  caoftrn  6128  frxp  6241  poxp  6243  tposoprab  6286  fvopab5  6305  ertr  6691  ecopovsym  6776  ecopovtrn  6777  th3qlem2  6781  domeng  6892  eqeng  6911  snfi  6957  sbth  6997  domunsn  7027  domssex  7038  nneneq  7060  php2  7062  onfin  7067  1sdom  7081  unxpdom  7086  isinf  7092  fineqvlem  7093  pssnn  7097  ssnnfi  7098  dif1enOLD  7106  dif1en  7107  findcard  7113  findcard2  7114  findcard3  7116  frfi  7118  fisupg  7121  nnsdomg  7132  unfi  7140  fiint  7149  supmo  7219  eqsup  7223  supub  7226  suplub  7227  suplub2  7228  supmaxlem  7231  fisup2g  7233  fisupcl  7234  suppr  7235  supisolem  7237  supisoex  7238  ordtypecbv  7248  ordtypelem3  7251  ordtypelem6  7254  ordtypelem7  7255  ordtypelem9  7257  wemaplem1  7277  wemaplem2  7278  harval  7292  wemapwe  7416  r111  7463  cardf2  7592  isnum2  7594  cardval3  7601  cardnueq0  7613  carden2a  7615  cardlim  7621  isinffi  7641  onsdom  7645  harval2  7646  cardmin2  7647  ondomen  7680  alephnbtwn  7714  alephinit  7738  aceq3lem  7763  infmap2  7860  cfslb2n  7910  sornom  7919  isfin4  7939  fin23lem26  7967  fin23lem27  7970  fin1a2lem11  8052  fin1a2lem12  8053  hsmex  8074  domtriomlem  8084  dominf  8087  zorn2lem2  8140  zorn2lem7  8145  zorn2g  8146  axdclem  8162  axdc  8164  fodomg  8166  brdom7disj  8172  brdom6disj  8173  cardmin  8202  ficard  8203  alephval2  8210  dominfac  8211  cfpwsdom  8222  gchi  8262  fpwwe2lem12  8279  fpwwe2lem13  8280  canthp1lem1  8290  canthp1lem2  8291  pwfseqlem4a  8299  pwfseqlem4  8300  elina  8325  winainflem  8331  eltskg  8388  rankcf  8415  indpi  8547  nqereu  8569  nsmallnq  8617  ltbtwnnq  8618  ltrnq  8619  prcdnq  8633  genpcd  8646  genpnmax  8647  ltaddpr2  8675  ltexprlem4  8679  prlem936  8687  reclem2pr  8688  reclem3pr  8689  supexpr  8694  ltsosr  8732  ltasr  8738  recexsrlem  8741  mulgt0sr  8743  map2psrpr  8748  supsrlem  8749  axpre-lttri  8803  axpre-lttrn  8804  axpre-ltadd  8805  axpre-mulgt0  8806  axpre-sup  8807  ltletr  8929  letr  8930  ltne  8933  eqle  8939  ltordlem  9314  elimgt0  9608  elimge0  9609  squeeze0  9675  fimaxre2  9718  lbreu  9720  lble  9722  lbinfm  9723  sup2  9726  infm3  9729  suprlub  9732  supmul1  9735  supmullem1  9736  supmullem2  9737  supmul  9738  infmrcl  9749  infmrgelb  9750  nn2ge  9787  nnge1  9788  nnsub  9800  nominpos  9964  nnunb  9977  elnnnn0b  10024  nn0sub  10030  peano2uz2  10115  peano5uzi  10116  dfuzi  10118  uzind  10119  uzind3  10121  uzindOLD  10122  uzind3OLD  10123  eluz1  10250  uzind4  10292  uzwo  10297  uzwoOLD  10298  nnwof  10301  indstr2  10312  ublbneg  10318  zsupss  10323  uzsupss  10326  uzwo3  10327  zmin  10328  zmax  10329  zbtwnre  10330  rebtwnz  10331  rpnnen1lem1  10358  rpnnen1lem2  10359  rpnnen1lem3  10360  rpnnen1lem4  10361  rpnnen1lem5  10362  reexALT  10364  elrp  10372  mnfltxr  10482  xrltnsym  10487  xrlttri  10489  xrlttr  10490  xrltletr  10504  xrletr  10505  ngtmnft  10512  xrltmin  10527  xrlemin  10529  ifle  10540  z2ge  10541  qbtwnre  10542  qbtwnxr  10543  qextlt  10546  qextle  10547  xltnegi  10559  xmullem2  10601  xmulasslem2  10618  xmulasslem  10621  xlemul1a  10624  xrsupexmnf  10639  xrsupsslem  10641  xrinfmsslem  10642  xrub  10646  supxrpnf  10653  supxrunb1  10654  supxrunb2  10655  ixxval  10680  elixx1  10681  elioo2  10713  iccid  10717  icc0  10720  iccsupr  10752  repos  10756  fzval  10800  elfz1  10803  flval  10942  flval2  10960  flval3  10961  uzsup  10983  modid2  11010  fsequb  11053  serge0  11116  expge0  11154  expge1  11155  facdiv  11316  facwordi  11318  hashkf  11355  hashdom  11377  shftfib  11583  shftfn  11584  2shfti  11591  sqrlem3  11746  resqrex  11752  cau3lem  11854  caubnd2  11857  caubnd  11858  sqreu  11860  limsuple  11968  limsupval2  11970  rlim2  11986  climi  12000  rlimi  12003  ello12r  12007  ello1mpt  12011  ello1d  12013  lo1bdd2  12014  lo1bddrp  12015  elo12r  12018  o1lo1  12027  rlimclim1  12035  rlimdm  12041  climeu  12045  climmo  12047  2clim  12062  o1co  12076  o1compt  12077  addcn2  12083  mulcn2  12085  reccn2  12086  cn1lem  12087  rlimo1  12106  lo1add  12116  lo1mul  12117  climsup  12159  caucvgrlem  12161  caucvgb  12168  summo  12206  zsum  12207  fsum  12209  o1fsum  12287  climcnds  12326  supcvg  12330  rpnnen2lem4  12512  rpnnen  12521  ruclem2  12526  ruclem12  12535  sqr2irr  12543  dvdsabsb  12564  0dvds  12565  dvdsle  12590  alzdvds  12594  dvdsext  12595  fzo0dvdseq  12597  divalglem10  12617  bitsinv1lem  12648  sadadd3  12668  bitsuz  12681  gcdval  12703  gcdcllem1  12706  gcdcllem2  12707  gcddvds  12710  bezoutlem4  12736  dvdsgcd  12738  dvdssq  12755  isprm  12776  isprm2lem  12781  dvdsprm  12794  coprmdvds2  12798  isprm6  12804  exprmfct  12805  maxprmfct  12808  prmexpb  12812  prmfac1  12813  rpexp  12815  iserodd  12904  pceu  12915  pczpre  12916  pcdiv  12921  pcdvdsb  12937  pcmpt  12956  pcmptdvds  12958  prmpwdvds  12967  unbenlem  12971  infpnlem2  12974  infpn2  12976  prmreclem1  12979  prmreclem2  12980  prmreclem3  12981  prmreclem5  12983  prmreclem6  12984  vdwlem9  13052  vdwlem10  13053  vdwlem13  13056  ramcl2lem  13072  ramz  13088  imasleval  13459  mreexexlem3d  13564  mreexexlem4d  13565  mreexexd  13566  prslem  14081  drsdirfi  14088  posi  14100  posasymb  14102  pleval2  14115  plttr  14120  pltletr  14121  pospo  14123  lubprop  14130  lubid  14132  glbprop  14135  glble  14136  joinlem  14140  joinle  14143  meetval2  14146  meetlem  14147  isglbd  14237  lubl  14240  lubun  14243  pospropd  14254  poslubmo  14266  poslubd  14267  tsrlin  14344  tsrlemax  14345  spwmo  14351  spwpr4  14356  letsr  14365  eqgen  14686  odeq  14881  odmulg  14885  pgpssslw  14941  sylow2alem2  14945  sylow2blem3  14949  efgval2  15049  efgsfo  15064  efgred  15073  efgredeu  15077  efgcpbllemb  15080  gexex  15161  cyggex2  15199  pgpfaclem1  15332  pgpfaclem2  15333  pgpfaclem3  15334  ablfaclem2  15337  ablfaclem3  15338  lidldvgen  16023  psrass1lem  16139  psrmulval  16147  mplmonmul  16224  opsrtoslem2  16242  coe1mul2  16362  coe1tmmul2fv  16370  coe1pwmulfv  16372  zndvds  16519  znleval  16524  ordtbaslem  16934  ordtbas2  16937  ordtopn1  16940  mnfnei  16967  ordtt1  17123  ordthauslem  17127  ordthmeolem  17508  imasdsf1olem  17953  comet  18075  stdbdxmet  18077  stdbdmet  18078  stdbdmopn  18080  metcnpi  18106  metcnpi2  18107  metcnpi3  18108  ngptgp  18168  nlmvscnlem1  18213  nrginvrcnlem  18217  nmogelb  18241  nmolb  18242  nghmcn  18270  xrsxmet  18331  icccmplem2  18344  icccmplem3  18345  reconnlem2  18348  xrge0tsms  18355  xmetdcn2  18358  metdsf  18368  metdsge  18369  metdscn  18376  metnrmlem1a  18378  addcnlem  18384  cncfi  18414  elcncf1di  18415  iccpnfhmeo  18459  xrhmeo  18460  cnllycmp  18470  evth  18473  ipcnlem1  18688  lmmcvg  18703  cfili  18710  cncmet  18760  minveclem1  18804  minveclem3b  18808  minveclem6  18814  pmltpclem1  18824  pmltpc  18826  ivthlem2  18828  ivthlem3  18829  cniccbdd  18837  ovolmge0  18852  ovolgelb  18855  ovolctb  18865  ovolunlem1  18872  ovoliunlem1  18877  ovoliun  18880  ovoliun2  18881  ovolshftlem1  18884  ovolscalem1  18888  ovolicc2lem3  18894  ovolicc2lem5  18896  ovolicc2  18897  voliunlem3  18925  ioombl1lem1  18931  ioombl1lem4  18934  uniioombllem2  18954  uniioombllem6  18959  volcn  18977  ismbfd  19011  mbfsup  19035  mbfinf  19036  mbflimsup  19037  itg1ge0  19057  itg1climres  19085  mbfi1fseqlem5  19090  itg2val  19099  itg2const  19111  itg2const2  19112  itg2seq  19113  itg2monolem1  19121  itg2i1fseq  19126  itg2i1fseq2  19127  itg2addlem  19129  itg2cnlem1  19132  itg2cnlem2  19133  itg2cn  19134  isibl  19136  ditgeq2  19215  dveflem  19342  dvferm1lem  19347  rolle  19353  c1lip1  19360  lhop1  19377  dvfsumlem2  19390  dvfsumlem4  19392  dvfsumrlim  19394  dvfsum2  19397  mdegmullem  19480  deg1leb  19497  deg1lt  19499  dvdsq1p  19562  plyeq0lem  19608  dgrco  19672  plydivex  19693  quotcan  19705  aannenlem1  19724  aannenlem2  19725  ulmi  19781  ulmcaulem  19787  ulmcau  19788  ulmbdd  19791  ulmdvlem3  19795  iblulm  19799  psercnlem1  19817  psercn  19818  abelthlem8  19831  sinhalfpilem  19850  logltb  19969  cxple2  20060  cxpcn3lem  20103  isosctrlem1  20134  leibpilem2  20253  cxploglim  20288  scvxcvx  20296  emcllem6  20310  ftalem3  20328  vmaval  20367  isppw2  20369  muval  20386  fsumdvdscom  20441  dvdsflf1o  20443  dvdsflsumcom  20444  musum  20447  muinv  20449  ppiublem1  20457  chtub  20467  logfac2  20472  bpos1lem  20537  bposlem9  20547  lgsdir  20585  lgsne0  20588  lgsqr  20601  lgsquadlem1  20609  lgsquadlem2  20610  lgsquadlem3  20611  2sqlem6  20624  2sqlem8  20627  2sqlem10  20629  dchrisumlema  20653  dchrisumlem2  20655  dchrisumlem3  20656  dchrvmasumiflem1  20666  dchrisum0fval  20670  dchrisum0ff  20672  dchrisum0flblem2  20674  logsqvma2  20708  pntrsumbnd2  20732  pntrlog2bndlem1  20742  pntpbnd1  20751  pntpbnd2  20752  pntibndlem2  20756  pntibndlem3  20757  pntibnd  20758  pntlemi  20769  pntlem3  20774  pntlemp  20775  pntleml  20776  pnt3  20777  gxval  20941  vacn  21283  nmcvcn  21284  smcnlem  21286  nmobndi  21369  blocni  21399  ubthlem1  21465  ubthlem2  21466  ubthlem3  21467  minvecolem1  21469  minvecolem5  21476  minvecolem6  21477  htthlem  21513  norm3lemt  21747  hcaucvg  21781  hlimconvi  21786  hlim2  21787  chlimi  21830  hlimreui  21835  occl  21899  cmbr3  22203  cmcm  22209  cmcm3  22210  lecm  22212  cnopc  22509  cnfnc  22526  0cnop  22575  0cnfn  22576  idcnop  22577  nmopun  22610  nmcexi  22622  lnconi  22629  branmfn  22701  opsqrlem1  22736  pjnmopi  22744  pjnormssi  22764  stge1i  22834  strlem5  22851  hstrlem5  22859  mddmd2  22905  csmdsymi  22930  cvmd  22932  ela  22935  cvbr4i  22963  chirredlem3  22988  chirredlem4  22989  chirred  22991  atmd  22995  mdsym  23008  mddmdin0i  23027  cdj1i  23029  cdj3i  23037  ballotlemfcc  23068  fmptcof2  23244  isoun  23257  rge0scvg  23388  xrge0tsmsd  23397  ishashinf  23404  esumcst  23451  esumpinfval  23456  esumpcvgval  23461  esumcvg  23469  dstfrvunirn  23690  subfacp1lem1  23725  relexpindlem  24051  relexpind  24052  rtrclreclem.trans  24058  dedekind  24097  dedekindle  24098  prodmo  24159  zprod  24160  zprodn0  24162  fprod  24164  dfpo2  24183  fundmpss  24193  funbreq  24198  predbrg  24257  poseq  24324  nodenselem4  24409  nodenselem5  24410  nodense  24414  nocvxminlem  24415  nobndup  24425  nofulllem5  24431  brtxp  24491  brtxp2  24492  brpprod3a  24497  elfix  24514  dffun10  24524  fnsingle  24529  brimageg  24537  fnimage  24539  brdomaing  24545  brrangeg  24546  brcup  24549  brcap  24550  funpartlem  24552  axcontlem10  24673  fvtransport  24727  supaddc  24995  supadd  24996  itg2addnclem  25003  itg2addnc  25005  itg2gt0cn  25006  srefwref  25170  oriso  25317  puub2  25361  puub  25362  supdef  25365  ismnl2  25371  defge3  25374  inposet  25381  cntrset  25705  lvsovso  25729  trer  26330  elicc3  26331  finminlem  26334  nn0prpwlem  26341  nn0prpw  26342  fnessref  26396  refssfne  26397  fnemeet2  26419  filnetlem3  26432  frinfm  26519  fdc1  26559  nninfnub  26564  equivbnd  26617  heibor1lem  26636  heiborlem8  26645  iccbnd  26667  lzenom  26952  fphpdo  27003  rencldnfilem  27006  irrapxlem5  27014  irrapxlem6  27015  pellexlem3  27019  pellqrex  27067  pellfundre  27069  pellfundge  27070  pellfundlb  27072  pellfundglb  27073  monotoddzz  27131  oddcomabszz  27132  zindbi  27134  jm2.22  27191  jm2.23  27192  rpnnen3  27228  ttac  27232  fnwe2lem2  27251  aomclem8  27262  islinds  27382  hbtlem1  27430  hbtlem5  27435  xrltneNEW  27760  ubelsupr  27794  climinf  27835  stoweidlem14  27866  stoweidlem29  27881  stoweidlem31  27883  stoweidlem34  27886  stoweidlem49  27901  wallispilem3  27919  stirlinglem13  27938  stirlinglem14  27939  rlimdmafv  28145  hashgt12el  28218  hashgt12el2  28219  usgra0v  28251  usgra1v  28260  3v3e3cycl1  28390  4cycl4v4e  28412  4cycl4dv  28413  isfrgra  28417  bnj1185  29142  bnj602  29263  bnj1228  29357  lubunNEW  29785  oposlem  29995  lub0N  30001  glb0N  30005  omllaw  30055  cvrval  30081  cvrnbtwn  30083  cvrnbtwn2  30087  cvrnbtwn3  30088  cvrcon3b  30089  cvrnbtwn4  30091  cvrcmp  30095  isat  30098  atnlt  30125  atlex  30128  cvlexch1  30140  cvlexchb1  30142  cvlatexch1  30148  glbconN  30188  2llnne2N  30219  cvratlem  30232  cvrat4  30254  ps-1  30288  3at  30301  islln  30317  llncmp  30333  llnnlt  30334  islpln  30341  islpln5  30346  lvolex3N  30349  lplncmp  30373  lplnexllnN  30375  lplnnlt  30376  islvol  30384  lvoli3  30388  islvol5  30390  lvolcmp  30428  lvolnltN  30429  dalem-cly  30482  dalem44  30527  pmapval  30568  pmapglbx  30580  lncvrelatN  30592  lncmp  30594  cdlemblem  30604  llnexchb2  30680  lautle  30895  lautcvr  30903  ldilset  30920  ltrnset  30929  trlset  30972  cdlemc4  31005  cdleme11dN  31073  cdleme20k  31130  cdleme21ct  31140  cdleme22b  31152  tendoex  31786  diafval  31843  diaval  31844  dicfval  31987  dihfval  32043  dihglblem2N  32106
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-rab 2565  df-v 2803  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-nul 3469  df-if 3579  df-sn 3659  df-pr 3660  df-op 3662  df-br 4040
  Copyright terms: Public domain W3C validator