Theorem breq2 4034

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 3806	. . 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 4031	. 2 |- ( C R A <-> <. C , A >. e. R )
4		df-br 4031	. 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 3622   class class class wbr 4030

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 3158  df-sn 3625  df-pr 3626  df-op 3628  df-br 4031

This theorem is referenced by:  breq12  4035  breq2i  4038  breq2d  4042  nbrne1  4049  brralrspcev  4088  brimralrspcev  4089  pocl  4335  swopolem  4337  swopo  4338  sowlin  4352  sotricim  4355  sotritrieq  4357  seex  4367  frind  4384  wetriext  4610  vtoclr  4708  posng  4732  brcog  4830  brcogw  4832  opelcnvg  4843  dfdmf  4856  breldmg  4869  dfrnf  4904  dmcoss  4932  resieq  4953  dfres2  4995  elimag  5010  elrelimasn  5032  elimasn  5033  intirr  5053  poirr2  5059  poltletr  5067  dffun6f  5268  dffun4f  5271  fun11  5322  brprcneu  5548  fv3  5578  tz6.12c  5585  relelfvdm  5587  funbrfv  5596  fnbrfvb  5598  funfvdm2f  5623  fndmdif  5664  dff3im  5704  fmptco  5725  foeqcnvco  5834  isorel  5852  isocnv  5855  isotr  5860  isopolem  5866  isosolem  5868  f1oiso  5870  f1oiso2  5871  caovordig  6086  caovordg  6088  caovord  6092  caofrss  6159  caoftrn  6160  poxp  6287  tposoprab  6335  ertr  6604  ecopovsym  6687  ecopovtrn  6688  ecopovsymg  6690  ecopovtrng  6691  th3qlem2  6694  domeng  6808  eqeng  6822  snfig  6870  nneneq  6915  nnfi  6930  ssfilem  6933  domfiexmid  6936  dif1enen  6938  diffitest  6945  findcard  6946  findcard2  6947  findcard2s  6948  diffisn  6951  tridc  6957  fimax2gtrilemstep  6958  inffiexmid  6964  unsnfi  6977  fiintim  6987  fisseneq  6990  isbth  7028  supmoti  7054  eqsupti  7057  supubti  7060  suplubti  7061  suplub2ti  7062  supmaxti  7065  supsnti  7066  isotilem  7067  isoti  7068  supisolem  7069  supisoex  7070  cardcl  7243  isnumi  7244  cardval3ex  7247  exmidfodomrlemr  7264  exmidfodomrlemrALT  7265  exmidapne  7322  nqtri3or  7458  ltsonq  7460  ltanqg  7462  ltmnqg  7463  ltexnqq  7470  nsmallnqq  7474  subhalfnqq  7476  ltbtwnnqq  7477  prarloclemarch2  7481  nqnq0pi  7500  prcdnql  7546  prcunqu  7547  prnminu  7551  genpcdl  7581  genprndl  7583  genprndu  7584  genpdisj  7585  nqprm  7604  nqprrnd  7605  nqprdisj  7606  nqprloc  7607  nqprlu  7609  nqprl  7613  addnqprlemru  7620  addnqprlemfl  7621  addnqprlemfu  7622  mulnqprlemru  7636  mulnqprlemfl  7637  mulnqprlemfu  7638  1idpru  7653  ltnqpr  7655  ltnqpri  7656  prplnqu  7682  recexprlemelu  7685  recexprlemm  7686  recexprlemloc  7693  recexprlem1ssl  7695  recexprlemss1u  7698  cauappcvgprlemm  7707  cauappcvgprlemopu  7710  cauappcvgprlemupu  7711  cauappcvgprlemdisj  7713  cauappcvgprlemloc  7714  cauappcvgprlemladdfu  7716  cauappcvgprlemladdru  7718  cauappcvgprlemladdrl  7719  cauappcvgprlem2  7722  caucvgprlemnkj  7728  caucvgprlemnbj  7729  caucvgprlemm  7730  caucvgprlemopu  7733  caucvgprlemupu  7734  caucvgprlemdisj  7736  caucvgprlemloc  7737  caucvgprlemcl  7738  caucvgprlemladdfu  7739  caucvgprlemladdrl  7740  caucvgprlem2  7742  caucvgprprlemelu  7748  caucvgprprlemcbv  7749  caucvgprprlemval  7750  caucvgprprlemnbj  7755  caucvgprprlemmu  7757  caucvgprprlemexbt  7768  caucvgprprlemaddq  7770  caucvgprprlem1  7771  caucvgprprlem2  7772  suplocexprlemmu  7780  suplocexprlemru  7781  suplocexprlemdisj  7782  suplocexprlemloc  7783  suplocexprlemub  7785  suplocexpr  7787  lttrsr  7824  ltsosr  7826  ltasrg  7832  recexgt0sr  7835  mulgt0sr  7840  aptisr  7841  mulextsr1  7843  srpospr  7845  caucvgsrlemgt1  7857  caucvgsrlemoffres  7862  caucvgsr  7864  map2psrprg  7867  suplocsrlemb  7868  suplocsrlempr  7869  suplocsrlem  7870  axprecex  7942  axpre-ltwlin  7945  axpre-lttrn  7946  axpre-apti  7947  axpre-ltadd  7948  axpre-mulgt0  7949  axpre-mulext  7950  axcaucvglemcau  7960  axcaucvglemres  7961  axcaucvg  7962  axpre-suploclemres  7963  axpre-suploc  7964  ltxrlt  8087  lttri3  8101  ltne  8106  eqle  8113  ltordlem  8503  reapti  8600  apreim  8624  squeeze0  8925  lbreu  8966  lble  8968  suprleubex  8975  sup3exmid  8978  nnge1  9007  nn2ge  9017  nn1gt1  9018  nnsub  9023  nominpos  9223  nn0ge0  9268  elnnnn0b  9287  nn0ge2m1nn  9303  zdclt  9397  suprzclex  9418  peano2uz2  9427  peano5uzti  9428  dfuzi  9430  uzind  9431  uzind3  9433  eluz1  9599  uzind4  9656  indstr  9661  supinfneg  9663  infsupneg  9664  infregelbex  9666  indstr2  9677  ublbneg  9681  irrmulap  9716  elpq  9717  elpqb  9718  elrp  9724  mnfltxr  9855  nn0pnfge0  9860  xrltnsym  9862  xrlttr  9864  xrltso  9865  xrlttri3  9866  xrltne  9882  ngtmnft  9886  nmnfgt  9887  xrrebnd  9888  z2ge  9895  xltnegi  9904  xltadd1  9945  xsubge0  9950  xleaddadd  9956  ixxval  9965  elixx1  9966  elioo2  9990  iccid  9994  iccsupr  10035  repos  10039  fzval  10079  elfz1  10082  fzm1  10169  qdclt  10318  exbtwnzlemstep  10319  exbtwnzlemex  10321  qbtwnre  10328  qbtwnxr  10329  flval  10344  apbtwnz  10346  modqid2  10425  modqmuladdnn0  10442  exp3val  10615  expge0  10649  expge1  10650  nn0ltexp2  10783  facdiv  10812  facwordi  10814  hashinfom  10852  hashennn  10854  hashunlem  10878  zfz1iso  10915  wrdlen1  10954  fstwrdne0  10956  ovshftex  10966  shftfibg  10967  shftfib  10970  shftfn  10971  2shfti  10978  sqrt0rlem  11150  resqrexlemex  11172  rsqrmo  11174  resqrtcl  11176  rersqrtthlem  11177  sqrtsq  11191  cau3lem  11261  caubnd2  11264  maxleim  11352  maxabslemval  11355  maxleast  11360  maxleb  11363  fimaxre2  11373  minmax  11376  xrmaxleim  11390  xrmaxiflemval  11396  xrmaxaddlem  11406  xrminmax  11411  xrbdtri  11422  climi  11433  climeu  11442  climmo  11444  2clim  11447  addcn2  11456  mulcn2  11458  reccn2ap  11459  cn1lem  11460  summodc  11529  zsumdc  11530  fsum3  11533  cvgratz  11678  ntrivcvgap0  11695  prodmodc  11724  zproddc  11725  fprodseq  11729  fprodntrivap  11730  sinltxirr  11907  dvdsabsb  11956  0dvds  11957  alzdvds  11999  dvdsext  12000  fzo0dvdseq  12002  2tp1odd  12028  2teven  12031  divalglemnn  12062  divalglemeunn  12065  divalglemeuneg  12067  zsupcllemstep  12085  suprzubdc  12092  zsupssdc  12094  gcdval  12099  gcddvds  12103  bezoutlemstep  12137  bezoutlemmain  12138  bezoutlemex  12141  bezoutlemeu  12147  bezoutlemsup  12149  dfgcd3  12150  bezout  12151  dvdsgcd  12152  dfgcd2  12154  dvdssq  12171  uzwodc  12177  nnwofdc  12178  lcmval  12204  lcmcllem  12208  dvdslcm  12210  lcmledvds  12211  lcmgcdlem  12218  lcmdvds  12220  coprmgcdb  12229  coprmdvds2  12234  cncongr1  12244  cncongr2  12245  isprm  12250  dvdsnprmd  12266  dvdsprm  12278  exprmfct  12279  isprm6  12288  prmexpb  12292  prmfac1  12293  rpexp  12294  sqrt2irr  12303  oddpwdclemdc  12314  oddpwdc  12315  sqpweven  12316  2sqpwodd  12317  sqne2sq  12318  nnoddn2prmb  12403  pceu  12436  pczpre  12438  pcdiv  12443  pcdvdsb  12461  difsqpwdvds  12479  pcmpt  12484  pcmptdvds  12486  oddprmdvds  12495  prmpwdvds  12496  infpnlem2  12501  oddennn  12552  evenennn  12553  exmidunben  12586  nninfdclemcl  12608  nninfdclemp1  12610  nninfdc  12613  infpn2  12616  eqgen  13300  zndvds  14148  znleval  14152  comet  14678  metcnpi  14694  metcnpi2  14695  metcnpi3  14696  addcncntoplem  14740  cncfi  14757  elcncf1di  14758  mulcncflem  14786  dedekindeulemuub  14796  dedekindeulemloc  14798  dedekindeulemlu  14800  dedekindeulemeu  14801  dedekindeu  14802  suplociccreex  14803  suplociccex  14804  dedekindicclemuub  14805  dedekindicclemloc  14807  dedekindicclemlu  14809  dedekindicclemeu  14810  dedekindicclemicc  14811  dedekindicc  14812  ivthinclemlopn  14815  ivthinclemlr  14816  ivthinclemuopn  14817  ivthinclemur  14818  ivthinclemloc  14820  ivthinc  14822  ivthreinc  14824  dich0  14831  ivthdich  14832  limcimo  14844  cnplimclemr  14848  limccnp2lem  14855  limccoap  14857  eldvap  14861  logltb  15050  lgsdir  15192  lgsne0  15195  gausslemma2dlem0i  15214  lgsquadlem1  15234  lgsquadlem2  15235  lgsquadlem3  15236  2lgslem2  15249  2lgs  15261  2sqlem6  15277  2sqlem8  15280  2sqlem10  15282  sbthom  15586  trilpo  15603  trirec0  15604  apdiff  15608  reap0  15618  cndcap  15619  nconstwlpolem  15625  neapmkv  15628  neap0mkv  15629  ltlenmkv  15630