Theorem breq2 4087

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 3858	. . 3 |- ( A = B -> <. C , A >. = <. C , B >. )
2	1	eleq1d 2298	. 2 |- ( A = B -> ( <. C , A >. e. R <-> <. C , B >. e. R ) )
3		df-br 4084	. 2 |- ( C R A <-> <. C , A >. e. R )
4		df-br 4084	. 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 1395   e. wcel 2200   <.cop 3669   class class class wbr 4083

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-v 2801  df-un 3201  df-sn 3672  df-pr 3673  df-op 3675  df-br 4084

This theorem is referenced by:  breq12  4088  breq2i  4091  breq2d  4095  nbrne1  4102  brralrspcev  4142  brimralrspcev  4143  pocl  4394  swopolem  4396  swopo  4397  sowlin  4411  sotricim  4414  sotritrieq  4416  seex  4426  frind  4443  wetriext  4669  vtoclr  4767  posng  4791  brcog  4889  brcogw  4891  opelcnvg  4902  dfdmf  4916  breldmg  4929  dfrnf  4965  dmcoss  4994  resieq  5015  dfres2  5057  elimag  5072  elrelimasn  5094  elimasn  5095  intirr  5115  poirr2  5121  poltletr  5129  dffun6f  5331  dffun4f  5334  fun11  5388  brprcneu  5620  fv3  5650  tz6.12c  5657  relelfvdm  5659  fvmbr  5662  funbrfv  5670  fnbrfvb  5672  funfvdm2f  5699  fndmdif  5740  dff3im  5780  fmptco  5801  foeqcnvco  5914  isorel  5932  isocnv  5935  isotr  5940  isopolem  5946  isosolem  5948  f1oiso  5950  f1oiso2  5951  caovordig  6171  caovordg  6173  caovord  6177  caofrss  6250  caoftrn  6251  poxp  6378  tposoprab  6426  ertr  6695  ecopovsym  6778  ecopovtrn  6779  ecopovsymg  6781  ecopovtrng  6782  th3qlem2  6785  domeng  6901  eqeng  6917  snfig  6967  nneneq  7018  nnfi  7034  ssfilem  7037  domfiexmid  7040  dif1enen  7042  diffitest  7049  findcard  7050  findcard2  7051  findcard2s  7052  diffisn  7055  tridc  7061  fimax2gtrilemstep  7062  inffiexmid  7068  unsnfi  7081  fiintim  7093  fisseneq  7096  isbth  7134  supmoti  7160  eqsupti  7163  supubti  7166  suplubti  7167  suplub2ti  7168  supmaxti  7171  supsnti  7172  isotilem  7173  isoti  7174  supisolem  7175  supisoex  7176  cardcl  7353  isnumi  7354  cardval3ex  7357  exmidfodomrlemr  7380  exmidfodomrlemrALT  7381  exmidapne  7446  nqtri3or  7583  ltsonq  7585  ltanqg  7587  ltmnqg  7588  ltexnqq  7595  nsmallnqq  7599  subhalfnqq  7601  ltbtwnnqq  7602  prarloclemarch2  7606  nqnq0pi  7625  prcdnql  7671  prcunqu  7672  prnminu  7676  genpcdl  7706  genprndl  7708  genprndu  7709  genpdisj  7710  nqprm  7729  nqprrnd  7730  nqprdisj  7731  nqprloc  7732  nqprlu  7734  nqprl  7738  addnqprlemru  7745  addnqprlemfl  7746  addnqprlemfu  7747  mulnqprlemru  7761  mulnqprlemfl  7762  mulnqprlemfu  7763  1idpru  7778  ltnqpr  7780  ltnqpri  7781  prplnqu  7807  recexprlemelu  7810  recexprlemm  7811  recexprlemloc  7818  recexprlem1ssl  7820  recexprlemss1u  7823  cauappcvgprlemm  7832  cauappcvgprlemopu  7835  cauappcvgprlemupu  7836  cauappcvgprlemdisj  7838  cauappcvgprlemloc  7839  cauappcvgprlemladdfu  7841  cauappcvgprlemladdru  7843  cauappcvgprlemladdrl  7844  cauappcvgprlem2  7847  caucvgprlemnkj  7853  caucvgprlemnbj  7854  caucvgprlemm  7855  caucvgprlemopu  7858  caucvgprlemupu  7859  caucvgprlemdisj  7861  caucvgprlemloc  7862  caucvgprlemcl  7863  caucvgprlemladdfu  7864  caucvgprlemladdrl  7865  caucvgprlem2  7867  caucvgprprlemelu  7873  caucvgprprlemcbv  7874  caucvgprprlemval  7875  caucvgprprlemnbj  7880  caucvgprprlemmu  7882  caucvgprprlemexbt  7893  caucvgprprlemaddq  7895  caucvgprprlem1  7896  caucvgprprlem2  7897  suplocexprlemmu  7905  suplocexprlemru  7906  suplocexprlemdisj  7907  suplocexprlemloc  7908  suplocexprlemub  7910  suplocexpr  7912  lttrsr  7949  ltsosr  7951  ltasrg  7957  recexgt0sr  7960  mulgt0sr  7965  aptisr  7966  mulextsr1  7968  srpospr  7970  caucvgsrlemgt1  7982  caucvgsrlemoffres  7987  caucvgsr  7989  map2psrprg  7992  suplocsrlemb  7993  suplocsrlempr  7994  suplocsrlem  7995  axprecex  8067  axpre-ltwlin  8070  axpre-lttrn  8071  axpre-apti  8072  axpre-ltadd  8073  axpre-mulgt0  8074  axpre-mulext  8075  axcaucvglemcau  8085  axcaucvglemres  8086  axcaucvg  8087  axpre-suploclemres  8088  axpre-suploc  8089  ltxrlt  8212  lttri3  8226  ltne  8231  eqle  8238  ltordlem  8629  reapti  8726  apreim  8750  squeeze0  9051  lbreu  9092  lble  9094  suprleubex  9101  sup3exmid  9104  nnge1  9133  nn2ge  9143  nn1gt1  9144  nnsub  9149  nominpos  9349  nn0ge0  9394  elnnnn0b  9413  nn0ge2m1nn  9429  zdclt  9524  suprzclex  9545  peano2uz2  9554  peano5uzti  9555  dfuzi  9557  uzind  9558  uzind3  9560  eluz1  9726  uzind4  9783  indstr  9788  supinfneg  9790  infsupneg  9791  infregelbex  9793  indstr2  9804  ublbneg  9808  irrmulap  9843  elpq  9844  elpqb  9845  elrp  9851  mnfltxr  9982  nn0pnfge0  9987  xrltnsym  9989  xrlttr  9991  xrltso  9992  xrlttri3  9993  xrltne  10009  ngtmnft  10013  nmnfgt  10014  xrrebnd  10015  z2ge  10022  xltnegi  10031  xltadd1  10072  xsubge0  10077  xleaddadd  10083  ixxval  10092  elixx1  10093  elioo2  10117  iccid  10121  iccsupr  10162  repos  10166  fzval  10206  elfz1  10209  fzm1  10296  zsupcllemstep  10449  suprzubdc  10456  zsupssdc  10458  qdclt  10465  exbtwnzlemstep  10467  exbtwnzlemex  10469  qbtwnre  10476  qbtwnxr  10477  flval  10492  apbtwnz  10494  modqid2  10573  modqmuladdnn0  10590  exp3val  10763  expge0  10797  expge1  10798  nn0ltexp2  10931  facdiv  10960  facwordi  10962  hashinfom  11000  hashennn  11002  hashunlem  11026  zfz1iso  11063  wrdlen1  11109  fstwrdne0  11111  wrdl1exs1  11162  pfxsuffeqwrdeq  11230  pfxsuff1eqwrdeq  11231  ccats1pfxeq  11246  ccats1pfxeqrex  11247  pfxccatin12lem3  11264  ovshftex  11330  shftfibg  11331  shftfib  11334  shftfn  11335  2shfti  11342  sqrt0rlem  11514  resqrexlemex  11536  rsqrmo  11538  resqrtcl  11540  rersqrtthlem  11541  sqrtsq  11555  cau3lem  11625  caubnd2  11628  maxleim  11716  maxabslemval  11719  maxleast  11724  maxleb  11727  fimaxre2  11738  minmax  11741  xrmaxleim  11755  xrmaxiflemval  11761  xrmaxaddlem  11771  xrminmax  11776  xrbdtri  11787  climi  11798  climeu  11807  climmo  11809  2clim  11812  addcn2  11821  mulcn2  11823  reccn2ap  11824  cn1lem  11825  summodc  11894  zsumdc  11895  fsum3  11898  cvgratz  12043  ntrivcvgap0  12060  prodmodc  12089  zproddc  12090  fprodseq  12094  fprodntrivap  12095  sinltxirr  12272  dvdsabsb  12321  0dvds  12322  alzdvds  12365  dvdsext  12366  fzo0dvdseq  12368  2tp1odd  12395  2teven  12398  divalglemnn  12429  divalglemeunn  12432  divalglemeuneg  12434  bitsinv1lem  12472  gcdval  12480  gcddvds  12484  bezoutlemstep  12518  bezoutlemmain  12519  bezoutlemex  12522  bezoutlemeu  12528  bezoutlemsup  12530  dfgcd3  12531  bezout  12532  dvdsgcd  12533  dfgcd2  12535  dvdssq  12552  uzwodc  12558  nnwofdc  12559  lcmval  12585  lcmcllem  12589  dvdslcm  12591  lcmledvds  12592  lcmgcdlem  12599  lcmdvds  12601  coprmgcdb  12610  coprmdvds2  12615  cncongr1  12625  cncongr2  12626  isprm  12631  dvdsnprmd  12647  dvdsprm  12659  exprmfct  12660  isprm6  12669  prmexpb  12673  prmfac1  12674  rpexp  12675  sqrt2irr  12684  oddpwdclemdc  12695  oddpwdc  12696  sqpweven  12697  2sqpwodd  12698  sqne2sq  12699  nnoddn2prmb  12785  pceu  12818  pczpre  12820  pcdiv  12825  pcdvdsb  12843  difsqpwdvds  12861  pcmpt  12866  pcmptdvds  12868  oddprmdvds  12877  prmpwdvds  12878  infpnlem2  12883  oddennn  12963  evenennn  12964  exmidunben  12997  nninfdclemcl  13019  nninfdclemp1  13021  nninfdc  13024  infpn2  13027  eqgen  13764  zndvds  14613  znleval  14617  comet  15173  metcnpi  15189  metcnpi2  15190  metcnpi3  15191  addcncntoplem  15235  cncfi  15252  elcncf1di  15253  mulcncflem  15281  dedekindeulemuub  15291  dedekindeulemloc  15293  dedekindeulemlu  15295  dedekindeulemeu  15296  dedekindeu  15297  suplociccreex  15298  suplociccex  15299  dedekindicclemuub  15300  dedekindicclemloc  15302  dedekindicclemlu  15304  dedekindicclemeu  15305  dedekindicclemicc  15306  dedekindicc  15307  ivthinclemlopn  15310  ivthinclemlr  15311  ivthinclemuopn  15312  ivthinclemur  15313  ivthinclemloc  15315  ivthinc  15317  ivthreinc  15319  dich0  15326  ivthdich  15327  limcimo  15339  cnplimclemr  15343  limccnp2lem  15350  limccoap  15352  eldvap  15356  logltb  15548  lgsdir  15714  lgsne0  15717  gausslemma2dlem0i  15736  lgsquadlem1  15756  lgsquadlem2  15757  lgsquadlem3  15758  2lgslem2  15771  2lgs  15783  2sqlem6  15799  2sqlem8  15802  2sqlem10  15804  lfgredg2dom  15930  sbthom  16394  trilpo  16411  trirec0  16412  apdiff  16416  reap0  16426  cndcap  16427  nconstwlpolem  16433  neapmkv  16436  neap0mkv  16437  ltlenmkv  16438