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

Theorem breq2 4216
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 3985 . . 3  |-  ( A  =  B  ->  <. C ,  A >.  =  <. C ,  B >. )
21eleq1d 2502 . 2  |-  ( A  =  B  ->  ( <. C ,  A >.  e.  R  <->  <. C ,  B >.  e.  R ) )
3 df-br 4213 . 2  |-  ( C R A  <->  <. C ,  A >.  e.  R )
4 df-br 4213 . 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 3817   class class class wbr 4212
This theorem is referenced by:  breq12  4217  breq2i  4220  breq2d  4224  nbrne1  4229  pocl  4510  swopolem  4512  swopo  4513  solin  4526  sotric  4529  sotrieq  4530  isso2i  4535  somo  4537  seex  4545  frirr  4559  fr2nr  4560  frminex  4562  wereu2  4579  fr3nr  4760  dfwe2  4762  vtoclr  4922  posn  4946  frsn  4948  brcog  5039  brcogw  5041  opelcnvg  5052  dfdmf  5064  breldmg  5075  dfrnf  5108  dmcoss  5135  resieq  5156  dfres2  5193  elimag  5207  elrelimasn  5228  elimasn  5229  asymref2  5251  intirr  5252  poirr2  5258  sotri3  5264  poltletr  5269  soltmin  5273  dffun3  5465  dffun6f  5468  fun11  5516  brprcneu  5721  fv3  5744  tz6.12c  5750  tz6.12i  5751  funbrfv  5765  fnbrfvb  5767  funfv2f  5792  dffv2  5796  fndmdif  5834  dff3  5882  fmptco  5901  foeqcnvco  6027  isorel  6046  soisores  6047  soisoi  6048  isocnv  6050  isotr  6056  isopolem  6065  isosolem  6067  f1oiso  6071  f1oiso2  6072  f1oweALT  6074  caovordig  6252  caovordg  6254  caovord  6258  caofrss  6337  caoftrn  6339  frxp  6456  poxp  6458  tposoprab  6515  fvopab5  6534  ertr  6920  ecopovsym  7006  ecopovtrn  7007  th3qlem2  7011  domeng  7122  eqeng  7141  snfi  7187  sbth  7227  domunsn  7257  domssex  7268  nneneq  7290  php2  7292  onfin  7297  1sdom  7311  unxpdom  7316  isinf  7322  fineqvlem  7323  pssnn  7327  ssnnfi  7328  dif1enOLD  7340  dif1en  7341  findcard  7347  findcard2  7348  findcard3  7350  frfi  7352  fisupg  7355  nnsdomg  7366  unfi  7374  fiint  7383  supmo  7457  eqsup  7461  supub  7464  suplub  7465  suplub2  7466  supmaxlem  7469  fisup2g  7471  fisupcl  7472  suppr  7473  supisolem  7475  supisoex  7476  ordtypecbv  7486  ordtypelem3  7489  ordtypelem6  7492  ordtypelem7  7493  ordtypelem9  7495  wemaplem1  7515  wemaplem2  7516  harval  7530  wemapwe  7654  r111  7701  cardf2  7830  isnum2  7832  cardval3  7839  cardnueq0  7851  carden2a  7853  cardlim  7859  isinffi  7879  onsdom  7883  harval2  7884  cardmin2  7885  ondomen  7918  alephnbtwn  7952  alephinit  7976  aceq3lem  8001  infmap2  8098  cfslb2n  8148  sornom  8157  isfin4  8177  fin23lem26  8205  fin23lem27  8208  fin1a2lem11  8290  fin1a2lem12  8291  hsmex  8312  domtriomlem  8322  dominf  8325  zorn2lem2  8377  zorn2lem7  8382  zorn2g  8383  axdclem  8399  axdc  8401  fodomg  8403  brdom7disj  8409  brdom6disj  8410  cardmin  8439  ficard  8440  alephval2  8447  dominfac  8448  cfpwsdom  8459  gchi  8499  fpwwe2lem12  8516  fpwwe2lem13  8517  canthp1lem1  8527  canthp1lem2  8528  pwfseqlem4a  8536  pwfseqlem4  8537  elina  8562  winainflem  8568  eltskg  8625  rankcf  8652  indpi  8784  nqereu  8806  nsmallnq  8854  ltbtwnnq  8855  ltrnq  8856  prcdnq  8870  genpcd  8883  genpnmax  8884  ltaddpr2  8912  ltexprlem4  8916  prlem936  8924  reclem2pr  8925  reclem3pr  8926  supexpr  8931  ltsosr  8969  ltasr  8975  recexsrlem  8978  mulgt0sr  8980  map2psrpr  8985  supsrlem  8986  axpre-lttri  9040  axpre-lttrn  9041  axpre-ltadd  9042  axpre-mulgt0  9043  axpre-sup  9044  ltletr  9166  letr  9167  ltne  9170  eqle  9176  ltordlem  9552  elimgt0  9846  elimge0  9847  squeeze0  9913  fimaxre2  9956  lbreu  9958  lble  9960  sup2  9964  infm3  9967  suprlub  9970  supmul1  9973  supmullem1  9974  supmullem2  9975  supmul  9976  infmrcl  9987  infmrgelb  9988  nn2ge  10025  nnge1  10026  nnsub  10038  nominpos  10204  nnunb  10217  elnnnn0b  10264  nn0sub  10270  peano2uz2  10357  peano5uzi  10358  dfuzi  10360  uzind  10361  uzind3  10363  uzindOLD  10364  uzind3OLD  10365  eluz1  10492  uzind4  10534  uzwo  10539  uzwoOLD  10540  nnwof  10543  indstr2  10554  ublbneg  10560  zsupss  10565  uzsupss  10568  uzwo3  10569  zmin  10570  zmax  10571  zbtwnre  10572  rebtwnz  10573  rpnnen1lem1  10600  rpnnen1lem2  10601  rpnnen1lem3  10602  rpnnen1lem4  10603  rpnnen1lem5  10604  reexALT  10606  elrp  10614  mnfltxr  10724  nn0pnfge0  10728  xrltnsym  10730  xrlttri  10732  xrlttr  10733  xrltletr  10747  xrletr  10748  ngtmnft  10755  xrltmin  10770  xrlemin  10772  ifle  10783  z2ge  10784  qbtwnre  10785  qbtwnxr  10786  qextlt  10789  qextle  10790  xltnegi  10802  xmullem2  10844  xmulasslem2  10861  xmulasslem  10864  xlemul1a  10867  xrsupexmnf  10883  xrsupsslem  10885  xrinfmsslem  10886  xrub  10890  supxrpnf  10897  supxrunb1  10898  supxrunb2  10899  ixxval  10924  elixx1  10925  elioo2  10957  iccid  10961  icc0  10964  iccsupr  10997  repos  11001  fzval  11045  elfz1  11048  flval  11203  flval2  11221  flval3  11222  uzsup  11244  modid2  11271  fsequb  11314  serge0  11377  expge0  11416  expge1  11417  facdiv  11578  facwordi  11580  hashkf  11620  hashnnn0genn0  11627  hashv01gt1  11629  hashdom  11653  hashnn0n0nn  11664  hashgt12el  11682  hashgt12el2  11683  brfi1uzind  11715  shftfib  11887  shftfn  11888  2shfti  11895  sqrlem3  12050  resqrex  12056  cau3lem  12158  caubnd2  12161  caubnd  12162  sqreu  12164  limsuple  12272  limsupval2  12274  rlim2  12290  climi  12304  rlimi  12307  ello12r  12311  ello1mpt  12315  ello1d  12317  lo1bdd2  12318  lo1bddrp  12319  elo12r  12322  o1lo1  12331  rlimclim1  12339  rlimdm  12345  climeu  12349  climmo  12351  2clim  12366  o1co  12380  o1compt  12381  addcn2  12387  mulcn2  12389  reccn2  12390  cn1lem  12391  rlimo1  12410  lo1add  12420  lo1mul  12421  climsup  12463  caucvgrlem  12466  caucvgb  12473  summo  12511  zsum  12512  fsum  12514  o1fsum  12592  climcnds  12631  supcvg  12635  rpnnen2lem4  12817  rpnnen  12826  ruclem2  12831  ruclem12  12840  sqr2irr  12848  dvdsabsb  12869  0dvds  12870  dvdsle  12895  alzdvds  12899  dvdsext  12900  fzo0dvdseq  12902  divalglem10  12922  bitsinv1lem  12953  sadadd3  12973  bitsuz  12986  gcdval  13008  gcdcllem1  13011  gcdcllem2  13012  gcddvds  13015  bezoutlem4  13041  dvdsgcd  13043  dvdssq  13060  isprm  13081  isprm2lem  13086  dvdsprm  13099  coprmdvds2  13103  isprm6  13109  exprmfct  13110  maxprmfct  13113  prmexpb  13117  prmfac1  13118  rpexp  13120  iserodd  13209  pceu  13220  pczpre  13221  pcdiv  13226  pcdvdsb  13242  pcmpt  13261  pcmptdvds  13263  prmpwdvds  13272  unbenlem  13276  infpnlem2  13279  infpn2  13281  prmreclem1  13284  prmreclem2  13285  prmreclem3  13286  prmreclem5  13288  prmreclem6  13289  vdwlem9  13357  vdwlem10  13358  vdwlem13  13361  ramz  13393  imasleval  13766  mreexexlem3d  13871  mreexexlem4d  13872  mreexexd  13873  prslem  14388  drsdirfi  14395  posi  14407  posasymb  14409  pleval2  14422  plttr  14427  pltletr  14428  pospo  14430  lubprop  14437  lubid  14439  glbprop  14442  glble  14443  joinlem  14447  joinle  14450  meetval2  14453  meetlem  14454  isglbd  14544  lubl  14547  lubun  14550  pospropd  14561  poslubmo  14573  poslubd  14574  tsrlin  14651  tsrlemax  14652  spwmo  14658  spwpr4  14663  letsr  14672  eqgen  14993  odeq  15188  odmulg  15192  pgpssslw  15248  sylow2alem2  15252  sylow2blem3  15256  efgval2  15356  efgsfo  15371  efgred  15380  efgredeu  15384  efgcpbllemb  15387  gexex  15468  cyggex2  15506  pgpfaclem1  15639  pgpfaclem2  15640  pgpfaclem3  15641  ablfaclem2  15644  ablfaclem3  15645  lidldvgen  16326  psrass1lem  16442  psrmulval  16450  mplmonmul  16527  opsrtoslem2  16545  coe1mul2  16662  coe1tmmul2fv  16670  coe1pwmulfv  16672  zndvds  16830  znleval  16835  ordtbaslem  17252  ordtbas2  17255  ordtopn1  17258  mnfnei  17285  ordtt1  17443  ordthauslem  17447  ordthmeolem  17833  trust  18259  ucncn  18315  imasdsf1olem  18403  comet  18543  stdbdxmet  18545  stdbdmet  18546  stdbdmopn  18548  metcnpi  18574  metcnpi2  18575  metcnpi3  18576  ngptgp  18677  nlmvscnlem1  18722  nrginvrcnlem  18726  nmogelb  18750  nmolb  18751  nghmcn  18779  xrsxmet  18840  icccmplem2  18854  icccmplem3  18855  reconnlem2  18858  xrge0tsms  18865  xmetdcn2  18868  metdsf  18878  metdsge  18879  metdscn  18886  metnrmlem1a  18888  addcnlem  18894  cncfi  18924  elcncf1di  18925  iccpnfhmeo  18970  xrhmeo  18971  cnllycmp  18981  evth  18984  ipcnlem1  19199  lmmcvg  19214  cfili  19221  cncmet  19275  minveclem1  19325  minveclem3b  19329  minveclem6  19335  pmltpclem1  19345  pmltpc  19347  ivthlem2  19349  ivthlem3  19350  cniccbdd  19358  ovolmge0  19373  ovolgelb  19376  ovolctb  19386  ovolunlem1  19393  ovoliunlem1  19398  ovoliun  19401  ovoliun2  19402  ovolshftlem1  19405  ovolscalem1  19409  ovolicc2lem3  19415  ovolicc2lem5  19417  ovolicc2  19418  voliunlem3  19446  ioombl1lem1  19452  ioombl1lem4  19455  uniioombllem2  19475  uniioombllem6  19480  volcn  19498  ismbfd  19532  mbfsup  19556  mbfinf  19557  mbflimsup  19558  itg1ge0  19578  itg1climres  19606  mbfi1fseqlem5  19611  itg2val  19620  itg2const  19632  itg2const2  19633  itg2seq  19634  itg2monolem1  19642  itg2i1fseq  19647  itg2i1fseq2  19648  itg2addlem  19650  itg2cnlem1  19653  itg2cnlem2  19654  itg2cn  19655  isibl  19657  ditgeq2  19736  dveflem  19863  dvferm1lem  19868  rolle  19874  c1lip1  19881  lhop1  19898  dvfsumlem2  19911  dvfsumlem4  19913  dvfsumrlim  19915  dvfsum2  19918  mdegmullem  20001  deg1leb  20018  deg1lt  20020  dvdsq1p  20083  plyeq0lem  20129  dgrco  20193  plydivex  20214  quotcan  20226  aannenlem1  20245  aannenlem2  20246  ulmi  20302  ulmcaulem  20310  ulmcau  20311  ulmbdd  20314  ulmdvlem3  20318  mtestbdd  20321  iblulm  20323  psercnlem1  20341  psercn  20342  abelthlem8  20355  sinhalfpilem  20374  logltb  20494  cxple2  20588  cxpcn3lem  20631  isosctrlem1  20662  leibpilem2  20781  cxploglim  20816  scvxcvx  20824  emcllem6  20839  ftalem3  20857  vmaval  20896  isppw2  20898  muval  20915  fsumdvdscom  20970  dvdsflf1o  20972  dvdsflsumcom  20973  musum  20976  muinv  20978  ppiublem1  20986  chtub  20996  logfac2  21001  bpos1lem  21066  bposlem9  21076  lgsdir  21114  lgsne0  21117  lgsqr  21130  lgsquadlem1  21138  lgsquadlem2  21139  lgsquadlem3  21140  2sqlem6  21153  2sqlem8  21156  2sqlem10  21158  dchrisumlema  21182  dchrisumlem2  21184  dchrisumlem3  21185  dchrvmasumiflem1  21195  dchrisum0fval  21199  dchrisum0ff  21201  dchrisum0flblem2  21203  logsqvma2  21237  pntrsumbnd2  21261  pntrlog2bndlem1  21271  pntpbnd1  21280  pntpbnd2  21281  pntibndlem2  21285  pntibndlem3  21286  pntibnd  21287  pntlemi  21298  pntlem3  21303  pntlemp  21304  pntleml  21305  pnt3  21306  uhgra0v  21345  usgra0v  21391  usgra1v  21409  cusgraexg  21478  sizeusglecusg  21495  usgramaxsize  21496  3v3e3cycl1  21631  4cycl4v4e  21653  4cycl4dv  21654  gxval  21846  vacn  22190  nmcvcn  22191  smcnlem  22193  nmobndi  22276  blocni  22306  ubthlem1  22372  ubthlem2  22373  ubthlem3  22374  minvecolem1  22376  minvecolem5  22383  minvecolem6  22384  htthlem  22420  norm3lemt  22654  hcaucvg  22688  hlimconvi  22693  hlim2  22694  chlimi  22737  hlimreui  22742  occl  22806  cmbr3  23110  cmcm  23116  cmcm3  23117  lecm  23119  cnopc  23416  cnfnc  23433  0cnop  23482  0cnfn  23483  idcnop  23484  nmopun  23517  nmcexi  23529  lnconi  23536  branmfn  23608  opsqrlem1  23643  pjnmopi  23651  pjnormssi  23671  stge1i  23741  strlem5  23758  hstrlem5  23766  mddmd2  23812  csmdsymi  23837  cvmd  23839  ela  23842  cvbr4i  23870  chirredlem3  23895  chirredlem4  23896  chirred  23898  atmd  23902  mdsym  23915  mddmdin0i  23934  cdj1i  23936  cdj3i  23944  fmptcof2  24076  isoun  24089  ishashinf  24159  tleile  24189  toslub  24191  tosglb  24192  xrge0tsmsd  24223  ofldadd  24238  ofldmul  24239  isinftm  24251  xrnarchi  24254  rge0scvg  24335  qqhcn  24375  qqhucn  24376  esumcst  24455  esumpinfval  24463  esumpcvgval  24468  esumcvg  24476  dstfrvunirn  24732  ballotlemfcc  24751  lgamgulmlem4  24816  lgamgulmlem5  24817  lgambdd  24821  subfacp1lem1  24865  relexpindlem  25139  relexpind  25140  rtrclreclem.trans  25146  dedekind  25187  dedekindle  25188  ntrivcvgn0  25226  ntrivcvgmullem  25229  prodmo  25262  zprod  25263  fprod  25267  fprodntriv  25268  dfpo2  25378  fundmpss  25390  funbreq  25395  dfpred3g  25450  predbrg  25461  poseq  25528  wzel  25575  wsuclem  25576  wsuclb  25579  nodenselem4  25639  nodenselem5  25640  nodense  25644  nocvxminlem  25645  nobndup  25655  nofulllem5  25661  brtxp  25725  brtxp2  25726  brpprod3a  25731  elfix  25748  sscoid  25758  elfuns  25760  fnsingle  25764  brimageg  25772  fnimage  25774  brdomaing  25780  brrangeg  25781  funpartlem  25787  axcontlem10  25912  fvtransport  25966  supaddc  26237  supadd  26238  mblfinlem1  26243  mblfinlem2  26244  mblfinlem3  26245  mblfinlem4  26246  ismblfin  26247  itg2addnclem  26256  itg2addnc  26259  itg2gt0cn  26260  ftc1anclem7  26286  ftc1anclem8  26287  ftc1anc  26288  trer  26319  elicc3  26320  finminlem  26321  nn0prpwlem  26325  nn0prpw  26326  fnessref  26373  refssfne  26374  fnemeet2  26396  filnetlem3  26409  frinfm  26437  fdc1  26450  nninfnub  26455  equivbnd  26499  heibor1lem  26518  heiborlem8  26527  iccbnd  26549  lzenom  26828  fphpdo  26878  rencldnfilem  26881  irrapxlem5  26889  irrapxlem6  26890  pellexlem3  26894  pellqrex  26942  pellfundre  26944  pellfundge  26945  pellfundlb  26947  pellfundglb  26948  monotoddzz  27006  oddcomabszz  27007  zindbi  27009  jm2.22  27066  jm2.23  27067  rpnnen3  27103  ttac  27107  fnwe2lem2  27126  aomclem8  27136  islinds  27256  hbtlem1  27304  hbtlem5  27309  xrltneNEW  27633  ubelsupr  27667  climinf  27708  stoweidlem14  27739  stoweidlem29  27754  stoweidlem31  27756  stoweidlem34  27759  stoweidlem49  27774  wallispilem3  27792  stirlinglem13  27811  stirlinglem14  27812  rlimdmafv  28017  swrdccatin12lem4  28213  isfrgra  28380  vdgfrgragt2  28418  frgrawopreglem2  28434  bnj1185  29165  bnj602  29286  bnj1228  29380  lubunNEW  29771  oposlem  29981  lub0N  29987  glb0N  29991  omllaw  30041  cvrval  30067  cvrnbtwn  30069  cvrnbtwn2  30073  cvrnbtwn3  30074  cvrcon3b  30075  cvrnbtwn4  30077  cvrcmp  30081  isat  30084  atnlt  30111  atlex  30114  cvlexch1  30126  cvlexchb1  30128  cvlatexch1  30134  glbconN  30174  2llnne2N  30205  cvratlem  30218  cvrat4  30240  ps-1  30274  3at  30287  islln  30303  llncmp  30319  llnnlt  30320  islpln  30327  islpln5  30332  lvolex3N  30335  lplncmp  30359  lplnexllnN  30361  lplnnlt  30362  islvol  30370  lvoli3  30374  islvol5  30376  lvolcmp  30414  lvolnltN  30415  dalem-cly  30468  dalem44  30513  pmapval  30554  pmapglbx  30566  lncvrelatN  30578  lncmp  30580  cdlemblem  30590  llnexchb2  30666  lautle  30881  lautcvr  30889  ldilset  30906  ltrnset  30915  trlset  30958  cdlemc4  30991  cdleme11dN  31059  cdleme20k  31116  cdleme21ct  31126  cdleme22b  31138  tendoex  31772  diafval  31829  diaval  31830  dicfval  31973  dihfval  32029  dihglblem2N  32092
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 2417
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 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-rab 2714  df-v 2958  df-dif 3323  df-un 3325  df-in 3327  df-ss 3334  df-nul 3629  df-if 3740  df-sn 3820  df-pr 3821  df-op 3823  df-br 4213
  Copyright terms: Public domain W3C validator