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

Theorem breq2 4027
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 3797 . . 3  |-  ( A  =  B  ->  <. C ,  A >.  =  <. C ,  B >. )
21eleq1d 2349 . 2  |-  ( A  =  B  ->  ( <. C ,  A >.  e.  R  <->  <. C ,  B >.  e.  R ) )
3 df-br 4024 . 2  |-  ( C R A  <->  <. C ,  A >.  e.  R )
4 df-br 4024 . 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 1623    e. wcel 1684   <.cop 3643   class class class wbr 4023
This theorem is referenced by:  breq12  4028  breq2i  4031  breq2d  4035  nbrne1  4040  pocl  4321  swopolem  4323  swopo  4324  solin  4337  sotric  4340  sotrieq  4341  isso2i  4346  somo  4348  seex  4356  frirr  4370  fr2nr  4371  frminex  4373  wereu2  4390  fr3nr  4571  dfwe2  4573  vtoclr  4733  posn  4758  frsn  4760  brcog  4850  opelcnvg  4861  dfdmf  4873  breldmg  4884  dfrnf  4917  dmcoss  4944  resieq  4965  dfres2  5002  elimag  5016  elrelimasn  5037  elimasn  5038  asymref2  5060  intirr  5061  poirr2  5067  sotri3  5073  poltletr  5078  soltmin  5082  dffun3  5266  dffun6f  5269  fun11  5315  brprcneu  5518  fv3  5541  tz6.12c  5547  tz6.12i  5548  funbrfv  5561  fnbrfvb  5563  funfv2f  5588  dffv2  5592  fndmdif  5629  dff3  5673  fmptco  5691  foeqcnvco  5804  isorel  5823  soisores  5824  soisoi  5825  isocnv  5827  isotr  5833  isopolem  5842  isosolem  5844  f1oiso  5848  f1oiso2  5849  f1oweALT  5851  caovordig  6025  caovordg  6027  caovord  6031  caofrss  6110  caoftrn  6112  frxp  6225  poxp  6227  tposoprab  6270  fvopab5  6289  ertr  6675  ecopovsym  6760  ecopovtrn  6761  th3qlem2  6765  domeng  6876  eqeng  6895  snfi  6941  sbth  6981  domunsn  7011  domssex  7022  nneneq  7044  php2  7046  onfin  7051  1sdom  7065  unxpdom  7070  isinf  7076  fineqvlem  7077  pssnn  7081  ssnnfi  7082  dif1enOLD  7090  dif1en  7091  findcard  7097  findcard2  7098  findcard3  7100  frfi  7102  fisupg  7105  nnsdomg  7116  unfi  7124  fiint  7133  supmo  7203  eqsup  7207  supub  7210  suplub  7211  suplub2  7212  supmaxlem  7215  fisup2g  7217  fisupcl  7218  suppr  7219  supisolem  7221  supisoex  7222  ordtypecbv  7232  ordtypelem3  7235  ordtypelem6  7238  ordtypelem7  7239  ordtypelem9  7241  wemaplem1  7261  wemaplem2  7262  harval  7276  wemapwe  7400  r111  7447  cardf2  7576  isnum2  7578  cardval3  7585  cardnueq0  7597  carden2a  7599  cardlim  7605  isinffi  7625  onsdom  7629  harval2  7630  cardmin2  7631  ondomen  7664  alephnbtwn  7698  alephinit  7722  aceq3lem  7747  infmap2  7844  cfslb2n  7894  sornom  7903  isfin4  7923  fin23lem26  7951  fin23lem27  7954  fin1a2lem11  8036  fin1a2lem12  8037  hsmex  8058  domtriomlem  8068  dominf  8071  zorn2lem2  8124  zorn2lem7  8129  zorn2g  8130  axdclem  8146  axdc  8148  fodomg  8150  brdom7disj  8156  brdom6disj  8157  cardmin  8186  ficard  8187  alephval2  8194  dominfac  8195  cfpwsdom  8206  gchi  8246  fpwwe2lem12  8263  fpwwe2lem13  8264  canthp1lem1  8274  canthp1lem2  8275  pwfseqlem4a  8283  pwfseqlem4  8284  elina  8309  winainflem  8315  eltskg  8372  rankcf  8399  indpi  8531  nqereu  8553  nsmallnq  8601  ltbtwnnq  8602  ltrnq  8603  prcdnq  8617  genpcd  8630  genpnmax  8631  ltaddpr2  8659  ltexprlem4  8663  prlem936  8671  reclem2pr  8672  reclem3pr  8673  supexpr  8678  ltsosr  8716  ltasr  8722  recexsrlem  8725  mulgt0sr  8727  map2psrpr  8732  supsrlem  8733  axpre-lttri  8787  axpre-lttrn  8788  axpre-ltadd  8789  axpre-mulgt0  8790  axpre-sup  8791  ltletr  8913  letr  8914  ltne  8917  eqle  8923  ltordlem  9298  elimgt0  9592  elimge0  9593  squeeze0  9659  fimaxre2  9702  lbreu  9704  lble  9706  lbinfm  9707  sup2  9710  infm3  9713  suprlub  9716  supmul1  9719  supmullem1  9720  supmullem2  9721  supmul  9722  infmrcl  9733  infmrgelb  9734  nn2ge  9771  nnge1  9772  nnsub  9784  nominpos  9948  nnunb  9961  elnnnn0b  10008  nn0sub  10014  peano2uz2  10099  peano5uzi  10100  dfuzi  10102  uzind  10103  uzind3  10105  uzindOLD  10106  uzind3OLD  10107  eluz1  10234  uzind4  10276  uzwo  10281  uzwoOLD  10282  nnwof  10285  indstr2  10296  ublbneg  10302  zsupss  10307  uzsupss  10310  uzwo3  10311  zmin  10312  zmax  10313  zbtwnre  10314  rebtwnz  10315  rpnnen1lem1  10342  rpnnen1lem2  10343  rpnnen1lem3  10344  rpnnen1lem4  10345  rpnnen1lem5  10346  reexALT  10348  elrp  10356  mnfltxr  10466  xrltnsym  10471  xrlttri  10473  xrlttr  10474  xrltletr  10488  xrletr  10489  ngtmnft  10496  xrltmin  10511  xrlemin  10513  ifle  10524  z2ge  10525  qbtwnre  10526  qbtwnxr  10527  qextlt  10530  qextle  10531  xltnegi  10543  xmullem2  10585  xmulasslem2  10602  xmulasslem  10605  xlemul1a  10608  xrsupexmnf  10623  xrsupsslem  10625  xrinfmsslem  10626  xrub  10630  supxrpnf  10637  supxrunb1  10638  supxrunb2  10639  ixxval  10664  elixx1  10665  elioo2  10697  iccid  10701  icc0  10704  iccsupr  10736  repos  10740  fzval  10784  elfz1  10787  flval  10926  flval2  10944  flval3  10945  uzsup  10967  modid2  10994  fsequb  11037  serge0  11100  expge0  11138  expge1  11139  facdiv  11300  facwordi  11302  hashkf  11339  hashdom  11361  shftfib  11567  shftfn  11568  2shfti  11575  sqrlem3  11730  resqrex  11736  cau3lem  11838  caubnd2  11841  caubnd  11842  sqreu  11844  limsuple  11952  limsupval2  11954  rlim2  11970  climi  11984  rlimi  11987  ello12r  11991  ello1mpt  11995  ello1d  11997  lo1bdd2  11998  lo1bddrp  11999  elo12r  12002  o1lo1  12011  rlimclim1  12019  rlimdm  12025  climeu  12029  climmo  12031  2clim  12046  o1co  12060  o1compt  12061  addcn2  12067  mulcn2  12069  reccn2  12070  cn1lem  12071  rlimo1  12090  lo1add  12100  lo1mul  12101  climsup  12143  caucvgrlem  12145  caucvgb  12152  summo  12190  zsum  12191  fsum  12193  o1fsum  12271  climcnds  12310  supcvg  12314  rpnnen2lem4  12496  rpnnen  12505  ruclem2  12510  ruclem12  12519  sqr2irr  12527  dvdsabsb  12548  0dvds  12549  dvdsle  12574  alzdvds  12578  dvdsext  12579  fzo0dvdseq  12581  divalglem10  12601  bitsinv1lem  12632  sadadd3  12652  bitsuz  12665  gcdval  12687  gcdcllem1  12690  gcdcllem2  12691  gcddvds  12694  bezoutlem4  12720  dvdsgcd  12722  dvdssq  12739  isprm  12760  isprm2lem  12765  dvdsprm  12778  coprmdvds2  12782  isprm6  12788  exprmfct  12789  maxprmfct  12792  prmexpb  12796  prmfac1  12797  rpexp  12799  iserodd  12888  pceu  12899  pczpre  12900  pcdiv  12905  pcdvdsb  12921  pcmpt  12940  pcmptdvds  12942  prmpwdvds  12951  unbenlem  12955  infpnlem2  12958  infpn2  12960  prmreclem1  12963  prmreclem2  12964  prmreclem3  12965  prmreclem5  12967  prmreclem6  12968  vdwlem9  13036  vdwlem10  13037  vdwlem13  13040  ramcl2lem  13056  ramz  13072  imasleval  13443  mreexexlem3d  13548  mreexexlem4d  13549  mreexexd  13550  prslem  14065  drsdirfi  14072  posi  14084  posasymb  14086  pleval2  14099  plttr  14104  pltletr  14105  pospo  14107  lubprop  14114  lubid  14116  glbprop  14119  glble  14120  joinlem  14124  joinle  14127  meetval2  14130  meetlem  14131  isglbd  14221  lubl  14224  lubun  14227  pospropd  14238  poslubmo  14250  poslubd  14251  tsrlin  14328  tsrlemax  14329  spwmo  14335  spwpr4  14340  letsr  14349  eqgen  14670  odeq  14865  odmulg  14869  pgpssslw  14925  sylow2alem2  14929  sylow2blem3  14933  efgval2  15033  efgsfo  15048  efgred  15057  efgredeu  15061  efgcpbllemb  15064  gexex  15145  cyggex2  15183  pgpfaclem1  15316  pgpfaclem2  15317  pgpfaclem3  15318  ablfaclem2  15321  ablfaclem3  15322  lidldvgen  16007  psrass1lem  16123  psrmulval  16131  mplmonmul  16208  opsrtoslem2  16226  coe1mul2  16346  coe1tmmul2fv  16354  coe1pwmulfv  16356  zndvds  16503  znleval  16508  ordtbaslem  16918  ordtbas2  16921  ordtopn1  16924  mnfnei  16951  ordtt1  17107  ordthauslem  17111  ordthmeolem  17492  imasdsf1olem  17937  comet  18059  stdbdxmet  18061  stdbdmet  18062  stdbdmopn  18064  metcnpi  18090  metcnpi2  18091  metcnpi3  18092  ngptgp  18152  nlmvscnlem1  18197  nrginvrcnlem  18201  nmogelb  18225  nmolb  18226  nghmcn  18254  xrsxmet  18315  icccmplem2  18328  icccmplem3  18329  reconnlem2  18332  xrge0tsms  18339  xmetdcn2  18342  metdsf  18352  metdsge  18353  metdscn  18360  metnrmlem1a  18362  addcnlem  18368  cncfi  18398  elcncf1di  18399  iccpnfhmeo  18443  xrhmeo  18444  cnllycmp  18454  evth  18457  ipcnlem1  18672  lmmcvg  18687  cfili  18694  cncmet  18744  minveclem1  18788  minveclem3b  18792  minveclem6  18798  pmltpclem1  18808  pmltpc  18810  ivthlem2  18812  ivthlem3  18813  cniccbdd  18821  ovolmge0  18836  ovolgelb  18839  ovolctb  18849  ovolunlem1  18856  ovoliunlem1  18861  ovoliun  18864  ovoliun2  18865  ovolshftlem1  18868  ovolscalem1  18872  ovolicc2lem3  18878  ovolicc2lem5  18880  ovolicc2  18881  voliunlem3  18909  ioombl1lem1  18915  ioombl1lem4  18918  uniioombllem2  18938  uniioombllem6  18943  volcn  18961  ismbfd  18995  mbfsup  19019  mbfinf  19020  mbflimsup  19021  itg1ge0  19041  itg1climres  19069  mbfi1fseqlem5  19074  itg2val  19083  itg2const  19095  itg2const2  19096  itg2seq  19097  itg2monolem1  19105  itg2i1fseq  19110  itg2i1fseq2  19111  itg2addlem  19113  itg2cnlem1  19116  itg2cnlem2  19117  itg2cn  19118  isibl  19120  ditgeq2  19199  dveflem  19326  dvferm1lem  19331  rolle  19337  c1lip1  19344  lhop1  19361  dvfsumlem2  19374  dvfsumlem4  19376  dvfsumrlim  19378  dvfsum2  19381  mdegmullem  19464  deg1leb  19481  deg1lt  19483  dvdsq1p  19546  plyeq0lem  19592  dgrco  19656  plydivex  19677  quotcan  19689  aannenlem1  19708  aannenlem2  19709  ulmi  19765  ulmcaulem  19771  ulmcau  19772  ulmbdd  19775  ulmdvlem3  19779  iblulm  19783  psercnlem1  19801  psercn  19802  abelthlem8  19815  sinhalfpilem  19834  logltb  19953  cxple2  20044  cxpcn3lem  20087  isosctrlem1  20118  leibpilem2  20237  cxploglim  20272  scvxcvx  20280  emcllem6  20294  ftalem3  20312  vmaval  20351  isppw2  20353  muval  20370  fsumdvdscom  20425  dvdsflf1o  20427  dvdsflsumcom  20428  musum  20431  muinv  20433  ppiublem1  20441  chtub  20451  logfac2  20456  bpos1lem  20521  bposlem9  20531  lgsdir  20569  lgsne0  20572  lgsqr  20585  lgsquadlem1  20593  lgsquadlem2  20594  lgsquadlem3  20595  2sqlem6  20608  2sqlem8  20611  2sqlem10  20613  dchrisumlema  20637  dchrisumlem2  20639  dchrisumlem3  20640  dchrvmasumiflem1  20650  dchrisum0fval  20654  dchrisum0ff  20656  dchrisum0flblem2  20658  logsqvma2  20692  pntrsumbnd2  20716  pntrlog2bndlem1  20726  pntpbnd1  20735  pntpbnd2  20736  pntibndlem2  20740  pntibndlem3  20741  pntibnd  20742  pntlemi  20753  pntlem3  20758  pntlemp  20759  pntleml  20760  pnt3  20761  gxval  20925  vacn  21267  nmcvcn  21268  smcnlem  21270  nmobndi  21353  blocni  21383  ubthlem1  21449  ubthlem2  21450  ubthlem3  21451  minvecolem1  21453  minvecolem5  21460  minvecolem6  21461  htthlem  21497  norm3lemt  21731  hcaucvg  21765  hlimconvi  21770  hlim2  21771  chlimi  21814  hlimreui  21819  occl  21883  cmbr3  22187  cmcm  22193  cmcm3  22194  lecm  22196  cnopc  22493  cnfnc  22510  0cnop  22559  0cnfn  22560  idcnop  22561  nmopun  22594  nmcexi  22606  lnconi  22613  branmfn  22685  opsqrlem1  22720  pjnmopi  22728  pjnormssi  22748  stge1i  22818  strlem5  22835  hstrlem5  22843  mddmd2  22889  csmdsymi  22914  cvmd  22916  ela  22919  cvbr4i  22947  chirredlem3  22972  chirredlem4  22973  chirred  22975  atmd  22979  mdsym  22992  mddmdin0i  23011  cdj1i  23013  cdj3i  23021  ballotlemfcc  23052  fmptcof2  23229  isoun  23242  rge0scvg  23373  xrge0tsmsd  23382  ishashinf  23389  esumcst  23436  esumpinfval  23441  esumpcvgval  23446  esumcvg  23454  dstfrvunirn  23675  subfacp1lem1  23710  relexpindlem  24036  relexpind  24037  rtrclreclem.trans  24043  dedekind  24082  dedekindle  24083  dfpo2  24112  fundmpss  24122  funbreq  24127  predbrg  24186  poseq  24253  nodenselem4  24338  nodenselem5  24339  nodense  24343  nocvxminlem  24344  nobndup  24354  nofulllem5  24360  brtxp  24420  brtxp2  24421  brpprod3a  24426  elfix  24443  dffun10  24453  fnsingle  24458  brimageg  24466  fnimage  24468  brdomaing  24474  brrangeg  24475  brcup  24478  brcap  24479  funpartfv  24483  axcontlem10  24601  fvtransport  24655  srefwref  25067  oriso  25214  puub2  25258  puub  25259  supdef  25262  ismnl2  25268  defge3  25271  inposet  25278  cntrset  25602  lvsovso  25626  trer  26227  elicc3  26228  finminlem  26231  nn0prpwlem  26238  nn0prpw  26239  fnessref  26293  refssfne  26294  fnemeet2  26316  filnetlem3  26329  frinfm  26416  fdc1  26456  nninfnub  26461  equivbnd  26514  heibor1lem  26533  heiborlem8  26542  iccbnd  26564  lzenom  26849  fphpdo  26900  rencldnfilem  26903  irrapxlem5  26911  irrapxlem6  26912  pellexlem3  26916  pellqrex  26964  pellfundre  26966  pellfundge  26967  pellfundlb  26969  pellfundglb  26970  monotoddzz  27028  oddcomabszz  27029  zindbi  27031  jm2.22  27088  jm2.23  27089  rpnnen3  27125  ttac  27129  fnwe2lem2  27148  aomclem8  27159  islinds  27279  hbtlem1  27327  hbtlem5  27332  xrltneNEW  27657  ubelsupr  27691  climinf  27732  stoweidlem14  27763  stoweidlem29  27778  stoweidlem31  27780  stoweidlem34  27783  stoweidlem49  27798  wallispilem3  27816  stirlinglem13  27835  stirlinglem14  27836  usgra0v  28117  usgra1v  28126  isfrgra  28171  bnj1185  28826  bnj602  28947  bnj1228  29041  lubunNEW  29163  oposlem  29373  lub0N  29379  glb0N  29383  omllaw  29433  cvrval  29459  cvrnbtwn  29461  cvrnbtwn2  29465  cvrnbtwn3  29466  cvrcon3b  29467  cvrnbtwn4  29469  cvrcmp  29473  isat  29476  atnlt  29503  atlex  29506  cvlexch1  29518  cvlexchb1  29520  cvlatexch1  29526  glbconN  29566  2llnne2N  29597  cvratlem  29610  cvrat4  29632  ps-1  29666  3at  29679  islln  29695  llncmp  29711  llnnlt  29712  islpln  29719  islpln5  29724  lvolex3N  29727  lplncmp  29751  lplnexllnN  29753  lplnnlt  29754  islvol  29762  lvoli3  29766  islvol5  29768  lvolcmp  29806  lvolnltN  29807  dalem-cly  29860  dalem44  29905  pmapval  29946  pmapglbx  29958  lncvrelatN  29970  lncmp  29972  cdlemblem  29982  llnexchb2  30058  lautle  30273  lautcvr  30281  ldilset  30298  ltrnset  30307  trlset  30350  cdlemc4  30383  cdleme11dN  30451  cdleme20k  30508  cdleme21ct  30518  cdleme22b  30530  tendoex  31164  diafval  31221  diaval  31222  dicfval  31365  dihfval  31421  dihglblem2N  31484
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-rab 2552  df-v 2790  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-br 4024
  Copyright terms: Public domain W3C validator