Theorem breq2 3991

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 3764	. . 3 |- ( A = B -> <. C , A >. = <. C , B >. )
2	1	eleq1d 2239	. 2 |- ( A = B -> ( <. C , A >. e. R <-> <. C , B >. e. R ) )
3		df-br 3988	. 2 |- ( C R A <-> <. C , A >. e. R )
4		df-br 3988	. 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 1348   e. wcel 2141   <.cop 3584   class class class wbr 3987

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 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-3an 975  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-v 2732  df-un 3125  df-sn 3587  df-pr 3588  df-op 3590  df-br 3988

This theorem is referenced by:  breq12  3992  breq2i  3995  breq2d  3999  nbrne1  4006  brralrspcev  4045  brimralrspcev  4046  pocl  4286  swopolem  4288  swopo  4289  sowlin  4303  sotricim  4306  sotritrieq  4308  seex  4318  frind  4335  wetriext  4559  vtoclr  4657  posng  4681  brcog  4776  brcogw  4778  opelcnvg  4789  dfdmf  4802  breldmg  4815  dfrnf  4850  dmcoss  4878  resieq  4899  dfres2  4941  elimag  4955  elreimasng  4975  elimasn  4976  intirr  4995  poirr2  5001  poltletr  5009  dffun6f  5209  dffun4f  5212  fun11  5263  brprcneu  5487  fv3  5517  tz6.12c  5524  relelfvdm  5526  funbrfv  5533  fnbrfvb  5535  funfvdm2f  5559  fndmdif  5598  dff3im  5638  fmptco  5659  foeqcnvco  5766  isorel  5784  isocnv  5787  isotr  5792  isopolem  5798  isosolem  5800  f1oiso  5802  f1oiso2  5803  caovordig  6015  caovordg  6017  caovord  6021  caofrss  6082  caoftrn  6083  poxp  6208  tposoprab  6256  ertr  6524  ecopovsym  6605  ecopovtrn  6606  ecopovsymg  6608  ecopovtrng  6609  th3qlem2  6612  domeng  6726  eqeng  6740  snfig  6788  nneneq  6831  nnfi  6846  ssfilem  6849  domfiexmid  6852  dif1enen  6854  diffitest  6861  findcard  6862  findcard2  6863  findcard2s  6864  diffisn  6867  tridc  6873  fimax2gtrilemstep  6874  inffiexmid  6880  unsnfi  6892  fiintim  6902  fisseneq  6905  isbth  6940  supmoti  6966  eqsupti  6969  supubti  6972  suplubti  6973  suplub2ti  6974  supmaxti  6977  supsnti  6978  isotilem  6979  isoti  6980  supisolem  6981  supisoex  6982  cardcl  7145  isnumi  7146  cardval3ex  7149  exmidfodomrlemr  7166  exmidfodomrlemrALT  7167  nqtri3or  7345  ltsonq  7347  ltanqg  7349  ltmnqg  7350  ltexnqq  7357  nsmallnqq  7361  subhalfnqq  7363  ltbtwnnqq  7364  prarloclemarch2  7368  nqnq0pi  7387  prcdnql  7433  prcunqu  7434  prnminu  7438  genpcdl  7468  genprndl  7470  genprndu  7471  genpdisj  7472  nqprm  7491  nqprrnd  7492  nqprdisj  7493  nqprloc  7494  nqprlu  7496  nqprl  7500  addnqprlemru  7507  addnqprlemfl  7508  addnqprlemfu  7509  mulnqprlemru  7523  mulnqprlemfl  7524  mulnqprlemfu  7525  1idpru  7540  ltnqpr  7542  ltnqpri  7543  prplnqu  7569  recexprlemelu  7572  recexprlemm  7573  recexprlemloc  7580  recexprlem1ssl  7582  recexprlemss1u  7585  cauappcvgprlemm  7594  cauappcvgprlemopu  7597  cauappcvgprlemupu  7598  cauappcvgprlemdisj  7600  cauappcvgprlemloc  7601  cauappcvgprlemladdfu  7603  cauappcvgprlemladdru  7605  cauappcvgprlemladdrl  7606  cauappcvgprlem2  7609  caucvgprlemnkj  7615  caucvgprlemnbj  7616  caucvgprlemm  7617  caucvgprlemopu  7620  caucvgprlemupu  7621  caucvgprlemdisj  7623  caucvgprlemloc  7624  caucvgprlemcl  7625  caucvgprlemladdfu  7626  caucvgprlemladdrl  7627  caucvgprlem2  7629  caucvgprprlemelu  7635  caucvgprprlemcbv  7636  caucvgprprlemval  7637  caucvgprprlemnbj  7642  caucvgprprlemmu  7644  caucvgprprlemexbt  7655  caucvgprprlemaddq  7657  caucvgprprlem1  7658  caucvgprprlem2  7659  suplocexprlemmu  7667  suplocexprlemru  7668  suplocexprlemdisj  7669  suplocexprlemloc  7670  suplocexprlemub  7672  suplocexpr  7674  lttrsr  7711  ltsosr  7713  ltasrg  7719  recexgt0sr  7722  mulgt0sr  7727  aptisr  7728  mulextsr1  7730  srpospr  7732  caucvgsrlemgt1  7744  caucvgsrlemoffres  7749  caucvgsr  7751  map2psrprg  7754  suplocsrlemb  7755  suplocsrlempr  7756  suplocsrlem  7757  axprecex  7829  axpre-ltwlin  7832  axpre-lttrn  7833  axpre-apti  7834  axpre-ltadd  7835  axpre-mulgt0  7836  axpre-mulext  7837  axcaucvglemcau  7847  axcaucvglemres  7848  axcaucvg  7849  axpre-suploclemres  7850  axpre-suploc  7851  ltxrlt  7972  lttri3  7986  ltne  7991  eqle  7998  ltordlem  8388  reapti  8485  apreim  8509  squeeze0  8807  lbreu  8848  lble  8850  suprleubex  8857  sup3exmid  8860  nnge1  8888  nn2ge  8898  nn1gt1  8899  nnsub  8904  nominpos  9102  nn0ge0  9147  elnnnn0b  9166  nn0ge2m1nn  9182  zdclt  9276  suprzclex  9297  peano2uz2  9306  peano5uzti  9307  dfuzi  9309  uzind  9310  uzind3  9312  eluz1  9478  uzind4  9534  indstr  9539  supinfneg  9541  infsupneg  9542  infregelbex  9544  indstr2  9555  ublbneg  9559  elpq  9594  elpqb  9595  elrp  9599  mnfltxr  9730  nn0pnfge0  9735  xrltnsym  9737  xrlttr  9739  xrltso  9740  xrlttri3  9741  xrltne  9757  ngtmnft  9761  nmnfgt  9762  xrrebnd  9763  z2ge  9770  xltnegi  9779  xltadd1  9820  xsubge0  9825  xleaddadd  9831  ixxval  9840  elixx1  9841  elioo2  9865  iccid  9869  iccsupr  9910  repos  9914  fzval  9954  elfz1  9957  fzm1  10043  exbtwnzlemstep  10191  exbtwnzlemex  10193  qbtwnre  10200  qbtwnxr  10201  flval  10215  apbtwnz  10217  modqid2  10294  modqmuladdnn0  10311  exp3val  10465  expge0  10499  expge1  10500  nn0ltexp2  10631  facdiv  10659  facwordi  10661  hashinfom  10699  hashennn  10701  hashunlem  10726  zfz1iso  10763  ovshftex  10770  shftfibg  10771  shftfib  10774  shftfn  10775  2shfti  10782  sqrt0rlem  10954  resqrexlemex  10976  rsqrmo  10978  resqrtcl  10980  rersqrtthlem  10981  sqrtsq  10995  cau3lem  11065  caubnd2  11068  maxleim  11156  maxabslemval  11159  maxleast  11164  maxleb  11167  fimaxre2  11177  minmax  11180  xrmaxleim  11194  xrmaxiflemval  11200  xrmaxaddlem  11210  xrminmax  11215  xrbdtri  11226  climi  11237  climeu  11246  climmo  11248  2clim  11251  addcn2  11260  mulcn2  11262  reccn2ap  11263  cn1lem  11264  summodc  11333  zsumdc  11334  fsum3  11337  cvgratz  11482  ntrivcvgap0  11499  prodmodc  11528  zproddc  11529  fprodseq  11533  fprodntrivap  11534  dvdsabsb  11759  0dvds  11760  alzdvds  11801  dvdsext  11802  fzo0dvdseq  11804  2tp1odd  11830  2teven  11833  divalglemnn  11864  divalglemeunn  11867  divalglemeuneg  11869  zsupcllemstep  11887  suprzubdc  11894  zsupssdc  11896  gcdval  11901  gcddvds  11905  bezoutlemstep  11939  bezoutlemmain  11940  bezoutlemex  11943  bezoutlemeu  11949  bezoutlemsup  11951  dfgcd3  11952  bezout  11953  dvdsgcd  11954  dfgcd2  11956  dvdssq  11973  uzwodc  11979  nnwofdc  11980  lcmval  12004  lcmcllem  12008  dvdslcm  12010  lcmledvds  12011  lcmgcdlem  12018  lcmdvds  12020  coprmgcdb  12029  coprmdvds2  12034  cncongr1  12044  cncongr2  12045  isprm  12050  dvdsnprmd  12066  dvdsprm  12078  exprmfct  12079  isprm6  12088  prmexpb  12092  prmfac1  12093  rpexp  12094  sqrt2irr  12103  oddpwdclemdc  12114  oddpwdc  12115  sqpweven  12116  2sqpwodd  12117  sqne2sq  12118  nnoddn2prmb  12203  pceu  12236  pczpre  12238  pcdiv  12243  pcdvdsb  12260  difsqpwdvds  12278  pcmpt  12282  pcmptdvds  12284  oddprmdvds  12293  prmpwdvds  12294  infpnlem2  12299  oddennn  12334  evenennn  12335  exmidunben  12368  nninfdclemcl  12390  nninfdclemp1  12392  nninfdc  12395  infpn2  12398  comet  13252  metcnpi  13268  metcnpi2  13269  metcnpi3  13270  addcncntoplem  13304  cncfi  13318  elcncf1di  13319  mulcncflem  13343  dedekindeulemuub  13348  dedekindeulemloc  13350  dedekindeulemlu  13352  dedekindeulemeu  13353  dedekindeu  13354  suplociccreex  13355  suplociccex  13356  dedekindicclemuub  13357  dedekindicclemloc  13359  dedekindicclemlu  13361  dedekindicclemeu  13362  dedekindicclemicc  13363  dedekindicc  13364  ivthinclemlopn  13367  ivthinclemlr  13368  ivthinclemuopn  13369  ivthinclemur  13370  ivthinclemloc  13372  ivthinc  13374  limcimo  13387  cnplimclemr  13391  limccnp2lem  13398  limccoap  13400  eldvap  13404  logltb  13548  lgsdir  13689  lgsne0  13692  2sqlem6  13709  2sqlem8  13712  2sqlem10  13714  sbthom  14018  trilpo  14035  trirec0  14036  apdiff  14040  reap0  14050  nconstwlpolem  14056  neapmkv  14059