Theorem breq2 3855

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 3629	. . 3 |- ( A = B -> <. C , A >. = <. C , B >. )
2	1	eleq1d 2157	. 2 |- ( A = B -> ( <. C , A >. e. R <-> <. C , B >. e. R ) )
3		df-br 3852	. 2 |- ( C R A <-> <. C , A >. e. R )
4		df-br 3852	. 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 1290   e. wcel 1439   <.cop 3453   class class class wbr 3851

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 666  ax-5 1382  ax-7 1383  ax-gen 1384  ax-ie1 1428  ax-ie2 1429  ax-8 1441  ax-10 1442  ax-11 1443  ax-i12 1444  ax-bndl 1445  ax-4 1446  ax-17 1465  ax-i9 1469  ax-ial 1473  ax-i5r 1474  ax-ext 2071

This theorem depends on definitions:  df-bi 116  df-3an 927  df-tru 1293  df-nf 1396  df-sb 1694  df-clab 2076  df-cleq 2082  df-clel 2085  df-nfc 2218  df-v 2622  df-un 3004  df-sn 3456  df-pr 3457  df-op 3459  df-br 3852

This theorem is referenced by:  breq12  3856  breq2i  3859  breq2d  3863  nbrne1  3868  pocl  4139  swopolem  4141  swopo  4142  sowlin  4156  sotricim  4159  sotritrieq  4161  seex  4171  frind  4188  wetriext  4405  vtoclr  4499  posng  4523  brcog  4616  brcogw  4618  opelcnvg  4629  dfdmf  4642  breldmg  4655  dfrnf  4689  dmcoss  4715  resieq  4736  dfres2  4777  elimag  4791  elreimasng  4811  elimasn  4812  intirr  4831  poirr2  4837  poltletr  4845  dffun6f  5041  dffun4f  5044  fun11  5094  brprcneu  5311  fv3  5341  tz6.12c  5347  relelfvdm  5349  funbrfv  5356  fnbrfvb  5358  funfvdm2f  5382  fndmdif  5418  dff3im  5458  fmptco  5478  foeqcnvco  5583  isorel  5601  isocnv  5604  isotr  5609  isopolem  5615  isosolem  5617  f1oiso  5619  f1oiso2  5620  caovordig  5824  caovordg  5826  caovord  5830  caofrss  5893  caoftrn  5894  poxp  6011  tposoprab  6059  ertr  6321  ecopovsym  6402  ecopovtrn  6403  ecopovsymg  6405  ecopovtrng  6406  th3qlem2  6409  domeng  6523  eqeng  6537  snfig  6585  nneneq  6627  nnfi  6642  ssfilem  6645  domfiexmid  6648  dif1enen  6650  diffitest  6657  findcard  6658  findcard2  6659  findcard2s  6660  diffisn  6663  tridc  6669  fimax2gtrilemstep  6670  inffiexmid  6676  unsnfi  6683  fiintim  6693  fisseneq  6696  isbth  6730  supmoti  6742  eqsupti  6745  supubti  6748  suplubti  6749  suplub2ti  6750  supmaxti  6753  supsnti  6754  isotilem  6755  isoti  6756  supisolem  6757  supisoex  6758  cardcl  6870  isnumi  6871  cardval3ex  6874  exmidfodomrlemr  6889  exmidfodomrlemrALT  6890  nqtri3or  7016  ltsonq  7018  ltanqg  7020  ltmnqg  7021  ltexnqq  7028  nsmallnqq  7032  subhalfnqq  7034  ltbtwnnqq  7035  prarloclemarch2  7039  nqnq0pi  7058  prcdnql  7104  prcunqu  7105  prnminu  7109  genpcdl  7139  genprndl  7141  genprndu  7142  genpdisj  7143  nqprm  7162  nqprrnd  7163  nqprdisj  7164  nqprloc  7165  nqprlu  7167  nqprl  7171  addnqprlemru  7178  addnqprlemfl  7179  addnqprlemfu  7180  mulnqprlemru  7194  mulnqprlemfl  7195  mulnqprlemfu  7196  1idpru  7211  ltnqpr  7213  ltnqpri  7214  prplnqu  7240  recexprlemelu  7243  recexprlemm  7244  recexprlemloc  7251  recexprlem1ssl  7253  recexprlemss1u  7256  cauappcvgprlemm  7265  cauappcvgprlemopu  7268  cauappcvgprlemupu  7269  cauappcvgprlemdisj  7271  cauappcvgprlemloc  7272  cauappcvgprlemladdfu  7274  cauappcvgprlemladdru  7276  cauappcvgprlemladdrl  7277  cauappcvgprlem2  7280  caucvgprlemnkj  7286  caucvgprlemnbj  7287  caucvgprlemm  7288  caucvgprlemopu  7291  caucvgprlemupu  7292  caucvgprlemdisj  7294  caucvgprlemloc  7295  caucvgprlemcl  7296  caucvgprlemladdfu  7297  caucvgprlemladdrl  7298  caucvgprlem2  7300  caucvgprprlemelu  7306  caucvgprprlemcbv  7307  caucvgprprlemval  7308  caucvgprprlemnbj  7313  caucvgprprlemmu  7315  caucvgprprlemexbt  7326  caucvgprprlemaddq  7328  caucvgprprlem1  7329  caucvgprprlem2  7330  lttrsr  7369  ltsosr  7371  ltasrg  7377  recexgt0sr  7380  mulgt0sr  7384  aptisr  7385  mulextsr1  7387  srpospr  7389  caucvgsrlemgt1  7401  caucvgsrlemoffres  7406  caucvgsr  7408  axprecex  7476  axpre-ltwlin  7479  axpre-lttrn  7480  axpre-apti  7481  axpre-ltadd  7482  axpre-mulgt0  7483  axpre-mulext  7484  axcaucvglemcau  7494  axcaucvglemres  7495  axcaucvg  7496  ltxrlt  7613  lttri3  7626  ltne  7631  eqle  7637  ltordlem  8021  reapti  8117  apreim  8141  squeeze0  8426  lbreu  8467  lble  8469  suprleubex  8476  nnge1  8506  nn2ge  8516  nn1gt1  8517  nnsub  8522  nominpos  8714  nn0ge0  8759  elnnnn0b  8778  nn0ge2m1nn  8794  zdclt  8885  suprzclex  8905  peano2uz2  8914  peano5uzti  8915  dfuzi  8917  uzind  8918  uzind3  8920  eluz1  9084  uzind4  9137  indstr  9142  supinfneg  9144  infsupneg  9145  indstr2  9157  ublbneg  9159  elrp  9197  mnfltxr  9317  nn0pnfge0  9322  xrltnsym  9324  xrlttr  9326  xrltso  9327  xrlttri3  9328  xrltne  9339  ngtmnft  9341  xrrebnd  9342  z2ge  9349  xltnegi  9358  ixxval  9375  elixx1  9376  elioo2  9400  iccid  9404  iccsupr  9445  repos  9449  fzval  9487  elfz1  9490  fzm1  9575  exbtwnzlemstep  9720  exbtwnzlemex  9722  qbtwnre  9729  qbtwnxr  9730  flval  9740  apbtwnz  9742  modqid2  9819  modqmuladdnn0  9836  exp3val  10018  expge0  10052  expge1  10053  facdiv  10207  facwordi  10209  hashinfom  10247  hashennn  10249  hashunlem  10273  zfz1iso  10307  ovshftex  10314  shftfibg  10315  shftfib  10318  shftfn  10319  2shfti  10326  sqrt0rlem  10497  resqrexlemex  10519  rsqrmo  10521  resqrtcl  10523  rersqrtthlem  10524  sqrtsq  10538  cau3lem  10608  caubnd2  10611  maxleim  10699  maxabslemval  10702  maxleast  10707  maxleb  10710  fimaxre2  10719  minmax  10722  climi  10736  climeu  10745  climmo  10747  2clim  10750  addcn2  10760  mulcn2  10762  cn1lem  10763  isummo  10834  zisum  10835  fisum  10839  cvgratz  10987  dvdsabsb  11154  0dvds  11155  alzdvds  11194  dvdsext  11195  fzo0dvdseq  11197  2tp1odd  11223  2teven  11226  divalglemnn  11257  divalglemeunn  11260  divalglemeuneg  11262  zsupcllemstep  11280  gcdval  11290  gcddvds  11294  bezoutlemstep  11325  bezoutlemmain  11326  bezoutlemex  11329  bezoutlemeu  11335  bezoutlemsup  11337  dfgcd3  11338  bezout  11339  dvdsgcd  11340  dfgcd2  11342  dvdssq  11359  lcmval  11384  lcmcllem  11388  dvdslcm  11390  lcmledvds  11391  lcmgcdlem  11398  lcmdvds  11400  coprmgcdb  11409  coprmdvds2  11414  cncongr1  11424  cncongr2  11425  isprm  11430  dvdsnprmd  11446  dvdsprm  11457  exprmfct  11458  isprm6  11465  prmexpb  11469  prmfac1  11470  rpexp  11471  sqrt2irr  11480  oddpwdclemdc  11490  oddpwdc  11491  sqpweven  11492  2sqpwodd  11493  sqne2sq  11494  oddennn  11544  evenennn  11545  cncfi  11907  elcncf1di  11908