Theorem breq2 4038

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 3810	. . 3 |- ( A = B -> <. C , A >. = <. C , B >. )
2	1	eleq1d 2265	. 2 |- ( A = B -> ( <. C , A >. e. R <-> <. C , B >. e. R ) )
3		df-br 4035	. 2 |- ( C R A <-> <. C , A >. e. R )
4		df-br 4035	. 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 2167   <.cop 3626   class class class wbr 4034

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 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-v 2765  df-un 3161  df-sn 3629  df-pr 3630  df-op 3632  df-br 4035

This theorem is referenced by:  breq12  4039  breq2i  4042  breq2d  4046  nbrne1  4053  brralrspcev  4092  brimralrspcev  4093  pocl  4339  swopolem  4341  swopo  4342  sowlin  4356  sotricim  4359  sotritrieq  4361  seex  4371  frind  4388  wetriext  4614  vtoclr  4712  posng  4736  brcog  4834  brcogw  4836  opelcnvg  4847  dfdmf  4860  breldmg  4873  dfrnf  4908  dmcoss  4936  resieq  4957  dfres2  4999  elimag  5014  elrelimasn  5036  elimasn  5037  intirr  5057  poirr2  5063  poltletr  5071  dffun6f  5272  dffun4f  5275  fun11  5326  brprcneu  5554  fv3  5584  tz6.12c  5591  relelfvdm  5593  funbrfv  5602  fnbrfvb  5604  funfvdm2f  5629  fndmdif  5670  dff3im  5710  fmptco  5731  foeqcnvco  5840  isorel  5858  isocnv  5861  isotr  5866  isopolem  5872  isosolem  5874  f1oiso  5876  f1oiso2  5877  caovordig  6093  caovordg  6095  caovord  6099  caofrss  6171  caoftrn  6172  poxp  6299  tposoprab  6347  ertr  6616  ecopovsym  6699  ecopovtrn  6700  ecopovsymg  6702  ecopovtrng  6703  th3qlem2  6706  domeng  6820  eqeng  6834  snfig  6882  nneneq  6927  nnfi  6942  ssfilem  6945  domfiexmid  6948  dif1enen  6950  diffitest  6957  findcard  6958  findcard2  6959  findcard2s  6960  diffisn  6963  tridc  6969  fimax2gtrilemstep  6970  inffiexmid  6976  unsnfi  6989  fiintim  7001  fisseneq  7004  isbth  7042  supmoti  7068  eqsupti  7071  supubti  7074  suplubti  7075  suplub2ti  7076  supmaxti  7079  supsnti  7080  isotilem  7081  isoti  7082  supisolem  7083  supisoex  7084  cardcl  7261  isnumi  7262  cardval3ex  7265  exmidfodomrlemr  7283  exmidfodomrlemrALT  7284  exmidapne  7345  nqtri3or  7482  ltsonq  7484  ltanqg  7486  ltmnqg  7487  ltexnqq  7494  nsmallnqq  7498  subhalfnqq  7500  ltbtwnnqq  7501  prarloclemarch2  7505  nqnq0pi  7524  prcdnql  7570  prcunqu  7571  prnminu  7575  genpcdl  7605  genprndl  7607  genprndu  7608  genpdisj  7609  nqprm  7628  nqprrnd  7629  nqprdisj  7630  nqprloc  7631  nqprlu  7633  nqprl  7637  addnqprlemru  7644  addnqprlemfl  7645  addnqprlemfu  7646  mulnqprlemru  7660  mulnqprlemfl  7661  mulnqprlemfu  7662  1idpru  7677  ltnqpr  7679  ltnqpri  7680  prplnqu  7706  recexprlemelu  7709  recexprlemm  7710  recexprlemloc  7717  recexprlem1ssl  7719  recexprlemss1u  7722  cauappcvgprlemm  7731  cauappcvgprlemopu  7734  cauappcvgprlemupu  7735  cauappcvgprlemdisj  7737  cauappcvgprlemloc  7738  cauappcvgprlemladdfu  7740  cauappcvgprlemladdru  7742  cauappcvgprlemladdrl  7743  cauappcvgprlem2  7746  caucvgprlemnkj  7752  caucvgprlemnbj  7753  caucvgprlemm  7754  caucvgprlemopu  7757  caucvgprlemupu  7758  caucvgprlemdisj  7760  caucvgprlemloc  7761  caucvgprlemcl  7762  caucvgprlemladdfu  7763  caucvgprlemladdrl  7764  caucvgprlem2  7766  caucvgprprlemelu  7772  caucvgprprlemcbv  7773  caucvgprprlemval  7774  caucvgprprlemnbj  7779  caucvgprprlemmu  7781  caucvgprprlemexbt  7792  caucvgprprlemaddq  7794  caucvgprprlem1  7795  caucvgprprlem2  7796  suplocexprlemmu  7804  suplocexprlemru  7805  suplocexprlemdisj  7806  suplocexprlemloc  7807  suplocexprlemub  7809  suplocexpr  7811  lttrsr  7848  ltsosr  7850  ltasrg  7856  recexgt0sr  7859  mulgt0sr  7864  aptisr  7865  mulextsr1  7867  srpospr  7869  caucvgsrlemgt1  7881  caucvgsrlemoffres  7886  caucvgsr  7888  map2psrprg  7891  suplocsrlemb  7892  suplocsrlempr  7893  suplocsrlem  7894  axprecex  7966  axpre-ltwlin  7969  axpre-lttrn  7970  axpre-apti  7971  axpre-ltadd  7972  axpre-mulgt0  7973  axpre-mulext  7974  axcaucvglemcau  7984  axcaucvglemres  7985  axcaucvg  7986  axpre-suploclemres  7987  axpre-suploc  7988  ltxrlt  8111  lttri3  8125  ltne  8130  eqle  8137  ltordlem  8528  reapti  8625  apreim  8649  squeeze0  8950  lbreu  8991  lble  8993  suprleubex  9000  sup3exmid  9003  nnge1  9032  nn2ge  9042  nn1gt1  9043  nnsub  9048  nominpos  9248  nn0ge0  9293  elnnnn0b  9312  nn0ge2m1nn  9328  zdclt  9422  suprzclex  9443  peano2uz2  9452  peano5uzti  9453  dfuzi  9455  uzind  9456  uzind3  9458  eluz1  9624  uzind4  9681  indstr  9686  supinfneg  9688  infsupneg  9689  infregelbex  9691  indstr2  9702  ublbneg  9706  irrmulap  9741  elpq  9742  elpqb  9743  elrp  9749  mnfltxr  9880  nn0pnfge0  9885  xrltnsym  9887  xrlttr  9889  xrltso  9890  xrlttri3  9891  xrltne  9907  ngtmnft  9911  nmnfgt  9912  xrrebnd  9913  z2ge  9920  xltnegi  9929  xltadd1  9970  xsubge0  9975  xleaddadd  9981  ixxval  9990  elixx1  9991  elioo2  10015  iccid  10019  iccsupr  10060  repos  10064  fzval  10104  elfz1  10107  fzm1  10194  zsupcllemstep  10338  suprzubdc  10345  zsupssdc  10347  qdclt  10354  exbtwnzlemstep  10356  exbtwnzlemex  10358  qbtwnre  10365  qbtwnxr  10366  flval  10381  apbtwnz  10383  modqid2  10462  modqmuladdnn0  10479  exp3val  10652  expge0  10686  expge1  10687  nn0ltexp2  10820  facdiv  10849  facwordi  10851  hashinfom  10889  hashennn  10891  hashunlem  10915  zfz1iso  10952  wrdlen1  10991  fstwrdne0  10993  ovshftex  11003  shftfibg  11004  shftfib  11007  shftfn  11008  2shfti  11015  sqrt0rlem  11187  resqrexlemex  11209  rsqrmo  11211  resqrtcl  11213  rersqrtthlem  11214  sqrtsq  11228  cau3lem  11298  caubnd2  11301  maxleim  11389  maxabslemval  11392  maxleast  11397  maxleb  11400  fimaxre2  11411  minmax  11414  xrmaxleim  11428  xrmaxiflemval  11434  xrmaxaddlem  11444  xrminmax  11449  xrbdtri  11460  climi  11471  climeu  11480  climmo  11482  2clim  11485  addcn2  11494  mulcn2  11496  reccn2ap  11497  cn1lem  11498  summodc  11567  zsumdc  11568  fsum3  11571  cvgratz  11716  ntrivcvgap0  11733  prodmodc  11762  zproddc  11763  fprodseq  11767  fprodntrivap  11768  sinltxirr  11945  dvdsabsb  11994  0dvds  11995  alzdvds  12038  dvdsext  12039  fzo0dvdseq  12041  2tp1odd  12068  2teven  12071  divalglemnn  12102  divalglemeunn  12105  divalglemeuneg  12107  bitsinv1lem  12145  gcdval  12153  gcddvds  12157  bezoutlemstep  12191  bezoutlemmain  12192  bezoutlemex  12195  bezoutlemeu  12201  bezoutlemsup  12203  dfgcd3  12204  bezout  12205  dvdsgcd  12206  dfgcd2  12208  dvdssq  12225  uzwodc  12231  nnwofdc  12232  lcmval  12258  lcmcllem  12262  dvdslcm  12264  lcmledvds  12265  lcmgcdlem  12272  lcmdvds  12274  coprmgcdb  12283  coprmdvds2  12288  cncongr1  12298  cncongr2  12299  isprm  12304  dvdsnprmd  12320  dvdsprm  12332  exprmfct  12333  isprm6  12342  prmexpb  12346  prmfac1  12347  rpexp  12348  sqrt2irr  12357  oddpwdclemdc  12368  oddpwdc  12369  sqpweven  12370  2sqpwodd  12371  sqne2sq  12372  nnoddn2prmb  12458  pceu  12491  pczpre  12493  pcdiv  12498  pcdvdsb  12516  difsqpwdvds  12534  pcmpt  12539  pcmptdvds  12541  oddprmdvds  12550  prmpwdvds  12551  infpnlem2  12556  oddennn  12636  evenennn  12637  exmidunben  12670  nninfdclemcl  12692  nninfdclemp1  12694  nninfdc  12697  infpn2  12700  eqgen  13435  zndvds  14283  znleval  14287  comet  14843  metcnpi  14859  metcnpi2  14860  metcnpi3  14861  addcncntoplem  14905  cncfi  14922  elcncf1di  14923  mulcncflem  14951  dedekindeulemuub  14961  dedekindeulemloc  14963  dedekindeulemlu  14965  dedekindeulemeu  14966  dedekindeu  14967  suplociccreex  14968  suplociccex  14969  dedekindicclemuub  14970  dedekindicclemloc  14972  dedekindicclemlu  14974  dedekindicclemeu  14975  dedekindicclemicc  14976  dedekindicc  14977  ivthinclemlopn  14980  ivthinclemlr  14981  ivthinclemuopn  14982  ivthinclemur  14983  ivthinclemloc  14985  ivthinc  14987  ivthreinc  14989  dich0  14996  ivthdich  14997  limcimo  15009  cnplimclemr  15013  limccnp2lem  15020  limccoap  15022  eldvap  15026  logltb  15218  lgsdir  15384  lgsne0  15387  gausslemma2dlem0i  15406  lgsquadlem1  15426  lgsquadlem2  15427  lgsquadlem3  15428  2lgslem2  15441  2lgs  15453  2sqlem6  15469  2sqlem8  15472  2sqlem10  15474  sbthom  15783  trilpo  15800  trirec0  15801  apdiff  15805  reap0  15815  cndcap  15816  nconstwlpolem  15822  neapmkv  15825  neap0mkv  15826  ltlenmkv  15827