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

Theorem breq2 4219
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 3987 . . 3  |-  ( A  =  B  ->  <. C ,  A >.  =  <. C ,  B >. )
21eleq1d 2504 . 2  |-  ( A  =  B  ->  ( <. C ,  A >.  e.  R  <->  <. C ,  B >.  e.  R ) )
3 df-br 4216 . 2  |-  ( C R A  <->  <. C ,  A >.  e.  R )
4 df-br 4216 . 2  |-  ( C R B  <->  <. C ,  B >.  e.  R )
52, 3, 43bitr4g 281 1  |-  ( A  =  B  ->  ( C R A  <->  C R B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178    = wceq 1653    e. wcel 1726   <.cop 3819   class class class wbr 4215
This theorem is referenced by:  breq12  4220  breq2i  4223  breq2d  4227  nbrne1  4232  pocl  4513  swopolem  4515  swopo  4516  solin  4529  sotric  4532  sotrieq  4533  isso2i  4538  somo  4540  seex  4548  frirr  4562  fr2nr  4563  frminex  4565  wereu2  4582  fr3nr  4763  dfwe2  4765  vtoclr  4925  posn  4949  frsn  4951  brcog  5042  brcogw  5044  opelcnvg  5055  dfdmf  5067  breldmg  5078  dfrnf  5111  dmcoss  5138  resieq  5159  dfres2  5196  elimag  5210  elrelimasn  5231  elimasn  5232  asymref2  5254  intirr  5255  poirr2  5261  sotri3  5267  poltletr  5272  soltmin  5276  dffun3  5468  dffun6f  5471  fun11  5519  brprcneu  5724  fv3  5747  tz6.12c  5753  tz6.12i  5754  funbrfv  5768  fnbrfvb  5770  funfv2f  5795  dffv2  5799  fndmdif  5837  dff3  5885  fmptco  5904  foeqcnvco  6030  isorel  6049  soisores  6050  soisoi  6051  isocnv  6053  isotr  6059  isopolem  6068  isosolem  6070  f1oiso  6074  f1oiso2  6075  f1oweALT  6077  caovordig  6255  caovordg  6257  caovord  6261  caofrss  6340  caoftrn  6342  frxp  6459  poxp  6461  tposoprab  6518  fvopab5  6537  ertr  6923  ecopovsym  7009  ecopovtrn  7010  th3qlem2  7014  domeng  7125  eqeng  7144  snfi  7190  sbth  7230  domunsn  7260  domssex  7271  nneneq  7293  php2  7295  onfin  7300  1sdom  7314  unxpdom  7319  isinf  7325  fineqvlem  7326  pssnn  7330  ssnnfi  7331  dif1enOLD  7343  dif1en  7344  findcard  7350  findcard2  7351  findcard3  7353  frfi  7355  fisupg  7358  nnsdomg  7369  unfi  7377  fiint  7386  supmo  7460  eqsup  7464  supub  7467  suplub  7468  suplub2  7469  supmaxlem  7472  fisup2g  7474  fisupcl  7475  suppr  7476  supisolem  7478  supisoex  7479  ordtypecbv  7489  ordtypelem3  7492  ordtypelem6  7495  ordtypelem7  7496  ordtypelem9  7498  wemaplem1  7518  wemaplem2  7519  harval  7533  wemapwe  7657  r111  7704  cardf2  7835  isnum2  7837  cardval3  7844  cardnueq0  7856  carden2a  7858  cardlim  7864  isinffi  7884  onsdom  7888  harval2  7889  cardmin2  7890  ondomen  7923  alephnbtwn  7957  alephinit  7981  aceq3lem  8006  infmap2  8103  cfslb2n  8153  sornom  8162  isfin4  8182  fin23lem26  8210  fin23lem27  8213  fin1a2lem11  8295  fin1a2lem12  8296  hsmex  8317  domtriomlem  8327  dominf  8330  zorn2lem2  8382  zorn2lem7  8387  zorn2g  8388  axdclem  8404  axdc  8406  fodomg  8408  brdom7disj  8414  brdom6disj  8415  cardmin  8444  ficard  8445  alephval2  8452  dominfac  8453  cfpwsdom  8464  gchi  8504  fpwwe2lem12  8521  fpwwe2lem13  8522  canthp1lem1  8532  canthp1lem2  8533  pwfseqlem4a  8541  pwfseqlem4  8542  elina  8567  winainflem  8573  eltskg  8630  rankcf  8657  indpi  8789  nqereu  8811  nsmallnq  8859  ltbtwnnq  8860  ltrnq  8861  prcdnq  8875  genpcd  8888  genpnmax  8889  ltaddpr2  8917  ltexprlem4  8921  prlem936  8929  reclem2pr  8930  reclem3pr  8931  supexpr  8936  ltsosr  8974  ltasr  8980  recexsrlem  8983  mulgt0sr  8985  map2psrpr  8990  supsrlem  8991  axpre-lttri  9045  axpre-lttrn  9046  axpre-ltadd  9047  axpre-mulgt0  9048  axpre-sup  9049  ltletr  9171  letr  9172  ltne  9175  eqle  9181  ltordlem  9557  elimgt0  9851  elimge0  9852  squeeze0  9918  fimaxre2  9961  lbreu  9963  lble  9965  sup2  9969  infm3  9972  suprlub  9975  supmul1  9978  supmullem1  9979  supmullem2  9980  supmul  9981  infmrcl  9992  infmrgelb  9993  nn2ge  10030  nnge1  10031  nnsub  10043  nominpos  10209  nnunb  10222  elnnnn0b  10269  nn0sub  10275  peano2uz2  10362  peano5uzi  10363  dfuzi  10365  uzind  10366  uzind3  10368  uzindOLD  10369  uzind3OLD  10370  eluz1  10497  uzind4  10539  uzwo  10544  uzwoOLD  10545  nnwof  10548  indstr2  10559  ublbneg  10565  zsupss  10570  uzsupss  10573  uzwo3  10574  zmin  10575  zmax  10576  zbtwnre  10577  rebtwnz  10578  rpnnen1lem1  10605  rpnnen1lem2  10606  rpnnen1lem3  10607  rpnnen1lem4  10608  rpnnen1lem5  10609  reexALT  10611  elrp  10619  mnfltxr  10729  nn0pnfge0  10733  xrltnsym  10735  xrlttri  10737  xrlttr  10738  xrltletr  10752  xrletr  10753  ngtmnft  10760  xrltmin  10775  xrlemin  10777  ifle  10788  z2ge  10789  qbtwnre  10790  qbtwnxr  10791  qextlt  10794  qextle  10795  xltnegi  10807  xmullem2  10849  xmulasslem2  10866  xmulasslem  10869  xlemul1a  10872  xrsupexmnf  10888  xrsupsslem  10890  xrinfmsslem  10891  xrub  10895  supxrpnf  10902  supxrunb1  10903  supxrunb2  10904  ixxval  10929  elixx1  10930  elioo2  10962  iccid  10966  icc0  10969  iccsupr  11002  repos  11006  fzval  11050  elfz1  11053  flval  11208  flval2  11226  flval3  11227  uzsup  11249  modid2  11276  fsequb  11319  serge0  11382  expge0  11421  expge1  11422  facdiv  11583  facwordi  11585  hashkf  11625  hashnnn0genn0  11632  hashv01gt1  11634  hashdom  11658  hashnn0n0nn  11669  hashgt12el  11687  hashgt12el2  11688  brfi1uzind  11720  shftfib  11892  shftfn  11893  2shfti  11900  sqrlem3  12055  resqrex  12061  cau3lem  12163  caubnd2  12166  caubnd  12167  sqreu  12169  limsuple  12277  limsupval2  12279  rlim2  12295  climi  12309  rlimi  12312  ello12r  12316  ello1mpt  12320  ello1d  12322  lo1bdd2  12323  lo1bddrp  12324  elo12r  12327  o1lo1  12336  rlimclim1  12344  rlimdm  12350  climeu  12354  climmo  12356  2clim  12371  o1co  12385  o1compt  12386  addcn2  12392  mulcn2  12394  reccn2  12395  cn1lem  12396  rlimo1  12415  lo1add  12425  lo1mul  12426  climsup  12468  caucvgrlem  12471  caucvgb  12478  summo  12516  zsum  12517  fsum  12519  o1fsum  12597  climcnds  12636  supcvg  12640  rpnnen2lem4  12822  rpnnen  12831  ruclem2  12836  ruclem12  12845  sqr2irr  12853  dvdsabsb  12874  0dvds  12875  dvdsle  12900  alzdvds  12904  dvdsext  12905  fzo0dvdseq  12907  divalglem10  12927  bitsinv1lem  12958  sadadd3  12978  bitsuz  12991  gcdval  13013  gcdcllem1  13016  gcdcllem2  13017  gcddvds  13020  bezoutlem4  13046  dvdsgcd  13048  dvdssq  13065  isprm  13086  isprm2lem  13091  dvdsprm  13104  coprmdvds2  13108  isprm6  13114  exprmfct  13115  maxprmfct  13118  prmexpb  13122  prmfac1  13123  rpexp  13125  iserodd  13214  pceu  13225  pczpre  13226  pcdiv  13231  pcdvdsb  13247  pcmpt  13266  pcmptdvds  13268  prmpwdvds  13277  unbenlem  13281  infpnlem2  13284  infpn2  13286  prmreclem1  13289  prmreclem2  13290  prmreclem3  13291  prmreclem5  13293  prmreclem6  13294  vdwlem9  13362  vdwlem10  13363  vdwlem13  13366  ramz  13398  imasleval  13771  mreexexlem3d  13876  mreexexlem4d  13877  mreexexd  13878  prslem  14393  drsdirfi  14400  posi  14412  posasymb  14414  pleval2  14427  plttr  14432  pltletr  14433  pospo  14435  lubprop  14442  lubid  14444  glbprop  14447  glble  14448  joinlem  14452  joinle  14455  meetval2  14458  meetlem  14459  isglbd  14549  lubl  14552  lubun  14555  pospropd  14566  poslubmo  14578  poslubd  14579  tsrlin  14656  tsrlemax  14657  spwmo  14663  spwpr4  14668  letsr  14677  eqgen  14998  odeq  15193  odmulg  15197  pgpssslw  15253  sylow2alem2  15257  sylow2blem3  15261  efgval2  15361  efgsfo  15376  efgred  15385  efgredeu  15389  efgcpbllemb  15392  gexex  15473  cyggex2  15511  pgpfaclem1  15644  pgpfaclem2  15645  pgpfaclem3  15646  ablfaclem2  15649  ablfaclem3  15650  lidldvgen  16331  psrass1lem  16447  psrmulval  16455  mplmonmul  16532  opsrtoslem2  16550  coe1mul2  16667  coe1tmmul2fv  16675  coe1pwmulfv  16677  zndvds  16835  znleval  16840  ordtbaslem  17257  ordtbas2  17260  ordtopn1  17263  mnfnei  17290  ordtt1  17448  ordthauslem  17452  ordthmeolem  17838  trust  18264  ucncn  18320  imasdsf1olem  18408  comet  18548  stdbdxmet  18550  stdbdmet  18551  stdbdmopn  18553  metcnpi  18579  metcnpi2  18580  metcnpi3  18581  ngptgp  18682  nlmvscnlem1  18727  nrginvrcnlem  18731  nmogelb  18755  nmolb  18756  nghmcn  18784  xrsxmet  18845  icccmplem2  18859  icccmplem3  18860  reconnlem2  18863  xrge0tsms  18870  xmetdcn2  18873  metdsf  18883  metdsge  18884  metdscn  18891  metnrmlem1a  18893  addcnlem  18899  cncfi  18929  elcncf1di  18930  iccpnfhmeo  18975  xrhmeo  18976  cnllycmp  18986  evth  18989  ipcnlem1  19204  lmmcvg  19219  cfili  19226  cncmet  19280  minveclem1  19330  minveclem3b  19334  minveclem6  19340  pmltpclem1  19350  pmltpc  19352  ivthlem2  19354  ivthlem3  19355  cniccbdd  19363  ovolmge0  19378  ovolgelb  19381  ovolctb  19391  ovolunlem1  19398  ovoliunlem1  19403  ovoliun  19406  ovoliun2  19407  ovolshftlem1  19410  ovolscalem1  19414  ovolicc2lem3  19420  ovolicc2lem5  19422  ovolicc2  19423  voliunlem3  19451  ioombl1lem1  19457  ioombl1lem4  19460  uniioombllem2  19480  uniioombllem6  19485  volcn  19503  ismbfd  19535  mbfsup  19559  mbfinf  19560  mbflimsup  19561  itg1ge0  19581  itg1climres  19609  mbfi1fseqlem5  19614  itg2val  19623  itg2const  19635  itg2const2  19636  itg2seq  19637  itg2monolem1  19645  itg2i1fseq  19650  itg2i1fseq2  19651  itg2addlem  19653  itg2cnlem1  19656  itg2cnlem2  19657  itg2cn  19658  isibl  19660  ditgeq2  19741  dveflem  19868  dvferm1lem  19873  rolle  19879  c1lip1  19886  lhop1  19903  dvfsumlem2  19916  dvfsumlem4  19918  dvfsumrlim  19920  dvfsum2  19923  mdegmullem  20006  deg1leb  20023  deg1lt  20025  dvdsq1p  20088  plyeq0lem  20134  dgrco  20198  plydivex  20219  quotcan  20231  aannenlem1  20250  aannenlem2  20251  ulmi  20307  ulmcaulem  20315  ulmcau  20316  ulmbdd  20319  ulmdvlem3  20323  mtestbdd  20326  iblulm  20328  psercnlem1  20346  psercn  20347  abelthlem8  20360  sinhalfpilem  20379  logltb  20499  cxple2  20593  cxpcn3lem  20636  isosctrlem1  20667  leibpilem2  20786  cxploglim  20821  scvxcvx  20829  emcllem6  20844  ftalem3  20862  vmaval  20901  isppw2  20903  muval  20920  fsumdvdscom  20975  dvdsflf1o  20977  dvdsflsumcom  20978  musum  20981  muinv  20983  ppiublem1  20991  chtub  21001  logfac2  21006  bpos1lem  21071  bposlem9  21081  lgsdir  21119  lgsne0  21122  lgsqr  21135  lgsquadlem1  21143  lgsquadlem2  21144  lgsquadlem3  21145  2sqlem6  21158  2sqlem8  21161  2sqlem10  21163  dchrisumlema  21187  dchrisumlem2  21189  dchrisumlem3  21190  dchrvmasumiflem1  21200  dchrisum0fval  21204  dchrisum0ff  21206  dchrisum0flblem2  21208  logsqvma2  21242  pntrsumbnd2  21266  pntrlog2bndlem1  21276  pntpbnd1  21285  pntpbnd2  21286  pntibndlem2  21290  pntibndlem3  21291  pntibnd  21292  pntlemi  21303  pntlem3  21308  pntlemp  21309  pntleml  21310  pnt3  21311  uhgra0v  21350  usgra0v  21396  usgra1v  21414  cusgraexg  21483  sizeusglecusg  21500  usgramaxsize  21501  3v3e3cycl1  21636  4cycl4v4e  21658  4cycl4dv  21659  gxval  21851  vacn  22195  nmcvcn  22196  smcnlem  22198  nmobndi  22281  blocni  22311  ubthlem1  22377  ubthlem2  22378  ubthlem3  22379  minvecolem1  22381  minvecolem5  22388  minvecolem6  22389  htthlem  22425  norm3lemt  22659  hcaucvg  22693  hlimconvi  22698  hlim2  22699  chlimi  22742  hlimreui  22747  occl  22811  cmbr3  23115  cmcm  23121  cmcm3  23122  lecm  23124  cnopc  23421  cnfnc  23438  0cnop  23487  0cnfn  23488  idcnop  23489  nmopun  23522  nmcexi  23534  lnconi  23541  branmfn  23613  opsqrlem1  23648  pjnmopi  23656  pjnormssi  23676  stge1i  23746  strlem5  23763  hstrlem5  23771  mddmd2  23817  csmdsymi  23842  cvmd  23844  ela  23847  cvbr4i  23875  chirredlem3  23900  chirredlem4  23901  chirred  23903  atmd  23907  mdsym  23920  mddmdin0i  23939  cdj1i  23941  cdj3i  23949  fmptcof2  24081  isoun  24094  ishashinf  24164  tleile  24194  toslub  24196  tosglb  24197  xrge0tsmsd  24228  ofldadd  24243  ofldmul  24244  isinftm  24256  xrnarchi  24259  rge0scvg  24340  qqhcn  24380  qqhucn  24381  esumcst  24460  esumpinfval  24468  esumpcvgval  24473  esumcvg  24481  dstfrvunirn  24737  ballotlemfcc  24756  lgamgulmlem4  24821  lgamgulmlem5  24822  lgambdd  24826  subfacp1lem1  24870  relexpindlem  25144  relexpind  25145  rtrclreclem.trans  25151  dedekind  25192  dedekindle  25193  ntrivcvgn0  25231  ntrivcvgmullem  25234  prodmo  25267  zprod  25268  fprod  25272  fprodntriv  25273  dfpo2  25383  fundmpss  25395  funbreq  25400  dfpred3g  25455  predbrg  25466  poseq  25533  wzel  25580  wsuclem  25581  wsuclb  25584  nodenselem4  25644  nodenselem5  25645  nodense  25649  nocvxminlem  25650  nobndup  25660  nofulllem5  25666  brtxp  25730  brtxp2  25731  brpprod3a  25736  elfix  25753  sscoid  25763  elfuns  25765  fnsingle  25769  brimageg  25777  fnimage  25779  brdomaing  25785  brrangeg  25786  funpartlem  25792  axcontlem10  25917  fvtransport  25971  supaddc  26245  supadd  26246  heicant  26253  mblfinlem1  26255  mblfinlem2  26256  mblfinlem3  26257  mblfinlem4  26258  ismblfin  26259  itg2addnclem  26270  itg2addnc  26273  itg2gt0cn  26274  ftc1anclem7  26300  ftc1anclem8  26301  ftc1anc  26302  trer  26333  elicc3  26334  finminlem  26335  nn0prpwlem  26339  nn0prpw  26340  fnessref  26387  refssfne  26388  fnemeet2  26410  filnetlem3  26423  frinfm  26451  fdc1  26464  nninfnub  26469  equivbnd  26513  heibor1lem  26532  heiborlem8  26541  iccbnd  26563  lzenom  26842  fphpdo  26892  rencldnfilem  26895  irrapxlem5  26903  irrapxlem6  26904  pellexlem3  26908  pellqrex  26956  pellfundre  26958  pellfundge  26959  pellfundlb  26961  pellfundglb  26962  monotoddzz  27020  oddcomabszz  27021  zindbi  27023  jm2.22  27080  jm2.23  27081  rpnnen3  27117  ttac  27121  fnwe2lem2  27140  aomclem8  27150  islinds  27270  hbtlem1  27318  hbtlem5  27323  xrltneNEW  27647  ubelsupr  27681  climinf  27722  stoweidlem14  27753  stoweidlem29  27768  stoweidlem31  27770  stoweidlem34  27773  stoweidlem49  27788  wallispilem3  27806  stirlinglem13  27825  stirlinglem14  27826  rlimdmafv  28031  hashss  28192  swrdccatin12lem4  28247  isfrgra  28454  vdgfrgragt2  28492  frgrawopreglem2  28508  bnj1185  29239  bnj602  29360  bnj1228  29454  lubunNEW  29845  oposlem  30055  lub0N  30061  glb0N  30065  omllaw  30115  cvrval  30141  cvrnbtwn  30143  cvrnbtwn2  30147  cvrnbtwn3  30148  cvrcon3b  30149  cvrnbtwn4  30151  cvrcmp  30155  isat  30158  atnlt  30185  atlex  30188  cvlexch1  30200  cvlexchb1  30202  cvlatexch1  30208  glbconN  30248  2llnne2N  30279  cvratlem  30292  cvrat4  30314  ps-1  30348  3at  30361  islln  30377  llncmp  30393  llnnlt  30394  islpln  30401  islpln5  30406  lvolex3N  30409  lplncmp  30433  lplnexllnN  30435  lplnnlt  30436  islvol  30444  lvoli3  30448  islvol5  30450  lvolcmp  30488  lvolnltN  30489  dalem-cly  30542  dalem44  30587  pmapval  30628  pmapglbx  30640  lncvrelatN  30652  lncmp  30654  cdlemblem  30664  llnexchb2  30740  lautle  30955  lautcvr  30963  ldilset  30980  ltrnset  30989  trlset  31032  cdlemc4  31065  cdleme11dN  31133  cdleme20k  31190  cdleme21ct  31200  cdleme22b  31212  tendoex  31846  diafval  31903  diaval  31904  dicfval  32047  dihfval  32103  dihglblem2N  32166
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-rab 2716  df-v 2960  df-dif 3325  df-un 3327  df-in 3329  df-ss 3336  df-nul 3631  df-if 3742  df-sn 3822  df-pr 3823  df-op 3825  df-br 4216
  Copyright terms: Public domain W3C validator