Theorem breq2 4115

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 3886	. . 3 |- ( A = B -> <. C , A >. = <. C , B >. )
2	1	eleq1d 2303	. 2 |- ( A = B -> ( <. C , A >. e. R <-> <. C , B >. e. R ) )
3		df-br 4112	. 2 |- ( C R A <-> <. C , A >. e. R )
4		df-br 4112	. 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 1398   e. wcel 2205   <.cop 3694   class class class wbr 4111

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-v 2817  df-un 3217  df-sn 3697  df-pr 3698  df-op 3700  df-br 4112

This theorem is referenced by:  breq12  4116  breq2i  4119  breq2d  4123  nbrne1  4130  brralrspcev  4170  brimralrspcev  4171  pocl  4426  swopolem  4428  swopo  4429  sowlin  4443  sotricim  4446  sotritrieq  4448  seex  4458  frind  4475  wetriext  4701  vtoclr  4800  posng  4824  brcog  4924  brcogw  4926  opelcnvg  4937  dfdmf  4951  breldmg  4964  dfrnf  5000  dmcoss  5029  resieq  5050  dfres2  5092  elimag  5107  elrelimasn  5130  elimasn  5131  intirr  5151  poirr2  5157  poltletr  5165  dffun6f  5367  dffun4f  5370  fun11  5425  brprcneu  5665  fv3  5695  tz6.12c  5702  relelfvdm  5704  fvmbr  5707  funbrfv  5715  fnbrfvb  5717  funfvdm2f  5744  fndmdif  5785  dff3im  5824  fmptco  5845  foeqcnvco  5965  isorel  5983  isocnv  5986  isotr  5991  isopolem  5997  isosolem  5999  f1oiso  6001  f1oiso2  6002  caovordig  6222  caovordg  6224  caovord  6228  caofrss  6300  caoftrn  6301  poxp  6430  tposoprab  6513  ertr  6784  ecopovsym  6867  ecopovtrn  6868  ecopovsymg  6870  ecopovtrng  6871  th3qlem2  6874  domeng  6991  eqeng  7007  snfig  7058  nneneq  7113  nnfi  7129  ssfilem  7132  ssfilemd  7134  domfiexmid  7137  dif1enen  7139  diffitest  7146  findcard  7147  findcard2  7148  findcard2s  7149  diffisn  7152  tridc  7159  fimax2gtrilemstep  7160  inffiexmid  7168  unsnfi  7181  fiintim  7193  fisseneq  7197  isbth  7239  supmoti  7286  eqsupti  7289  supubti  7292  suplubti  7293  suplub2ti  7294  supmaxti  7297  supsnti  7298  isotilem  7299  isoti  7300  supisolem  7301  supisoex  7302  cardcl  7479  isnumi  7480  cardval3ex  7483  exmidfodomrlemr  7507  exmidfodomrlemrALT  7508  papsym  7563  papcotr  7564  exmidapne  7576  nqtri3or  7713  ltsonq  7715  ltanqg  7717  ltmnqg  7718  ltexnqq  7725  nsmallnqq  7729  subhalfnqq  7731  ltbtwnnqq  7732  prarloclemarch2  7736  nqnq0pi  7755  prcdnql  7801  prcunqu  7802  prnminu  7806  genpcdl  7836  genprndl  7838  genprndu  7839  genpdisj  7840  nqprm  7859  nqprrnd  7860  nqprdisj  7861  nqprloc  7862  nqprlu  7864  nqprl  7868  addnqprlemru  7875  addnqprlemfl  7876  addnqprlemfu  7877  mulnqprlemru  7891  mulnqprlemfl  7892  mulnqprlemfu  7893  1idpru  7908  ltnqpr  7910  ltnqpri  7911  prplnqu  7937  recexprlemelu  7940  recexprlemm  7941  recexprlemloc  7948  recexprlem1ssl  7950  recexprlemss1u  7953  cauappcvgprlemm  7962  cauappcvgprlemopu  7965  cauappcvgprlemupu  7966  cauappcvgprlemdisj  7968  cauappcvgprlemloc  7969  cauappcvgprlemladdfu  7971  cauappcvgprlemladdru  7973  cauappcvgprlemladdrl  7974  cauappcvgprlem2  7977  caucvgprlemnkj  7983  caucvgprlemnbj  7984  caucvgprlemm  7985  caucvgprlemopu  7988  caucvgprlemupu  7989  caucvgprlemdisj  7991  caucvgprlemloc  7992  caucvgprlemcl  7993  caucvgprlemladdfu  7994  caucvgprlemladdrl  7995  caucvgprlem2  7997  caucvgprprlemelu  8003  caucvgprprlemcbv  8004  caucvgprprlemval  8005  caucvgprprlemnbj  8010  caucvgprprlemmu  8012  caucvgprprlemexbt  8023  caucvgprprlemaddq  8025  caucvgprprlem1  8026  caucvgprprlem2  8027  suplocexprlemmu  8035  suplocexprlemru  8036  suplocexprlemdisj  8037  suplocexprlemloc  8038  suplocexprlemub  8040  suplocexpr  8042  lttrsr  8079  ltsosr  8081  ltasrg  8087  recexgt0sr  8090  mulgt0sr  8095  aptisr  8096  mulextsr1  8098  srpospr  8100  caucvgsrlemgt1  8112  caucvgsrlemoffres  8117  caucvgsr  8119  map2psrprg  8122  suplocsrlemb  8123  suplocsrlempr  8124  suplocsrlem  8125  axprecex  8197  axpre-ltwlin  8200  axpre-lttrn  8201  axpre-apti  8202  axpre-ltadd  8203  axpre-mulgt0  8204  axpre-mulext  8205  axcaucvglemcau  8215  axcaucvglemres  8216  axcaucvg  8217  axpre-suploclemres  8218  axpre-suploc  8219  ltxrlt  8341  lttri3  8355  ltne  8360  eqle  8367  ltordlem  8758  reapti  8855  apreim  8879  squeeze0  9180  lbreu  9221  lble  9223  suprleubex  9230  sup3exmid  9233  nnge1  9262  nn2ge  9272  nn1gt1  9273  nnsub  9278  nominpos  9478  nn0ge0  9523  elnnnn0b  9542  nn0ge2m1nn  9562  zdclt  9657  suprzclex  9679  peano2uz2  9688  peano5uzti  9689  dfuzi  9691  uzind  9692  uzind3  9694  eluz1  9860  uzind4  9923  indstr  9928  supinfneg  9930  infsupneg  9931  infregelbex  9933  indstr2  9944  ublbneg  9948  irrmulap  9983  elpq  9984  elpqb  9985  elrp  9991  mnfltxr  10122  nn0pnfge0  10127  xrltnsym  10129  xrlttr  10131  xrltso  10132  xrlttri3  10133  xrltne  10149  ngtmnft  10153  nmnfgt  10154  xrrebnd  10155  z2ge  10162  xltnegi  10171  xltadd1  10212  xsubge0  10217  xleaddadd  10223  ixxval  10232  elixx1  10233  elioo2  10257  iccid  10261  iccsupr  10302  repos  10306  fzval  10347  elfz1  10350  fzm1  10438  zsupcllemstep  10593  suprzubdc  10600  zsupssdc  10602  qdclt  10609  exbtwnzlemstep  10611  exbtwnzlemex  10613  qbtwnre  10620  qbtwnxr  10621  flval  10636  apbtwnz  10638  modqid2  10717  modqmuladdnn0  10734  exp3val  10907  expge0  10941  expge1  10942  nn0ltexp2  11075  facdiv  11104  facwordi  11106  hashinfom  11145  hashennn  11147  hashunlem  11172  zfz1iso  11217  wrdlen1  11266  fstwrdne0  11268  wrdl1exs1  11321  pfxsuffeqwrdeq  11394  pfxsuff1eqwrdeq  11395  ccats1pfxeq  11410  ccats1pfxeqrex  11411  pfxccatin12lem3  11428  ovshftex  11508  shftfibg  11509  shftfib  11512  shftfn  11513  2shfti  11520  sqrt0rlem  11692  resqrexlemex  11714  rsqrmo  11716  resqrtcl  11718  rersqrtthlem  11719  sqrtsq  11733  cau3lem  11803  caubnd2  11806  maxleim  11894  maxabslemval  11897  maxleast  11902  maxleb  11905  fimaxre2  11916  minmax  11919  xrmaxleim  11933  xrmaxiflemval  11939  xrmaxaddlem  11949  xrminmax  11954  xrbdtri  11965  climi  11976  climeu  11985  climmo  11987  2clim  11990  addcn2  11999  mulcn2  12001  reccn2ap  12002  cn1lem  12003  summodc  12073  zsumdc  12074  fsum3  12077  cvgratz  12222  ntrivcvgap0  12239  prodmodc  12268  zproddc  12269  fprodseq  12273  fprodntrivap  12274  sinltxirr  12451  dvdsabsb  12500  0dvds  12501  alzdvds  12544  dvdsext  12545  fzo0dvdseq  12547  2tp1odd  12574  2teven  12577  divalglemnn  12608  divalglemeunn  12611  divalglemeuneg  12613  bitsinv1lem  12651  gcdval  12659  gcddvds  12663  bezoutlemstep  12697  bezoutlemmain  12698  bezoutlemex  12701  bezoutlemeu  12707  bezoutlemsup  12709  dfgcd3  12710  bezout  12711  dvdsgcd  12712  dfgcd2  12714  dvdssq  12731  uzwodc  12737  nnwofdc  12738  lcmval  12764  lcmcllem  12768  dvdslcm  12770  lcmledvds  12771  lcmgcdlem  12778  lcmdvds  12780  coprmgcdb  12789  coprmdvds2  12794  cncongr1  12804  cncongr2  12805  isprm  12810  dvdsnprmd  12826  dvdsprm  12838  exprmfct  12839  isprm6  12848  prmexpb  12852  prmfac1  12853  rpexp  12854  sqrt2irr  12863  oddpwdclemdc  12874  oddpwdc  12875  sqpweven  12876  2sqpwodd  12877  sqne2sq  12878  nnoddn2prmb  12964  pceu  12997  pczpre  12999  pcdiv  13004  pcdvdsb  13022  difsqpwdvds  13040  pcmpt  13045  pcmptdvds  13047  oddprmdvds  13056  prmpwdvds  13057  infpnlem2  13062  ballotfilemfcc  13154  oddennn  13160  evenennn  13161  exmidunben  13194  nninfdclemcl  13216  nninfdclemp1  13218  nninfdc  13221  infpn2  13224  eqgen  13961  zndvds  14814  znleval  14818  comet  15381  metcnpi  15397  metcnpi2  15398  metcnpi3  15399  addcncntoplem  15443  cncfi  15460  elcncf1di  15461  mulcncflem  15489  dedekindeulemuub  15499  dedekindeulemloc  15501  dedekindeulemlu  15503  dedekindeulemeu  15504  dedekindeu  15505  suplociccreex  15506  suplociccex  15507  dedekindicclemuub  15508  dedekindicclemloc  15510  dedekindicclemlu  15512  dedekindicclemeu  15513  dedekindicclemicc  15514  dedekindicc  15515  ivthinclemlopn  15518  ivthinclemlr  15519  ivthinclemuopn  15520  ivthinclemur  15521  ivthinclemloc  15523  ivthinc  15525  ivthreinc  15527  dich0  15534  ivthdich  15535  limcimo  15547  cnplimclemr  15551  limccnp2lem  15558  limccoap  15560  eldvap  15564  logltb  15756  pellexlem3  15864  lgsdir  15925  lgsne0  15928  gausslemma2dlem0i  15947  lgsquadlem1  15967  lgsquadlem2  15968  lgsquadlem3  15969  2lgslem2  15982  2lgs  15994  2sqlem6  16010  2sqlem8  16013  2sqlem10  16015  lfgredg2dom  16144  istrl  16397  clwwlkn0  16420  clwwlkext2edg  16434  clwwlknonccat  16445  clwwlknonex2  16451  iseupth  16459  konigsberg  16505  sbthom  16823  trilpo  16844  trirec0  16845  apdiff  16849  reap0  16860  cndcap  16861  trimul0or  16862  nconstwlpolem  16868  neapmkv  16871  neap0mkv  16872  ltlenmkv  16873