Theorem breq2 4033

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 3805	. . 3 |- ( A = B -> <. C , A >. = <. C , B >. )
2	1	eleq1d 2262	. 2 |- ( A = B -> ( <. C , A >. e. R <-> <. C , B >. e. R ) )
3		df-br 4030	. 2 |- ( C R A <-> <. C , A >. e. R )
4		df-br 4030	. 2 |- ( C R B <-> <. C , B >. e. R )
5	2, 3, 4	3bitr4g 223	1 |- ( A = B -> ( C R A <-> C R B ) )

Syntax hints:   -> wi 4   <-> wb 105   = wceq 1364   e. wcel 2164   <.cop 3621   class class class wbr 4029

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-v 2762  df-un 3157  df-sn 3624  df-pr 3625  df-op 3627  df-br 4030

This theorem is referenced by:  breq12  4034  breq2i  4037  breq2d  4041  nbrne1  4048  brralrspcev  4087  brimralrspcev  4088  pocl  4334  swopolem  4336  swopo  4337  sowlin  4351  sotricim  4354  sotritrieq  4356  seex  4366  frind  4383  wetriext  4609  vtoclr  4707  posng  4731  brcog  4829  brcogw  4831  opelcnvg  4842  dfdmf  4855  breldmg  4868  dfrnf  4903  dmcoss  4931  resieq  4952  dfres2  4994  elimag  5009  elrelimasn  5031  elimasn  5032  intirr  5052  poirr2  5058  poltletr  5066  dffun6f  5267  dffun4f  5270  fun11  5321  brprcneu  5547  fv3  5577  tz6.12c  5584  relelfvdm  5586  funbrfv  5595  fnbrfvb  5597  funfvdm2f  5622  fndmdif  5663  dff3im  5703  fmptco  5724  foeqcnvco  5833  isorel  5851  isocnv  5854  isotr  5859  isopolem  5865  isosolem  5867  f1oiso  5869  f1oiso2  5870  caovordig  6084  caovordg  6086  caovord  6090  caofrss  6157  caoftrn  6158  poxp  6285  tposoprab  6333  ertr  6602  ecopovsym  6685  ecopovtrn  6686  ecopovsymg  6688  ecopovtrng  6689  th3qlem2  6692  domeng  6806  eqeng  6820  snfig  6868  nneneq  6913  nnfi  6928  ssfilem  6931  domfiexmid  6934  dif1enen  6936  diffitest  6943  findcard  6944  findcard2  6945  findcard2s  6946  diffisn  6949  tridc  6955  fimax2gtrilemstep  6956  inffiexmid  6962  unsnfi  6975  fiintim  6985  fisseneq  6988  isbth  7026  supmoti  7052  eqsupti  7055  supubti  7058  suplubti  7059  suplub2ti  7060  supmaxti  7063  supsnti  7064  isotilem  7065  isoti  7066  supisolem  7067  supisoex  7068  cardcl  7241  isnumi  7242  cardval3ex  7245  exmidfodomrlemr  7262  exmidfodomrlemrALT  7263  exmidapne  7320  nqtri3or  7456  ltsonq  7458  ltanqg  7460  ltmnqg  7461  ltexnqq  7468  nsmallnqq  7472  subhalfnqq  7474  ltbtwnnqq  7475  prarloclemarch2  7479  nqnq0pi  7498  prcdnql  7544  prcunqu  7545  prnminu  7549  genpcdl  7579  genprndl  7581  genprndu  7582  genpdisj  7583  nqprm  7602  nqprrnd  7603  nqprdisj  7604  nqprloc  7605  nqprlu  7607  nqprl  7611  addnqprlemru  7618  addnqprlemfl  7619  addnqprlemfu  7620  mulnqprlemru  7634  mulnqprlemfl  7635  mulnqprlemfu  7636  1idpru  7651  ltnqpr  7653  ltnqpri  7654  prplnqu  7680  recexprlemelu  7683  recexprlemm  7684  recexprlemloc  7691  recexprlem1ssl  7693  recexprlemss1u  7696  cauappcvgprlemm  7705  cauappcvgprlemopu  7708  cauappcvgprlemupu  7709  cauappcvgprlemdisj  7711  cauappcvgprlemloc  7712  cauappcvgprlemladdfu  7714  cauappcvgprlemladdru  7716  cauappcvgprlemladdrl  7717  cauappcvgprlem2  7720  caucvgprlemnkj  7726  caucvgprlemnbj  7727  caucvgprlemm  7728  caucvgprlemopu  7731  caucvgprlemupu  7732  caucvgprlemdisj  7734  caucvgprlemloc  7735  caucvgprlemcl  7736  caucvgprlemladdfu  7737  caucvgprlemladdrl  7738  caucvgprlem2  7740  caucvgprprlemelu  7746  caucvgprprlemcbv  7747  caucvgprprlemval  7748  caucvgprprlemnbj  7753  caucvgprprlemmu  7755  caucvgprprlemexbt  7766  caucvgprprlemaddq  7768  caucvgprprlem1  7769  caucvgprprlem2  7770  suplocexprlemmu  7778  suplocexprlemru  7779  suplocexprlemdisj  7780  suplocexprlemloc  7781  suplocexprlemub  7783  suplocexpr  7785  lttrsr  7822  ltsosr  7824  ltasrg  7830  recexgt0sr  7833  mulgt0sr  7838  aptisr  7839  mulextsr1  7841  srpospr  7843  caucvgsrlemgt1  7855  caucvgsrlemoffres  7860  caucvgsr  7862  map2psrprg  7865  suplocsrlemb  7866  suplocsrlempr  7867  suplocsrlem  7868  axprecex  7940  axpre-ltwlin  7943  axpre-lttrn  7944  axpre-apti  7945  axpre-ltadd  7946  axpre-mulgt0  7947  axpre-mulext  7948  axcaucvglemcau  7958  axcaucvglemres  7959  axcaucvg  7960  axpre-suploclemres  7961  axpre-suploc  7962  ltxrlt  8085  lttri3  8099  ltne  8104  eqle  8111  ltordlem  8501  reapti  8598  apreim  8622  squeeze0  8923  lbreu  8964  lble  8966  suprleubex  8973  sup3exmid  8976  nnge1  9005  nn2ge  9015  nn1gt1  9016  nnsub  9021  nominpos  9220  nn0ge0  9265  elnnnn0b  9284  nn0ge2m1nn  9300  zdclt  9394  suprzclex  9415  peano2uz2  9424  peano5uzti  9425  dfuzi  9427  uzind  9428  uzind3  9430  eluz1  9596  uzind4  9653  indstr  9658  supinfneg  9660  infsupneg  9661  infregelbex  9663  indstr2  9674  ublbneg  9678  irrmulap  9713  elpq  9714  elpqb  9715  elrp  9721  mnfltxr  9852  nn0pnfge0  9857  xrltnsym  9859  xrlttr  9861  xrltso  9862  xrlttri3  9863  xrltne  9879  ngtmnft  9883  nmnfgt  9884  xrrebnd  9885  z2ge  9892  xltnegi  9901  xltadd1  9942  xsubge0  9947  xleaddadd  9953  ixxval  9962  elixx1  9963  elioo2  9987  iccid  9991  iccsupr  10032  repos  10036  fzval  10076  elfz1  10079  fzm1  10166  qdclt  10315  exbtwnzlemstep  10316  exbtwnzlemex  10318  qbtwnre  10325  qbtwnxr  10326  flval  10341  apbtwnz  10343  modqid2  10422  modqmuladdnn0  10439  exp3val  10612  expge0  10646  expge1  10647  nn0ltexp2  10780  facdiv  10809  facwordi  10811  hashinfom  10849  hashennn  10851  hashunlem  10875  zfz1iso  10912  wrdlen1  10951  fstwrdne0  10953  ovshftex  10963  shftfibg  10964  shftfib  10967  shftfn  10968  2shfti  10975  sqrt0rlem  11147  resqrexlemex  11169  rsqrmo  11171  resqrtcl  11173  rersqrtthlem  11174  sqrtsq  11188  cau3lem  11258  caubnd2  11261  maxleim  11349  maxabslemval  11352  maxleast  11357  maxleb  11360  fimaxre2  11370  minmax  11373  xrmaxleim  11387  xrmaxiflemval  11393  xrmaxaddlem  11403  xrminmax  11408  xrbdtri  11419  climi  11430  climeu  11439  climmo  11441  2clim  11444  addcn2  11453  mulcn2  11455  reccn2ap  11456  cn1lem  11457  summodc  11526  zsumdc  11527  fsum3  11530  cvgratz  11675  ntrivcvgap0  11692  prodmodc  11721  zproddc  11722  fprodseq  11726  fprodntrivap  11727  sinltxirr  11904  dvdsabsb  11953  0dvds  11954  alzdvds  11996  dvdsext  11997  fzo0dvdseq  11999  2tp1odd  12025  2teven  12028  divalglemnn  12059  divalglemeunn  12062  divalglemeuneg  12064  zsupcllemstep  12082  suprzubdc  12089  zsupssdc  12091  gcdval  12096  gcddvds  12100  bezoutlemstep  12134  bezoutlemmain  12135  bezoutlemex  12138  bezoutlemeu  12144  bezoutlemsup  12146  dfgcd3  12147  bezout  12148  dvdsgcd  12149  dfgcd2  12151  dvdssq  12168  uzwodc  12174  nnwofdc  12175  lcmval  12201  lcmcllem  12205  dvdslcm  12207  lcmledvds  12208  lcmgcdlem  12215  lcmdvds  12217  coprmgcdb  12226  coprmdvds2  12231  cncongr1  12241  cncongr2  12242  isprm  12247  dvdsnprmd  12263  dvdsprm  12275  exprmfct  12276  isprm6  12285  prmexpb  12289  prmfac1  12290  rpexp  12291  sqrt2irr  12300  oddpwdclemdc  12311  oddpwdc  12312  sqpweven  12313  2sqpwodd  12314  sqne2sq  12315  nnoddn2prmb  12400  pceu  12433  pczpre  12435  pcdiv  12440  pcdvdsb  12458  difsqpwdvds  12476  pcmpt  12481  pcmptdvds  12483  oddprmdvds  12492  prmpwdvds  12493  infpnlem2  12498  oddennn  12549  evenennn  12550  exmidunben  12583  nninfdclemcl  12605  nninfdclemp1  12607  nninfdc  12610  infpn2  12613  eqgen  13297  zndvds  14137  znleval  14141  comet  14667  metcnpi  14683  metcnpi2  14684  metcnpi3  14685  addcncntoplem  14719  cncfi  14733  elcncf1di  14734  mulcncflem  14761  dedekindeulemuub  14771  dedekindeulemloc  14773  dedekindeulemlu  14775  dedekindeulemeu  14776  dedekindeu  14777  suplociccreex  14778  suplociccex  14779  dedekindicclemuub  14780  dedekindicclemloc  14782  dedekindicclemlu  14784  dedekindicclemeu  14785  dedekindicclemicc  14786  dedekindicc  14787  ivthinclemlopn  14790  ivthinclemlr  14791  ivthinclemuopn  14792  ivthinclemur  14793  ivthinclemloc  14795  ivthinc  14797  ivthreinc  14799  dich0  14806  ivthdich  14807  limcimo  14819  cnplimclemr  14823  limccnp2lem  14830  limccoap  14832  eldvap  14836  logltb  15009  lgsdir  15151  lgsne0  15154  gausslemma2dlem0i  15173  lgsquadlem1  15191  2sqlem6  15207  2sqlem8  15210  2sqlem10  15212  sbthom  15516  trilpo  15533  trirec0  15534  apdiff  15538  reap0  15548  cndcap  15549  nconstwlpolem  15555  neapmkv  15558  neap0mkv  15559  ltlenmkv  15560