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

Theorem breq2 4208
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 3977 . . 3  |-  ( A  =  B  ->  <. C ,  A >.  =  <. C ,  B >. )
21eleq1d 2501 . 2  |-  ( A  =  B  ->  ( <. C ,  A >.  e.  R  <->  <. C ,  B >.  e.  R ) )
3 df-br 4205 . 2  |-  ( C R A  <->  <. C ,  A >.  e.  R )
4 df-br 4205 . 2  |-  ( C R B  <->  <. C ,  B >.  e.  R )
52, 3, 43bitr4g 280 1  |-  ( A  =  B  ->  ( C R A  <->  C R B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    = wceq 1652    e. wcel 1725   <.cop 3809   class class class wbr 4204
This theorem is referenced by:  breq12  4209  breq2i  4212  breq2d  4216  nbrne1  4221  pocl  4502  swopolem  4504  swopo  4505  solin  4518  sotric  4521  sotrieq  4522  isso2i  4527  somo  4529  seex  4537  frirr  4551  fr2nr  4552  frminex  4554  wereu2  4571  fr3nr  4752  dfwe2  4754  vtoclr  4914  posn  4938  frsn  4940  brcog  5031  brcogw  5033  opelcnvg  5044  dfdmf  5056  breldmg  5067  dfrnf  5100  dmcoss  5127  resieq  5148  dfres2  5185  elimag  5199  elrelimasn  5220  elimasn  5221  asymref2  5243  intirr  5244  poirr2  5250  sotri3  5256  poltletr  5261  soltmin  5265  dffun3  5457  dffun6f  5460  fun11  5508  brprcneu  5713  fv3  5736  tz6.12c  5742  tz6.12i  5743  funbrfv  5757  fnbrfvb  5759  funfv2f  5784  dffv2  5788  fndmdif  5826  dff3  5874  fmptco  5893  foeqcnvco  6019  isorel  6038  soisores  6039  soisoi  6040  isocnv  6042  isotr  6048  isopolem  6057  isosolem  6059  f1oiso  6063  f1oiso2  6064  f1oweALT  6066  caovordig  6244  caovordg  6246  caovord  6250  caofrss  6329  caoftrn  6331  frxp  6448  poxp  6450  tposoprab  6507  fvopab5  6526  ertr  6912  ecopovsym  6998  ecopovtrn  6999  th3qlem2  7003  domeng  7114  eqeng  7133  snfi  7179  sbth  7219  domunsn  7249  domssex  7260  nneneq  7282  php2  7284  onfin  7289  1sdom  7303  unxpdom  7308  isinf  7314  fineqvlem  7315  pssnn  7319  ssnnfi  7320  dif1enOLD  7332  dif1en  7333  findcard  7339  findcard2  7340  findcard3  7342  frfi  7344  fisupg  7347  nnsdomg  7358  unfi  7366  fiint  7375  supmo  7449  eqsup  7453  supub  7456  suplub  7457  suplub2  7458  supmaxlem  7461  fisup2g  7463  fisupcl  7464  suppr  7465  supisolem  7467  supisoex  7468  ordtypecbv  7478  ordtypelem3  7481  ordtypelem6  7484  ordtypelem7  7485  ordtypelem9  7487  wemaplem1  7507  wemaplem2  7508  harval  7522  wemapwe  7646  r111  7693  cardf2  7822  isnum2  7824  cardval3  7831  cardnueq0  7843  carden2a  7845  cardlim  7851  isinffi  7871  onsdom  7875  harval2  7876  cardmin2  7877  ondomen  7910  alephnbtwn  7944  alephinit  7968  aceq3lem  7993  infmap2  8090  cfslb2n  8140  sornom  8149  isfin4  8169  fin23lem26  8197  fin23lem27  8200  fin1a2lem11  8282  fin1a2lem12  8283  hsmex  8304  domtriomlem  8314  dominf  8317  zorn2lem2  8369  zorn2lem7  8374  zorn2g  8375  axdclem  8391  axdc  8393  fodomg  8395  brdom7disj  8401  brdom6disj  8402  cardmin  8431  ficard  8432  alephval2  8439  dominfac  8440  cfpwsdom  8451  gchi  8491  fpwwe2lem12  8508  fpwwe2lem13  8509  canthp1lem1  8519  canthp1lem2  8520  pwfseqlem4a  8528  pwfseqlem4  8529  elina  8554  winainflem  8560  eltskg  8617  rankcf  8644  indpi  8776  nqereu  8798  nsmallnq  8846  ltbtwnnq  8847  ltrnq  8848  prcdnq  8862  genpcd  8875  genpnmax  8876  ltaddpr2  8904  ltexprlem4  8908  prlem936  8916  reclem2pr  8917  reclem3pr  8918  supexpr  8923  ltsosr  8961  ltasr  8967  recexsrlem  8970  mulgt0sr  8972  map2psrpr  8977  supsrlem  8978  axpre-lttri  9032  axpre-lttrn  9033  axpre-ltadd  9034  axpre-mulgt0  9035  axpre-sup  9036  ltletr  9158  letr  9159  ltne  9162  eqle  9168  ltordlem  9544  elimgt0  9838  elimge0  9839  squeeze0  9905  fimaxre2  9948  lbreu  9950  lble  9952  sup2  9956  infm3  9959  suprlub  9962  supmul1  9965  supmullem1  9966  supmullem2  9967  supmul  9968  infmrcl  9979  infmrgelb  9980  nn2ge  10017  nnge1  10018  nnsub  10030  nominpos  10196  nnunb  10209  elnnnn0b  10256  nn0sub  10262  peano2uz2  10349  peano5uzi  10350  dfuzi  10352  uzind  10353  uzind3  10355  uzindOLD  10356  uzind3OLD  10357  eluz1  10484  uzind4  10526  uzwo  10531  uzwoOLD  10532  nnwof  10535  indstr2  10546  ublbneg  10552  zsupss  10557  uzsupss  10560  uzwo3  10561  zmin  10562  zmax  10563  zbtwnre  10564  rebtwnz  10565  rpnnen1lem1  10592  rpnnen1lem2  10593  rpnnen1lem3  10594  rpnnen1lem4  10595  rpnnen1lem5  10596  reexALT  10598  elrp  10606  mnfltxr  10716  nn0pnfge0  10720  xrltnsym  10722  xrlttri  10724  xrlttr  10725  xrltletr  10739  xrletr  10740  ngtmnft  10747  xrltmin  10762  xrlemin  10764  ifle  10775  z2ge  10776  qbtwnre  10777  qbtwnxr  10778  qextlt  10781  qextle  10782  xltnegi  10794  xmullem2  10836  xmulasslem2  10853  xmulasslem  10856  xlemul1a  10859  xrsupexmnf  10875  xrsupsslem  10877  xrinfmsslem  10878  xrub  10882  supxrpnf  10889  supxrunb1  10890  supxrunb2  10891  ixxval  10916  elixx1  10917  elioo2  10949  iccid  10953  icc0  10956  iccsupr  10989  repos  10993  fzval  11037  elfz1  11040  flval  11195  flval2  11213  flval3  11214  uzsup  11236  modid2  11263  fsequb  11306  serge0  11369  expge0  11408  expge1  11409  facdiv  11570  facwordi  11572  hashkf  11612  hashnnn0genn0  11619  hashv01gt1  11621  hashdom  11645  hashnn0n0nn  11656  hashgt12el  11674  hashgt12el2  11675  brfi1uzind  11707  shftfib  11879  shftfn  11880  2shfti  11887  sqrlem3  12042  resqrex  12048  cau3lem  12150  caubnd2  12153  caubnd  12154  sqreu  12156  limsuple  12264  limsupval2  12266  rlim2  12282  climi  12296  rlimi  12299  ello12r  12303  ello1mpt  12307  ello1d  12309  lo1bdd2  12310  lo1bddrp  12311  elo12r  12314  o1lo1  12323  rlimclim1  12331  rlimdm  12337  climeu  12341  climmo  12343  2clim  12358  o1co  12372  o1compt  12373  addcn2  12379  mulcn2  12381  reccn2  12382  cn1lem  12383  rlimo1  12402  lo1add  12412  lo1mul  12413  climsup  12455  caucvgrlem  12458  caucvgb  12465  summo  12503  zsum  12504  fsum  12506  o1fsum  12584  climcnds  12623  supcvg  12627  rpnnen2lem4  12809  rpnnen  12818  ruclem2  12823  ruclem12  12832  sqr2irr  12840  dvdsabsb  12861  0dvds  12862  dvdsle  12887  alzdvds  12891  dvdsext  12892  fzo0dvdseq  12894  divalglem10  12914  bitsinv1lem  12945  sadadd3  12965  bitsuz  12978  gcdval  13000  gcdcllem1  13003  gcdcllem2  13004  gcddvds  13007  bezoutlem4  13033  dvdsgcd  13035  dvdssq  13052  isprm  13073  isprm2lem  13078  dvdsprm  13091  coprmdvds2  13095  isprm6  13101  exprmfct  13102  maxprmfct  13105  prmexpb  13109  prmfac1  13110  rpexp  13112  iserodd  13201  pceu  13212  pczpre  13213  pcdiv  13218  pcdvdsb  13234  pcmpt  13253  pcmptdvds  13255  prmpwdvds  13264  unbenlem  13268  infpnlem2  13271  infpn2  13273  prmreclem1  13276  prmreclem2  13277  prmreclem3  13278  prmreclem5  13280  prmreclem6  13281  vdwlem9  13349  vdwlem10  13350  vdwlem13  13353  ramz  13385  imasleval  13758  mreexexlem3d  13863  mreexexlem4d  13864  mreexexd  13865  prslem  14380  drsdirfi  14387  posi  14399  posasymb  14401  pleval2  14414  plttr  14419  pltletr  14420  pospo  14422  lubprop  14429  lubid  14431  glbprop  14434  glble  14435  joinlem  14439  joinle  14442  meetval2  14445  meetlem  14446  isglbd  14536  lubl  14539  lubun  14542  pospropd  14553  poslubmo  14565  poslubd  14566  tsrlin  14643  tsrlemax  14644  spwmo  14650  spwpr4  14655  letsr  14664  eqgen  14985  odeq  15180  odmulg  15184  pgpssslw  15240  sylow2alem2  15244  sylow2blem3  15248  efgval2  15348  efgsfo  15363  efgred  15372  efgredeu  15376  efgcpbllemb  15379  gexex  15460  cyggex2  15498  pgpfaclem1  15631  pgpfaclem2  15632  pgpfaclem3  15633  ablfaclem2  15636  ablfaclem3  15637  lidldvgen  16318  psrass1lem  16434  psrmulval  16442  mplmonmul  16519  opsrtoslem2  16537  coe1mul2  16654  coe1tmmul2fv  16662  coe1pwmulfv  16664  zndvds  16822  znleval  16827  ordtbaslem  17244  ordtbas2  17247  ordtopn1  17250  mnfnei  17277  ordtt1  17435  ordthauslem  17439  ordthmeolem  17825  trust  18251  ucncn  18307  imasdsf1olem  18395  comet  18535  stdbdxmet  18537  stdbdmet  18538  stdbdmopn  18540  metcnpi  18566  metcnpi2  18567  metcnpi3  18568  ngptgp  18669  nlmvscnlem1  18714  nrginvrcnlem  18718  nmogelb  18742  nmolb  18743  nghmcn  18771  xrsxmet  18832  icccmplem2  18846  icccmplem3  18847  reconnlem2  18850  xrge0tsms  18857  xmetdcn2  18860  metdsf  18870  metdsge  18871  metdscn  18878  metnrmlem1a  18880  addcnlem  18886  cncfi  18916  elcncf1di  18917  iccpnfhmeo  18962  xrhmeo  18963  cnllycmp  18973  evth  18976  ipcnlem1  19191  lmmcvg  19206  cfili  19213  cncmet  19267  minveclem1  19317  minveclem3b  19321  minveclem6  19327  pmltpclem1  19337  pmltpc  19339  ivthlem2  19341  ivthlem3  19342  cniccbdd  19350  ovolmge0  19365  ovolgelb  19368  ovolctb  19378  ovolunlem1  19385  ovoliunlem1  19390  ovoliun  19393  ovoliun2  19394  ovolshftlem1  19397  ovolscalem1  19401  ovolicc2lem3  19407  ovolicc2lem5  19409  ovolicc2  19410  voliunlem3  19438  ioombl1lem1  19444  ioombl1lem4  19447  uniioombllem2  19467  uniioombllem6  19472  volcn  19490  ismbfd  19524  mbfsup  19548  mbfinf  19549  mbflimsup  19550  itg1ge0  19570  itg1climres  19598  mbfi1fseqlem5  19603  itg2val  19612  itg2const  19624  itg2const2  19625  itg2seq  19626  itg2monolem1  19634  itg2i1fseq  19639  itg2i1fseq2  19640  itg2addlem  19642  itg2cnlem1  19645  itg2cnlem2  19646  itg2cn  19647  isibl  19649  ditgeq2  19728  dveflem  19855  dvferm1lem  19860  rolle  19866  c1lip1  19873  lhop1  19890  dvfsumlem2  19903  dvfsumlem4  19905  dvfsumrlim  19907  dvfsum2  19910  mdegmullem  19993  deg1leb  20010  deg1lt  20012  dvdsq1p  20075  plyeq0lem  20121  dgrco  20185  plydivex  20206  quotcan  20218  aannenlem1  20237  aannenlem2  20238  ulmi  20294  ulmcaulem  20302  ulmcau  20303  ulmbdd  20306  ulmdvlem3  20310  mtestbdd  20313  iblulm  20315  psercnlem1  20333  psercn  20334  abelthlem8  20347  sinhalfpilem  20366  logltb  20486  cxple2  20580  cxpcn3lem  20623  isosctrlem1  20654  leibpilem2  20773  cxploglim  20808  scvxcvx  20816  emcllem6  20831  ftalem3  20849  vmaval  20888  isppw2  20890  muval  20907  fsumdvdscom  20962  dvdsflf1o  20964  dvdsflsumcom  20965  musum  20968  muinv  20970  ppiublem1  20978  chtub  20988  logfac2  20993  bpos1lem  21058  bposlem9  21068  lgsdir  21106  lgsne0  21109  lgsqr  21122  lgsquadlem1  21130  lgsquadlem2  21131  lgsquadlem3  21132  2sqlem6  21145  2sqlem8  21148  2sqlem10  21150  dchrisumlema  21174  dchrisumlem2  21176  dchrisumlem3  21177  dchrvmasumiflem1  21187  dchrisum0fval  21191  dchrisum0ff  21193  dchrisum0flblem2  21195  logsqvma2  21229  pntrsumbnd2  21253  pntrlog2bndlem1  21263  pntpbnd1  21272  pntpbnd2  21273  pntibndlem2  21277  pntibndlem3  21278  pntibnd  21279  pntlemi  21290  pntlem3  21295  pntlemp  21296  pntleml  21297  pnt3  21298  uhgra0v  21337  usgra0v  21383  usgra1v  21401  cusgraexg  21470  sizeusglecusg  21487  usgramaxsize  21488  3v3e3cycl1  21623  4cycl4v4e  21645  4cycl4dv  21646  gxval  21838  vacn  22182  nmcvcn  22183  smcnlem  22185  nmobndi  22268  blocni  22298  ubthlem1  22364  ubthlem2  22365  ubthlem3  22366  minvecolem1  22368  minvecolem5  22375  minvecolem6  22376  htthlem  22412  norm3lemt  22646  hcaucvg  22680  hlimconvi  22685  hlim2  22686  chlimi  22729  hlimreui  22734  occl  22798  cmbr3  23102  cmcm  23108  cmcm3  23109  lecm  23111  cnopc  23408  cnfnc  23425  0cnop  23474  0cnfn  23475  idcnop  23476  nmopun  23509  nmcexi  23521  lnconi  23528  branmfn  23600  opsqrlem1  23635  pjnmopi  23643  pjnormssi  23663  stge1i  23733  strlem5  23750  hstrlem5  23758  mddmd2  23804  csmdsymi  23829  cvmd  23831  ela  23834  cvbr4i  23862  chirredlem3  23887  chirredlem4  23888  chirred  23890  atmd  23894  mdsym  23907  mddmdin0i  23926  cdj1i  23928  cdj3i  23936  fmptcof2  24068  isoun  24081  ishashinf  24151  tleile  24181  toslub  24183  tosglb  24184  xrge0tsmsd  24215  ofldadd  24230  ofldmul  24231  isinftm  24243  xrnarchi  24246  rge0scvg  24327  qqhcn  24367  qqhucn  24368  esumcst  24447  esumpinfval  24455  esumpcvgval  24460  esumcvg  24468  dstfrvunirn  24724  ballotlemfcc  24743  lgamgulmlem4  24808  lgamgulmlem5  24809  lgambdd  24813  subfacp1lem1  24857  relexpindlem  25131  relexpind  25132  rtrclreclem.trans  25138  dedekind  25179  dedekindle  25180  ntrivcvgn0  25218  ntrivcvgmullem  25221  prodmo  25254  zprod  25255  fprod  25259  fprodntriv  25260  dfpo2  25370  fundmpss  25382  funbreq  25387  dfpred3g  25442  predbrg  25453  poseq  25520  wzel  25567  wsuclem  25568  wsuclb  25571  nodenselem4  25631  nodenselem5  25632  nodense  25636  nocvxminlem  25637  nobndup  25647  nofulllem5  25653  brtxp  25717  brtxp2  25718  brpprod3a  25723  elfix  25740  sscoid  25750  elfuns  25752  fnsingle  25756  brimageg  25764  fnimage  25766  brdomaing  25772  brrangeg  25773  funpartlem  25779  axcontlem10  25904  fvtransport  25958  supaddc  26228  supadd  26229  mblfinlem  26234  mblfinlem2  26235  mblfinlem3  26236  ismblfin  26237  itg2addnclem  26246  itg2addnc  26249  itg2gt0cn  26250  ftc1anclem7  26276  ftc1anclem8  26277  ftc1anc  26278  trer  26310  elicc3  26311  finminlem  26312  nn0prpwlem  26316  nn0prpw  26317  fnessref  26364  refssfne  26365  fnemeet2  26387  filnetlem3  26400  frinfm  26428  fdc1  26441  nninfnub  26446  equivbnd  26490  heibor1lem  26509  heiborlem8  26518  iccbnd  26540  lzenom  26819  fphpdo  26869  rencldnfilem  26872  irrapxlem5  26880  irrapxlem6  26881  pellexlem3  26885  pellqrex  26933  pellfundre  26935  pellfundge  26936  pellfundlb  26938  pellfundglb  26939  monotoddzz  26997  oddcomabszz  26998  zindbi  27000  jm2.22  27057  jm2.23  27058  rpnnen3  27094  ttac  27098  fnwe2lem2  27117  aomclem8  27127  islinds  27247  hbtlem1  27295  hbtlem5  27300  xrltneNEW  27624  ubelsupr  27658  climinf  27699  stoweidlem14  27730  stoweidlem29  27745  stoweidlem31  27747  stoweidlem34  27750  stoweidlem49  27765  wallispilem3  27783  stirlinglem13  27802  stirlinglem14  27803  rlimdmafv  28008  swrdccatin12lem4  28179  isfrgra  28317  vdgfrgragt2  28355  frgrawopreglem2  28371  bnj1185  29102  bnj602  29223  bnj1228  29317  lubunNEW  29708  oposlem  29918  lub0N  29924  glb0N  29928  omllaw  29978  cvrval  30004  cvrnbtwn  30006  cvrnbtwn2  30010  cvrnbtwn3  30011  cvrcon3b  30012  cvrnbtwn4  30014  cvrcmp  30018  isat  30021  atnlt  30048  atlex  30051  cvlexch1  30063  cvlexchb1  30065  cvlatexch1  30071  glbconN  30111  2llnne2N  30142  cvratlem  30155  cvrat4  30177  ps-1  30211  3at  30224  islln  30240  llncmp  30256  llnnlt  30257  islpln  30264  islpln5  30269  lvolex3N  30272  lplncmp  30296  lplnexllnN  30298  lplnnlt  30299  islvol  30307  lvoli3  30311  islvol5  30313  lvolcmp  30351  lvolnltN  30352  dalem-cly  30405  dalem44  30450  pmapval  30491  pmapglbx  30503  lncvrelatN  30515  lncmp  30517  cdlemblem  30527  llnexchb2  30603  lautle  30818  lautcvr  30826  ldilset  30843  ltrnset  30852  trlset  30895  cdlemc4  30928  cdleme11dN  30996  cdleme20k  31053  cdleme21ct  31063  cdleme22b  31075  tendoex  31709  diafval  31766  diaval  31767  dicfval  31910  dihfval  31966  dihglblem2N  32029
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-rab 2706  df-v 2950  df-dif 3315  df-un 3317  df-in 3319  df-ss 3326  df-nul 3621  df-if 3732  df-sn 3812  df-pr 3813  df-op 3815  df-br 4205
  Copyright terms: Public domain W3C validator