Theorem breq2 4118

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 3889	. . 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 4115	. 2 |- ( C R A <-> <. C , A >. e. R )
4		df-br 4115	. 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 3697   class class class wbr 4114

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 3218  df-sn 3700  df-pr 3701  df-op 3703  df-br 4115

This theorem is referenced by:  breq12  4119  breq2i  4122  breq2d  4126  nbrne1  4133  brralrspcev  4173  brimralrspcev  4174  pocl  4429  swopolem  4431  swopo  4432  sowlin  4446  sotricim  4449  sotritrieq  4451  seex  4461  frind  4478  wetriext  4704  vtoclr  4803  posng  4827  brcog  4927  brcogw  4929  opelcnvg  4940  dfdmf  4954  breldmg  4967  dfrnf  5003  dmcoss  5032  resieq  5053  dfres2  5095  elimag  5110  elrelimasn  5133  elimasn  5134  intirr  5154  poirr2  5160  poltletr  5168  dffun6f  5370  dffun4f  5373  fun11  5428  brprcneu  5668  fv3  5698  tz6.12c  5705  relelfvdm  5707  fvmbr  5710  funbrfv  5718  fnbrfvb  5720  funfvdm2f  5747  fndmdif  5788  dff3im  5827  fmptco  5848  foeqcnvco  5969  isorel  5987  isocnv  5990  isotr  5995  isopolem  6001  isosolem  6003  f1oiso  6005  f1oiso2  6006  caovordig  6228  caovordg  6230  caovord  6234  caofrss  6307  caoftrn  6308  poxp  6441  tposoprab  6524  ertr  6795  ecopovsym  6878  ecopovtrn  6879  ecopovsymg  6881  ecopovtrng  6882  th3qlem2  6885  domeng  7002  eqeng  7018  snfig  7069  nneneq  7124  nnfi  7140  ssfilem  7143  ssfilemd  7145  domfiexmid  7148  dif1enen  7150  diffitest  7157  findcard  7158  findcard2  7159  findcard2s  7160  diffisn  7163  tridc  7170  fimax2gtrilemstep  7171  inffiexmid  7179  unsnfi  7192  fiintim  7204  fisseneq  7208  isbth  7250  supmoti  7297  eqsupti  7300  supubti  7303  suplubti  7304  suplub2ti  7305  supmaxti  7308  supsnti  7309  isotilem  7310  isoti  7311  supisolem  7312  supisoex  7313  cardcl  7490  isnumi  7491  cardval3ex  7494  exmidfodomrlemr  7518  exmidfodomrlemrALT  7519  papsym  7576  papcotr  7577  exmidapne  7590  nqtri3or  7727  ltsonq  7729  ltanqg  7731  ltmnqg  7732  ltexnqq  7739  nsmallnqq  7743  subhalfnqq  7745  ltbtwnnqq  7746  prarloclemarch2  7750  nqnq0pi  7769  prcdnql  7815  prcunqu  7816  prnminu  7820  genpcdl  7850  genprndl  7852  genprndu  7853  genpdisj  7854  nqprm  7873  nqprrnd  7874  nqprdisj  7875  nqprloc  7876  nqprlu  7878  nqprl  7882  addnqprlemru  7889  addnqprlemfl  7890  addnqprlemfu  7891  mulnqprlemru  7905  mulnqprlemfl  7906  mulnqprlemfu  7907  1idpru  7922  ltnqpr  7924  ltnqpri  7925  prplnqu  7951  recexprlemelu  7954  recexprlemm  7955  recexprlemloc  7962  recexprlem1ssl  7964  recexprlemss1u  7967  cauappcvgprlemm  7976  cauappcvgprlemopu  7979  cauappcvgprlemupu  7980  cauappcvgprlemdisj  7982  cauappcvgprlemloc  7983  cauappcvgprlemladdfu  7985  cauappcvgprlemladdru  7987  cauappcvgprlemladdrl  7988  cauappcvgprlem2  7991  caucvgprlemnkj  7997  caucvgprlemnbj  7998  caucvgprlemm  7999  caucvgprlemopu  8002  caucvgprlemupu  8003  caucvgprlemdisj  8005  caucvgprlemloc  8006  caucvgprlemcl  8007  caucvgprlemladdfu  8008  caucvgprlemladdrl  8009  caucvgprlem2  8011  caucvgprprlemelu  8017  caucvgprprlemcbv  8018  caucvgprprlemval  8019  caucvgprprlemnbj  8024  caucvgprprlemmu  8026  caucvgprprlemexbt  8037  caucvgprprlemaddq  8039  caucvgprprlem1  8040  caucvgprprlem2  8041  suplocexprlemmu  8049  suplocexprlemru  8050  suplocexprlemdisj  8051  suplocexprlemloc  8052  suplocexprlemub  8054  suplocexpr  8056  lttrsr  8093  ltsosr  8095  ltasrg  8101  recexgt0sr  8104  mulgt0sr  8109  aptisr  8110  mulextsr1  8112  srpospr  8114  caucvgsrlemgt1  8126  caucvgsrlemoffres  8131  caucvgsr  8133  map2psrprg  8136  suplocsrlemb  8137  suplocsrlempr  8138  suplocsrlem  8139  axprecex  8211  axpre-ltwlin  8214  axpre-lttrn  8215  axpre-apti  8216  axpre-ltadd  8217  axpre-mulgt0  8218  axpre-mulext  8219  axcaucvglemcau  8229  axcaucvglemres  8230  axcaucvg  8231  axpre-suploclemres  8232  axpre-suploc  8233  ltxrlt  8355  lttri3  8369  ltne  8374  eqle  8381  ltordlem  8774  reapti  8871  apreim  8895  squeeze0  9198  lbreu  9239  lble  9241  suprleubex  9248  sup3exmid  9251  nnge1  9280  nn2ge  9290  nn1gt1  9291  nnsub  9296  nominpos  9496  nn0ge0  9541  elnnnn0b  9560  nn0ge2m1nn  9580  zdclt  9675  suprzclex  9697  peano2uz2  9706  peano5uzti  9707  dfuzi  9709  uzind  9710  uzind3  9712  eluz1  9878  uzind4  9941  indstr  9946  supinfneg  9948  infsupneg  9949  infregelbex  9951  indstr2  9962  ublbneg  9966  irrmulap  10001  elpq  10002  elpqb  10003  elrp  10009  mnfltxr  10141  nn0pnfge0  10146  xrltnsym  10148  xrlttr  10150  xrltso  10151  xrlttri3  10152  xrltne  10168  ngtmnft  10172  nmnfgt  10173  xrrebnd  10174  z2ge  10181  xltnegi  10190  xltadd1  10231  xsubge0  10236  xleaddadd  10242  ixxval  10251  elixx1  10252  elioo2  10276  iccid  10280  iccsupr  10321  repos  10325  fzval  10366  elfz1  10369  fzm1  10459  zsupcllemstep  10614  suprzubdc  10623  zsupssdc  10625  qdclt  10632  exbtwnzlemstep  10634  exbtwnzlemex  10636  qbtwnre  10643  qbtwnxr  10644  flval  10659  apbtwnz  10661  modqid2  10740  modqmuladdnn0  10757  exp3val  10930  expge0  10964  expge1  10965  nn0ltexp2  11099  facdiv  11128  facwordi  11130  hashinfom  11169  hashennn  11171  hashunlem  11196  zfz1iso  11241  wrdlen1  11290  fstwrdne0  11292  wrdl1exs1  11345  pfxsuffeqwrdeq  11418  pfxsuff1eqwrdeq  11419  ccats1pfxeq  11434  ccats1pfxeqrex  11435  pfxccatin12lem3  11452  ovshftex  11532  shftfibg  11533  shftfib  11536  shftfn  11537  2shfti  11544  sqrt0rlem  11717  resqrexlemex  11739  rsqrmo  11741  resqrtcl  11743  rersqrtthlem  11744  sqrtsq  11758  cau3lem  11828  caubnd2  11831  maxleim  11919  maxabslemval  11922  maxleast  11927  maxleb  11930  fimaxre2  11941  minmax  11944  xrmaxleim  11958  xrmaxiflemval  11964  xrmaxaddlem  11974  xrminmax  11979  xrbdtri  11990  climi  12001  climeu  12010  climmo  12012  2clim  12015  addcn2  12024  mulcn2  12026  reccn2ap  12027  cn1lem  12028  summodc  12098  zsumdc  12099  fsum3  12102  cvgratz  12247  ntrivcvgap0  12264  prodmodc  12293  zproddc  12294  fprodseq  12298  fprodntrivap  12299  sinltxirr  12476  dvdsabsb  12525  0dvds  12526  alzdvds  12569  dvdsext  12570  fzo0dvdseq  12572  2tp1odd  12599  2teven  12602  divalglemnn  12633  divalglemeunn  12636  divalglemeuneg  12638  bitsinv1lem  12676  gcdval  12684  gcddvds  12688  bezoutlemstep  12722  bezoutlemmain  12723  bezoutlemex  12726  bezoutlemeu  12732  bezoutlemsup  12734  dfgcd3  12735  bezout  12736  dvdsgcd  12737  dfgcd2  12739  dvdssq  12756  uzwodc  12762  nnwofdc  12763  lcmval  12789  lcmcllem  12793  dvdslcm  12795  lcmledvds  12796  lcmgcdlem  12803  lcmdvds  12805  coprmgcdb  12814  coprmdvds2  12819  cncongr1  12829  cncongr2  12830  isprm  12835  dvdsnprmd  12851  dvdsprm  12863  exprmfct  12864  isprm6  12873  prmexpb  12877  prmfac1  12878  rpexp  12879  sqrt2irr  12888  oddpwdclemdc  12899  oddpwdc  12900  sqpweven  12901  2sqpwodd  12902  sqne2sq  12903  nnoddn2prmb  12989  pceu  13022  pczpre  13024  pcdiv  13029  pcdvdsb  13047  difsqpwdvds  13065  pcmpt  13070  pcmptdvds  13072  oddprmdvds  13081  prmpwdvds  13082  infpnlem2  13087  ballotfilemfcc  13181  oddennn  13231  evenennn  13232  exmidunben  13265  nninfdclemcl  13287  nninfdclemp1  13289  nninfdc  13292  infpn2  13295  eqgen  13984  zndvds  14927  znleval  14931  comet  15494  metcnpi  15510  metcnpi2  15511  metcnpi3  15512  addcncntoplem  15556  cncfi  15573  elcncf1di  15574  mulcncflem  15602  dedekindeulemuub  15612  dedekindeulemloc  15614  dedekindeulemlu  15616  dedekindeulemeu  15617  dedekindeu  15618  suplociccreex  15619  suplociccex  15620  dedekindicclemuub  15621  dedekindicclemloc  15623  dedekindicclemlu  15625  dedekindicclemeu  15626  dedekindicclemicc  15627  dedekindicc  15628  ivthinclemlopn  15631  ivthinclemlr  15632  ivthinclemuopn  15633  ivthinclemur  15634  ivthinclemloc  15636  ivthinc  15638  ivthreinc  15640  dich0  15647  ivthdich  15648  limcimo  15660  cnplimclemr  15664  limccnp2lem  15671  limccoap  15673  eldvap  15677  logltb  15869  pellexlem3  15977  lgsdir  16038  lgsne0  16041  gausslemma2dlem0i  16060  lgsquadlem1  16080  lgsquadlem2  16081  lgsquadlem3  16082  2lgslem2  16095  2lgs  16107  2sqlem6  16123  2sqlem8  16126  2sqlem10  16128  lfgredg2dom  16257  istrl  16510  clwwlkn0  16533  clwwlkext2edg  16547  clwwlknonccat  16558  clwwlknonex2  16564  iseupth  16572  konigsberg  16618  lealltlt2  16636  sbthom  16946  trilpo  16967  trirec0  16968  apdiff  16972  reap0  16983  cndcap  16984  nconstwlpolem  16990  neapmkv  16993  neap0mkv  16994  ltlenmkv  16995