Theorem breq2 4118

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 3889	. . 3 |- ( A = B -> <. C , A >. = <. C , B >. )
2	1	eleq1d 2303	. 2 |- ( A = B -> ( <. C , A >. e. R <-> <. C , B >. e. R ) )
3		df-br 4115	. 2 |- ( C R A <-> <. C , A >. e. R )
4		df-br 4115	. 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 1398   e. wcel 2205   <.cop 3697   class class class wbr 4114

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-v 2817  df-un 3218  df-sn 3700  df-pr 3701  df-op 3703  df-br 4115

This theorem is referenced by:  breq12  4119  breq2i  4122  breq2d  4126  nbrne1  4133  brralrspcev  4173  brimralrspcev  4174  pocl  4429  swopolem  4431  swopo  4432  sowlin  4446  sotricim  4449  sotritrieq  4451  seex  4461  frind  4478  wetriext  4704  vtoclr  4803  posng  4827  brcog  4927  brcogw  4929  opelcnvg  4940  dfdmf  4954  breldmg  4967  dfrnf  5003  dmcoss  5032  resieq  5053  dfres2  5095  elimag  5110  elrelimasn  5133  elimasn  5134  intirr  5154  poirr2  5160  poltletr  5168  dffun6f  5370  dffun4f  5373  fun11  5428  brprcneu  5668  fv3  5698  tz6.12c  5705  relelfvdm  5707  fvmbr  5710  funbrfv  5718  fnbrfvb  5720  funfvdm2f  5747  fndmdif  5788  dff3im  5827  fmptco  5848  foeqcnvco  5969  isorel  5987  isocnv  5990  isotr  5995  isopolem  6001  isosolem  6003  f1oiso  6005  f1oiso2  6006  caovordig  6228  caovordg  6230  caovord  6234  caofrss  6307  caoftrn  6308  poxp  6441  tposoprab  6524  ertr  6795  ecopovsym  6878  ecopovtrn  6879  ecopovsymg  6881  ecopovtrng  6882  th3qlem2  6885  domeng  7002  eqeng  7018  snfig  7069  nneneq  7124  nnfi  7140  ssfilem  7143  ssfilemd  7145  domfiexmid  7148  dif1enen  7150  diffitest  7157  findcard  7158  findcard2  7159  findcard2s  7160  diffisn  7163  tridc  7170  fimax2gtrilemstep  7171  inffiexmid  7179  unsnfi  7192  fiintim  7204  fisseneq  7208  isbth  7250  supmoti  7297  eqsupti  7300  supubti  7303  suplubti  7304  suplub2ti  7305  supmaxti  7308  supsnti  7309  isotilem  7310  isoti  7311  supisolem  7312  supisoex  7313  cardcl  7490  isnumi  7491  cardval3ex  7494  exmidfodomrlemr  7518  exmidfodomrlemrALT  7519  papsym  7576  papcotr  7577  exmidapne  7590  nqtri3or  7727  ltsonq  7729  ltanqg  7731  ltmnqg  7732  ltexnqq  7739  nsmallnqq  7743  subhalfnqq  7745  ltbtwnnqq  7746  prarloclemarch2  7750  nqnq0pi  7769  prcdnql  7815  prcunqu  7816  prnminu  7820  genpcdl  7850  genprndl  7852  genprndu  7853  genpdisj  7854  nqprm  7873  nqprrnd  7874  nqprdisj  7875  nqprloc  7876  nqprlu  7878  nqprl  7882  addnqprlemru  7889  addnqprlemfl  7890  addnqprlemfu  7891  mulnqprlemru  7905  mulnqprlemfl  7906  mulnqprlemfu  7907  1idpru  7922  ltnqpr  7924  ltnqpri  7925  prplnqu  7951  recexprlemelu  7954  recexprlemm  7955  recexprlemloc  7962  recexprlem1ssl  7964  recexprlemss1u  7967  cauappcvgprlemm  7976  cauappcvgprlemopu  7979  cauappcvgprlemupu  7980  cauappcvgprlemdisj  7982  cauappcvgprlemloc  7983  cauappcvgprlemladdfu  7985  cauappcvgprlemladdru  7987  cauappcvgprlemladdrl  7988  cauappcvgprlem2  7991  caucvgprlemnkj  7997  caucvgprlemnbj  7998  caucvgprlemm  7999  caucvgprlemopu  8002  caucvgprlemupu  8003  caucvgprlemdisj  8005  caucvgprlemloc  8006  caucvgprlemcl  8007  caucvgprlemladdfu  8008  caucvgprlemladdrl  8009  caucvgprlem2  8011  caucvgprprlemelu  8017  caucvgprprlemcbv  8018  caucvgprprlemval  8019  caucvgprprlemnbj  8024  caucvgprprlemmu  8026  caucvgprprlemexbt  8037  caucvgprprlemaddq  8039  caucvgprprlem1  8040  caucvgprprlem2  8041  suplocexprlemmu  8049  suplocexprlemru  8050  suplocexprlemdisj  8051  suplocexprlemloc  8052  suplocexprlemub  8054  suplocexpr  8056  lttrsr  8093  ltsosr  8095  ltasrg  8101  recexgt0sr  8104  mulgt0sr  8109  aptisr  8110  mulextsr1  8112  srpospr  8114  caucvgsrlemgt1  8126  caucvgsrlemoffres  8131  caucvgsr  8133  map2psrprg  8136  suplocsrlemb  8137  suplocsrlempr  8138  suplocsrlem  8139  axprecex  8211  axpre-ltwlin  8214  axpre-lttrn  8215  axpre-apti  8216  axpre-ltadd  8217  axpre-mulgt0  8218  axpre-mulext  8219  axcaucvglemcau  8229  axcaucvglemres  8230  axcaucvg  8231  axpre-suploclemres  8232  axpre-suploc  8233  ltxrlt  8355  lttri3  8369  ltne  8374  eqle  8381  ltordlem  8773  reapti  8870  apreim  8894  squeeze0  9195  lbreu  9236  lble  9238  suprleubex  9245  sup3exmid  9248  nnge1  9277  nn2ge  9287  nn1gt1  9288  nnsub  9293  nominpos  9493  nn0ge0  9538  elnnnn0b  9557  nn0ge2m1nn  9577  zdclt  9672  suprzclex  9694  peano2uz2  9703  peano5uzti  9704  dfuzi  9706  uzind  9707  uzind3  9709  eluz1  9875  uzind4  9938  indstr  9943  supinfneg  9945  infsupneg  9946  infregelbex  9948  indstr2  9959  ublbneg  9963  irrmulap  9998  elpq  9999  elpqb  10000  elrp  10006  mnfltxr  10138  nn0pnfge0  10143  xrltnsym  10145  xrlttr  10147  xrltso  10148  xrlttri3  10149  xrltne  10165  ngtmnft  10169  nmnfgt  10170  xrrebnd  10171  z2ge  10178  xltnegi  10187  xltadd1  10228  xsubge0  10233  xleaddadd  10239  ixxval  10248  elixx1  10249  elioo2  10273  iccid  10277  iccsupr  10318  repos  10322  fzval  10363  elfz1  10366  fzm1  10456  zsupcllemstep  10611  suprzubdc  10620  zsupssdc  10622  qdclt  10629  exbtwnzlemstep  10631  exbtwnzlemex  10633  qbtwnre  10640  qbtwnxr  10641  flval  10656  apbtwnz  10658  modqid2  10737  modqmuladdnn0  10754  exp3val  10927  expge0  10961  expge1  10962  nn0ltexp2  11096  facdiv  11125  facwordi  11127  hashinfom  11166  hashennn  11168  hashunlem  11193  zfz1iso  11238  wrdlen1  11287  fstwrdne0  11289  wrdl1exs1  11342  pfxsuffeqwrdeq  11415  pfxsuff1eqwrdeq  11416  ccats1pfxeq  11431  ccats1pfxeqrex  11432  pfxccatin12lem3  11449  ovshftex  11529  shftfibg  11530  shftfib  11533  shftfn  11534  2shfti  11541  sqrt0rlem  11713  resqrexlemex  11735  rsqrmo  11737  resqrtcl  11739  rersqrtthlem  11740  sqrtsq  11754  cau3lem  11824  caubnd2  11827  maxleim  11915  maxabslemval  11918  maxleast  11923  maxleb  11926  fimaxre2  11937  minmax  11940  xrmaxleim  11954  xrmaxiflemval  11960  xrmaxaddlem  11970  xrminmax  11975  xrbdtri  11986  climi  11997  climeu  12006  climmo  12008  2clim  12011  addcn2  12020  mulcn2  12022  reccn2ap  12023  cn1lem  12024  summodc  12094  zsumdc  12095  fsum3  12098  cvgratz  12243  ntrivcvgap0  12260  prodmodc  12289  zproddc  12290  fprodseq  12294  fprodntrivap  12295  sinltxirr  12472  dvdsabsb  12521  0dvds  12522  alzdvds  12565  dvdsext  12566  fzo0dvdseq  12568  2tp1odd  12595  2teven  12598  divalglemnn  12629  divalglemeunn  12632  divalglemeuneg  12634  bitsinv1lem  12672  gcdval  12680  gcddvds  12684  bezoutlemstep  12718  bezoutlemmain  12719  bezoutlemex  12722  bezoutlemeu  12728  bezoutlemsup  12730  dfgcd3  12731  bezout  12732  dvdsgcd  12733  dfgcd2  12735  dvdssq  12752  uzwodc  12758  nnwofdc  12759  lcmval  12785  lcmcllem  12789  dvdslcm  12791  lcmledvds  12792  lcmgcdlem  12799  lcmdvds  12801  coprmgcdb  12810  coprmdvds2  12815  cncongr1  12825  cncongr2  12826  isprm  12831  dvdsnprmd  12847  dvdsprm  12859  exprmfct  12860  isprm6  12869  prmexpb  12873  prmfac1  12874  rpexp  12875  sqrt2irr  12884  oddpwdclemdc  12895  oddpwdc  12896  sqpweven  12897  2sqpwodd  12898  sqne2sq  12899  nnoddn2prmb  12985  pceu  13018  pczpre  13020  pcdiv  13025  pcdvdsb  13043  difsqpwdvds  13061  pcmpt  13066  pcmptdvds  13068  oddprmdvds  13077  prmpwdvds  13078  infpnlem2  13083  ballotfilemfcc  13177  oddennn  13227  evenennn  13228  exmidunben  13261  nninfdclemcl  13283  nninfdclemp1  13285  nninfdc  13288  infpn2  13291  eqgen  13980  zndvds  14923  znleval  14927  comet  15490  metcnpi  15506  metcnpi2  15507  metcnpi3  15508  addcncntoplem  15552  cncfi  15569  elcncf1di  15570  mulcncflem  15598  dedekindeulemuub  15608  dedekindeulemloc  15610  dedekindeulemlu  15612  dedekindeulemeu  15613  dedekindeu  15614  suplociccreex  15615  suplociccex  15616  dedekindicclemuub  15617  dedekindicclemloc  15619  dedekindicclemlu  15621  dedekindicclemeu  15622  dedekindicclemicc  15623  dedekindicc  15624  ivthinclemlopn  15627  ivthinclemlr  15628  ivthinclemuopn  15629  ivthinclemur  15630  ivthinclemloc  15632  ivthinc  15634  ivthreinc  15636  dich0  15643  ivthdich  15644  limcimo  15656  cnplimclemr  15660  limccnp2lem  15667  limccoap  15669  eldvap  15673  logltb  15865  pellexlem3  15973  lgsdir  16034  lgsne0  16037  gausslemma2dlem0i  16056  lgsquadlem1  16076  lgsquadlem2  16077  lgsquadlem3  16078  2lgslem2  16091  2lgs  16103  2sqlem6  16119  2sqlem8  16122  2sqlem10  16124  lfgredg2dom  16253  istrl  16506  clwwlkn0  16529  clwwlkext2edg  16543  clwwlknonccat  16554  clwwlknonex2  16560  iseupth  16568  konigsberg  16614  sbthom  16932  trilpo  16953  trirec0  16954  apdiff  16958  reap0  16969  cndcap  16970  trimul0or  16971  nconstwlpolem  16977  neapmkv  16980  neap0mkv  16981  ltlenmkv  16982