Theorem breq2 3985

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

Step	Hyp	Ref	Expression
1		opeq2 3758	. . 3 |- ( A = B -> <. C , A >. = <. C , B >. )
2	1	eleq1d 2234	. 2 |- ( A = B -> ( <. C , A >. e. R <-> <. C , B >. e. R ) )
3		df-br 3982	. 2 |- ( C R A <-> <. C , A >. e. R )
4		df-br 3982	. 2 |- ( C R B <-> <. C , B >. e. R )
5	2, 3, 4	3bitr4g 222	1 |- ( A = B -> ( C R A <-> C R B ) )

Syntax hints:   -> wi 4   <-> wb 104   = wceq 1343   e. wcel 2136   <.cop 3578   class class class wbr 3981

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-10 1493  ax-11 1494  ax-i12 1495  ax-bndl 1497  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-3an 970  df-tru 1346  df-nf 1449  df-sb 1751  df-clab 2152  df-cleq 2158  df-clel 2161  df-nfc 2296  df-v 2727  df-un 3119  df-sn 3581  df-pr 3582  df-op 3584  df-br 3982

This theorem is referenced by:  breq12  3986  breq2i  3989  breq2d  3993  nbrne1  4000  brralrspcev  4039  brimralrspcev  4040  pocl  4280  swopolem  4282  swopo  4283  sowlin  4297  sotricim  4300  sotritrieq  4302  seex  4312  frind  4329  wetriext  4553  vtoclr  4651  posng  4675  brcog  4770  brcogw  4772  opelcnvg  4783  dfdmf  4796  breldmg  4809  dfrnf  4844  dmcoss  4872  resieq  4893  dfres2  4935  elimag  4949  elreimasng  4969  elimasn  4970  intirr  4989  poirr2  4995  poltletr  5003  dffun6f  5200  dffun4f  5203  fun11  5254  brprcneu  5478  fv3  5508  tz6.12c  5515  relelfvdm  5517  funbrfv  5524  fnbrfvb  5526  funfvdm2f  5550  fndmdif  5589  dff3im  5629  fmptco  5650  foeqcnvco  5757  isorel  5775  isocnv  5778  isotr  5783  isopolem  5789  isosolem  5791  f1oiso  5793  f1oiso2  5794  caovordig  6003  caovordg  6005  caovord  6009  caofrss  6073  caoftrn  6074  poxp  6196  tposoprab  6244  ertr  6512  ecopovsym  6593  ecopovtrn  6594  ecopovsymg  6596  ecopovtrng  6597  th3qlem2  6600  domeng  6714  eqeng  6728  snfig  6776  nneneq  6819  nnfi  6834  ssfilem  6837  domfiexmid  6840  dif1enen  6842  diffitest  6849  findcard  6850  findcard2  6851  findcard2s  6852  diffisn  6855  tridc  6861  fimax2gtrilemstep  6862  inffiexmid  6868  unsnfi  6880  fiintim  6890  fisseneq  6893  isbth  6928  supmoti  6954  eqsupti  6957  supubti  6960  suplubti  6961  suplub2ti  6962  supmaxti  6965  supsnti  6966  isotilem  6967  isoti  6968  supisolem  6969  supisoex  6970  cardcl  7133  isnumi  7134  cardval3ex  7137  exmidfodomrlemr  7154  exmidfodomrlemrALT  7155  nqtri3or  7333  ltsonq  7335  ltanqg  7337  ltmnqg  7338  ltexnqq  7345  nsmallnqq  7349  subhalfnqq  7351  ltbtwnnqq  7352  prarloclemarch2  7356  nqnq0pi  7375  prcdnql  7421  prcunqu  7422  prnminu  7426  genpcdl  7456  genprndl  7458  genprndu  7459  genpdisj  7460  nqprm  7479  nqprrnd  7480  nqprdisj  7481  nqprloc  7482  nqprlu  7484  nqprl  7488  addnqprlemru  7495  addnqprlemfl  7496  addnqprlemfu  7497  mulnqprlemru  7511  mulnqprlemfl  7512  mulnqprlemfu  7513  1idpru  7528  ltnqpr  7530  ltnqpri  7531  prplnqu  7557  recexprlemelu  7560  recexprlemm  7561  recexprlemloc  7568  recexprlem1ssl  7570  recexprlemss1u  7573  cauappcvgprlemm  7582  cauappcvgprlemopu  7585  cauappcvgprlemupu  7586  cauappcvgprlemdisj  7588  cauappcvgprlemloc  7589  cauappcvgprlemladdfu  7591  cauappcvgprlemladdru  7593  cauappcvgprlemladdrl  7594  cauappcvgprlem2  7597  caucvgprlemnkj  7603  caucvgprlemnbj  7604  caucvgprlemm  7605  caucvgprlemopu  7608  caucvgprlemupu  7609  caucvgprlemdisj  7611  caucvgprlemloc  7612  caucvgprlemcl  7613  caucvgprlemladdfu  7614  caucvgprlemladdrl  7615  caucvgprlem2  7617  caucvgprprlemelu  7623  caucvgprprlemcbv  7624  caucvgprprlemval  7625  caucvgprprlemnbj  7630  caucvgprprlemmu  7632  caucvgprprlemexbt  7643  caucvgprprlemaddq  7645  caucvgprprlem1  7646  caucvgprprlem2  7647  suplocexprlemmu  7655  suplocexprlemru  7656  suplocexprlemdisj  7657  suplocexprlemloc  7658  suplocexprlemub  7660  suplocexpr  7662  lttrsr  7699  ltsosr  7701  ltasrg  7707  recexgt0sr  7710  mulgt0sr  7715  aptisr  7716  mulextsr1  7718  srpospr  7720  caucvgsrlemgt1  7732  caucvgsrlemoffres  7737  caucvgsr  7739  map2psrprg  7742  suplocsrlemb  7743  suplocsrlempr  7744  suplocsrlem  7745  axprecex  7817  axpre-ltwlin  7820  axpre-lttrn  7821  axpre-apti  7822  axpre-ltadd  7823  axpre-mulgt0  7824  axpre-mulext  7825  axcaucvglemcau  7835  axcaucvglemres  7836  axcaucvg  7837  axpre-suploclemres  7838  axpre-suploc  7839  ltxrlt  7960  lttri3  7974  ltne  7979  eqle  7986  ltordlem  8376  reapti  8473  apreim  8497  squeeze0  8795  lbreu  8836  lble  8838  suprleubex  8845  sup3exmid  8848  nnge1  8876  nn2ge  8886  nn1gt1  8887  nnsub  8892  nominpos  9090  nn0ge0  9135  elnnnn0b  9154  nn0ge2m1nn  9170  zdclt  9264  suprzclex  9285  peano2uz2  9294  peano5uzti  9295  dfuzi  9297  uzind  9298  uzind3  9300  eluz1  9466  uzind4  9522  indstr  9527  supinfneg  9529  infsupneg  9530  infregelbex  9532  indstr2  9543  ublbneg  9547  elpq  9582  elpqb  9583  elrp  9587  mnfltxr  9718  nn0pnfge0  9723  xrltnsym  9725  xrlttr  9727  xrltso  9728  xrlttri3  9729  xrltne  9745  ngtmnft  9749  nmnfgt  9750  xrrebnd  9751  z2ge  9758  xltnegi  9767  xltadd1  9808  xsubge0  9813  xleaddadd  9819  ixxval  9828  elixx1  9829  elioo2  9853  iccid  9857  iccsupr  9898  repos  9902  fzval  9942  elfz1  9945  fzm1  10031  exbtwnzlemstep  10179  exbtwnzlemex  10181  qbtwnre  10188  qbtwnxr  10189  flval  10203  apbtwnz  10205  modqid2  10282  modqmuladdnn0  10299  exp3val  10453  expge0  10487  expge1  10488  nn0ltexp2  10619  facdiv  10647  facwordi  10649  hashinfom  10687  hashennn  10689  hashunlem  10713  zfz1iso  10750  ovshftex  10757  shftfibg  10758  shftfib  10761  shftfn  10762  2shfti  10769  sqrt0rlem  10941  resqrexlemex  10963  rsqrmo  10965  resqrtcl  10967  rersqrtthlem  10968  sqrtsq  10982  cau3lem  11052  caubnd2  11055  maxleim  11143  maxabslemval  11146  maxleast  11151  maxleb  11154  fimaxre2  11164  minmax  11167  xrmaxleim  11181  xrmaxiflemval  11187  xrmaxaddlem  11197  xrminmax  11202  xrbdtri  11213  climi  11224  climeu  11233  climmo  11235  2clim  11238  addcn2  11247  mulcn2  11249  reccn2ap  11250  cn1lem  11251  summodc  11320  zsumdc  11321  fsum3  11324  cvgratz  11469  ntrivcvgap0  11486  prodmodc  11515  zproddc  11516  fprodseq  11520  fprodntrivap  11521  dvdsabsb  11746  0dvds  11747  alzdvds  11788  dvdsext  11789  fzo0dvdseq  11791  2tp1odd  11817  2teven  11820  divalglemnn  11851  divalglemeunn  11854  divalglemeuneg  11856  zsupcllemstep  11874  suprzubdc  11881  zsupssdc  11883  gcdval  11888  gcddvds  11892  bezoutlemstep  11926  bezoutlemmain  11927  bezoutlemex  11930  bezoutlemeu  11936  bezoutlemsup  11938  dfgcd3  11939  bezout  11940  dvdsgcd  11941  dfgcd2  11943  dvdssq  11960  uzwodc  11966  nnwofdc  11967  lcmval  11991  lcmcllem  11995  dvdslcm  11997  lcmledvds  11998  lcmgcdlem  12005  lcmdvds  12007  coprmgcdb  12016  coprmdvds2  12021  cncongr1  12031  cncongr2  12032  isprm  12037  dvdsnprmd  12053  dvdsprm  12065  exprmfct  12066  isprm6  12075  prmexpb  12079  prmfac1  12080  rpexp  12081  sqrt2irr  12090  oddpwdclemdc  12101  oddpwdc  12102  sqpweven  12103  2sqpwodd  12104  sqne2sq  12105  nnoddn2prmb  12190  pceu  12223  pczpre  12225  pcdiv  12230  pcdvdsb  12247  difsqpwdvds  12265  pcmpt  12269  pcmptdvds  12271  oddprmdvds  12280  prmpwdvds  12281  infpnlem2  12286  oddennn  12321  evenennn  12322  exmidunben  12355  nninfdclemcl  12377  nninfdclemp1  12379  nninfdc  12382  infpn2  12385  comet  13099  metcnpi  13115  metcnpi2  13116  metcnpi3  13117  addcncntoplem  13151  cncfi  13165  elcncf1di  13166  mulcncflem  13190  dedekindeulemuub  13195  dedekindeulemloc  13197  dedekindeulemlu  13199  dedekindeulemeu  13200  dedekindeu  13201  suplociccreex  13202  suplociccex  13203  dedekindicclemuub  13204  dedekindicclemloc  13206  dedekindicclemlu  13208  dedekindicclemeu  13209  dedekindicclemicc  13210  dedekindicc  13211  ivthinclemlopn  13214  ivthinclemlr  13215  ivthinclemuopn  13216  ivthinclemur  13217  ivthinclemloc  13219  ivthinc  13221  limcimo  13234  cnplimclemr  13238  limccnp2lem  13245  limccoap  13247  eldvap  13251  logltb  13395  lgsdir  13536  lgsne0  13539  2sqlem6  13556  2sqlem8  13559  2sqlem10  13561  sbthom  13865  trilpo  13882  trirec0  13883  apdiff  13887  reap0  13897  nconstwlpolem  13903  neapmkv  13906