Theorem breq2 4135

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 3905	. . 3 |- ( A = B -> <. C , A >. = <. C , B >. )
2	1	eleq1d 2307	. 2 |- ( A = B -> ( <. C , A >. e. R <-> <. C , B >. e. R ) )
3		df-br 4132	. 2 |- ( C R A <-> <. C , A >. e. R )
4		df-br 4132	. 2 |- ( C R B <-> <. C , B >. e. R )
5	2, 3, 4	3bitr4g 223	1 |- ( A = B -> ( C R A <-> C R B ) )

This proof depends on syntax axioms:   -> wi 4   <-> wb 105   = wceq 1402   e. wcel 2209   <.cop 3712   class class class wbr 4131

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-3an 1011  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-v 2823  df-un 3224  df-sn 3715  df-pr 3716  df-op 3718  df-br 4132

This theorem is used by:  breq12  4136  breq2i  4139  breq2d  4143  nbrne1  4150  brralrspcev  4190  brimralrspcev  4191  pocl  4450  swopolem  4452  swopo  4453  sowlin  4467  sotricim  4470  sotritrieq  4472  seex  4482  frind  4499  wetriext  4726  vtoclr  4825  posng  4849  brcog  4949  brcogw  4951  opelcnvg  4962  dfdmf  4976  breldmg  4989  dfrnf  5025  dmcoss  5054  resieq  5075  dfres2  5118  elimag  5133  elrelimasn  5156  elimasn  5157  intirr  5177  poirr2  5183  poltletr  5191  dffun6f  5393  dffun4f  5396  fun11  5451  brprcneu  5691  fv3  5721  tz6.12c  5728  relelfvdm  5730  fvmbr  5734  funbrfv  5742  fnbrfvb  5744  funfvdm2f  5771  fndmdif  5817  dff3im  5856  fmptco  5877  foeqcnvco  5999  isorel  6017  isocnv  6020  isotr  6025  isopolem  6031  isosolem  6033  f1oiso  6035  f1oiso2  6036  caovordig  6258  caovordg  6260  caovord  6264  caofrss  6338  caoftrn  6339  poxp  6472  tposoprab  6555  ertr  6826  ecopovsym  6909  ecopovtrn  6910  ecopovsymg  6912  ecopovtrng  6913  th3qlem2  6916  domeng  7040  eqeng  7056  snfig  7107  nneneq  7162  nnfi  7178  ssfilem  7181  ssfilemd  7183  domfiexmid  7186  dif1enen  7188  diffitest  7195  findcard  7196  findcard2  7197  findcard2s  7198  diffisn  7201  tridc  7208  fimax2gtrilemstep  7209  inffiexmid  7217  unsnfi  7230  fiintim  7242  fisseneq  7246  isbth  7289  supmoti  7339  eqsupti  7342  supubti  7345  suplubti  7346  suplub2ti  7347  supmaxti  7350  supsnti  7351  isotilem  7352  isoti  7353  supisolem  7354  supisoex  7355  cardcl  7532  isnumi  7533  cardval3ex  7536  exmidfodomrlemr  7560  exmidfodomrlemrALT  7561  papsym  7618  papcotr  7619  exmidapne  7632  nqtri3or  7769  ltsonq  7771  ltanqg  7773  ltmnqg  7774  ltexnqq  7781  nsmallnqq  7785  subhalfnqq  7787  ltbtwnnqq  7788  prarloclemarch2  7792  nqnq0pi  7811  prcdnql  7857  prcunqu  7858  prnminu  7862  genpcdl  7892  genprndl  7894  genprndu  7895  genpdisj  7896  nqprm  7915  nqprrnd  7916  nqprdisj  7917  nqprloc  7918  nqprlu  7920  nqprl  7924  addnqprlemru  7931  addnqprlemfl  7932  addnqprlemfu  7933  mulnqprlemru  7947  mulnqprlemfl  7948  mulnqprlemfu  7949  1idpru  7964  ltnqpr  7966  ltnqpri  7967  prplnqu  7993  recexprlemelu  7996  recexprlemm  7997  recexprlemloc  8004  recexprlem1ssl  8006  recexprlemss1u  8009  cauappcvgprlemm  8018  cauappcvgprlemopu  8021  cauappcvgprlemupu  8022  cauappcvgprlemdisj  8024  cauappcvgprlemloc  8025  cauappcvgprlemladdfu  8027  cauappcvgprlemladdru  8029  cauappcvgprlemladdrl  8030  cauappcvgprlem2  8033  caucvgprlemnkj  8039  caucvgprlemnbj  8040  caucvgprlemm  8041  caucvgprlemopu  8044  caucvgprlemupu  8045  caucvgprlemdisj  8047  caucvgprlemloc  8048  caucvgprlemcl  8049  caucvgprlemladdfu  8050  caucvgprlemladdrl  8051  caucvgprlem2  8053  caucvgprprlemelu  8059  caucvgprprlemcbv  8060  caucvgprprlemval  8061  caucvgprprlemnbj  8066  caucvgprprlemmu  8068  caucvgprprlemexbt  8079  caucvgprprlemaddq  8081  caucvgprprlem1  8082  caucvgprprlem2  8083  suplocexprlemmu  8091  suplocexprlemru  8092  suplocexprlemdisj  8093  suplocexprlemloc  8094  suplocexprlemub  8096  suplocexpr  8098  lttrsr  8135  ltsosr  8137  ltasrg  8143  recexgt0sr  8146  mulgt0sr  8151  aptisr  8152  mulextsr1  8154  srpospr  8156  caucvgsrlemgt1  8168  caucvgsrlemoffres  8173  caucvgsr  8175  map2psrprg  8178  suplocsrlemb  8179  suplocsrlempr  8180  suplocsrlem  8181  axprecex  8253  axpre-ltwlin  8256  axpre-lttrn  8257  axpre-apti  8258  axpre-ltadd  8259  axpre-mulgt0  8260  axpre-mulext  8261  axcaucvglemcau  8271  axcaucvglemres  8272  axcaucvg  8273  axpre-suploclemres  8274  axpre-suploc  8275  ltxrlt  8397  lttri3  8411  ltne  8416  eqle  8423  ltordlem  8817  reapti  8915  apreim  8939  squeeze0  9242  lbreu  9283  lble  9285  suprleubex  9292  sup3exmid  9295  nnge1  9336  nn2ge  9346  nn1gt1  9347  nnsub  9352  nominpos  9554  nn0ge0  9599  elnnnn0b  9618  nn0ge2m1nn  9638  zdclt  9733  suprzclex  9755  peano2uz2  9764  peano5uzti  9765  dfuzi  9767  uzind  9768  uzind3  9770  eluz1  9941  uzind4  10004  indstr  10009  supinfneg  10011  infsupneg  10012  infregelbex  10014  indstr2  10025  ublbneg  10029  irraddap  10063  irrmulap  10065  elpq  10066  elpqb  10067  elrp  10073  mnfltxr  10205  nn0pnfge0  10210  xrltnsym  10212  xrlttr  10214  xrltso  10215  xrlttri3  10216  xrltne  10232  ngtmnft  10236  nmnfgt  10237  xrrebnd  10238  z2ge  10245  xltnegi  10254  xltadd1  10295  xsubge0  10300  xleaddadd  10306  ixxval  10315  elixx1  10316  elioo2  10340  iccid  10344  iccsupr  10385  repos  10389  fzval  10430  elfz1  10433  fzm1  10524  zsupcllemstep  10679  suprzubdc  10688  zsupssdc  10690  qdclt  10697  exbtwnzlemstep  10699  exbtwnzlemex  10701  qbtwnre  10708  qbtwnxr  10709  flval  10724  apbtwnz  10726  flaplt  10739  modqid2  10809  modqmuladdnn0  10826  exp3val  10999  expge0  11033  expge1  11034  nn0ltexp2  11169  facdiv  11198  facwordi  11200  hashinfom  11239  hashennn  11241  hashunlem  11266  zfz1iso  11315  wrdlen1  11364  fstwrdne0  11366  wrdl1exs1  11419  pfxsuffeqwrdeq  11492  pfxsuff1eqwrdeq  11493  ccats1pfxeq  11508  ccats1pfxeqrex  11509  pfxccatin12lem3  11526  ovshftex  11606  shftfibg  11607  shftfib  11610  shftfn  11611  2shfti  11618  sqrt0rlem  11791  resqrexlemex  11813  rsqrmo  11815  resqrtcl  11817  rersqrtthlem  11818  sqrtsq  11832  cau3lem  11903  caubnd2  11906  maxleim  11994  maxabslemval  11997  maxleast  12002  maxleb  12005  fimaxre2  12016  fiidxsupcl  12018  minmax  12020  xrmaxleim  12035  xrmaxiflemval  12041  xrmaxaddlem  12051  xrminmax  12056  xrbdtri  12067  climi  12078  climeu  12087  climmo  12089  2clim  12092  addcn2  12101  mulcn2  12103  reccn2ap  12104  cn1lem  12105  summodc  12175  zsumdc  12176  fsum3  12179  cvgratz  12324  ntrivcvgap0  12341  prodmodc  12370  zproddc  12371  fprodseq  12375  fprodntrivap  12376  sinltxirr  12553  dvdsabsb  12602  0dvds  12603  alzdvds  12646  dvdsext  12647  fzo0dvdseq  12649  2tp1odd  12676  2teven  12679  divalglemnn  12710  divalglemeunn  12713  divalglemeuneg  12715  bitsinv1lem  12753  gcdval  12761  gcddvds  12765  bezoutlemstep  12799  bezoutlemmain  12800  bezoutlemex  12803  bezoutlemeu  12809  bezoutlemsup  12811  dfgcd3  12812  bezout  12813  dvdsgcd  12814  dfgcd2  12816  dvdssq  12833  uzwodc  12839  nnwofdc  12840  lcmval  12866  lcmcllem  12870  dvdslcm  12872  lcmledvds  12873  lcmgcdlem  12880  lcmdvds  12882  coprmgcdb  12891  coprmdvds2  12896  cncongr1  12906  cncongr2  12907  isprm  12912  dvdsnprmd  12928  dvdsprm  12941  exprmfct  12942  isprm6  12951  prmexpb  12955  prmfac1  12956  rpexp  12957  sqrt2irr  12966  nnmaxpwlemparts  12977  nnmaxpw  12978  sqpweven  12980  2sqpwodd  12981  sqne2sq  12982  nnoddn2prmb  13070  pceu  13103  pczpre  13105  pcdiv  13110  pcdvdsb  13128  difsqpwdvds  13146  pcmpt  13151  pcmptdvds  13153  oddprmdvds  13162  prmpwdvds  13163  infpnlem2  13168  ballotfilemfcc  13291  oddennn  13341  evenennn  13342  exmidunben  13375  nninfdclemcl  13397  nninfdclemp1  13399  nninfdc  13402  infpn2  13405  eqgen  14089  zndvds  15093  znleval  15097  psrass1filem  15177  psrmulvalfi  15188  comet  15725  metcnpi  15741  metcnpi2  15742  metcnpi3  15743  addcncntoplem  15787  cncfi  15804  elcncf1di  15805  mulcncflem  15833  dedekindeulemuub  15843  dedekindeulemloc  15845  dedekindeulemlu  15847  dedekindeulemeu  15848  dedekindeu  15849  suplociccreex  15850  suplociccex  15851  dedekindicclemuub  15852  dedekindicclemloc  15854  dedekindicclemlu  15856  dedekindicclemeu  15857  dedekindicclemicc  15858  dedekindicc  15859  ivthinclemlopn  15862  ivthinclemlr  15863  ivthinclemuopn  15864  ivthinclemur  15865  ivthinclemloc  15867  ivthinc  15869  ivthreinc  15871  dich0  15878  ivthdich  15879  limcimo  15891  cnplimclemr  15895  limccnp2lem  15902  limccoap  15904  eldvap  15908  logltb  16104  zprmlogbaplem3  16217  zprmlogbap  16218  pellexlem3  16231  ppiublem1  16291  chtqub  16296  bpos1lem  16309  bposlem9  16319  lgsdir  16359  lgsne0  16362  gausslemma2dlem0i  16381  lgsquadlem1  16401  lgsquadlem2  16402  lgsquadlem3  16403  2lgslem2  16416  2lgs  16428  2sqlem6  16444  2sqlem8  16447  2sqlem10  16449  lfgredg2dom  16578  istrl  16831  clwwlkn0  16854  clwwlkext2edg  16868  clwwlknonccat  16879  clwwlknonex2  16885  iseupth  16893  konigsberg  16939  lealltlt2  16957  sbthom  17277  rirrdisj  17291  trilpo  17299  trirec0  17300  apdiff  17304  reap0  17315  cndcap  17316  nconstwlpolem  17322  neapmkv  17325  neap0mkv  17326  ltlenmkv  17327