Theorem breq2 3941

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 3714	. . 3 |- ( A = B -> <. C , A >. = <. C , B >. )
2	1	eleq1d 2209	. 2 |- ( A = B -> ( <. C , A >. e. R <-> <. C , B >. e. R ) )
3		df-br 3938	. 2 |- ( C R A <-> <. C , A >. e. R )
4		df-br 3938	. 2 |- ( C R B <-> <. C , B >. e. R )
5	2, 3, 4	3bitr4g 222	1 |- ( A = B -> ( C R A <-> C R B ) )

Syntax hints:   -> wi 4   <-> wb 104   = wceq 1332   e. wcel 1481   <.cop 3535   class class class wbr 3937

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122

This theorem depends on definitions:  df-bi 116  df-3an 965  df-tru 1335  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-v 2691  df-un 3080  df-sn 3538  df-pr 3539  df-op 3541  df-br 3938

This theorem is referenced by:  breq12  3942  breq2i  3945  breq2d  3949  nbrne1  3955  brralrspcev  3994  brimralrspcev  3995  pocl  4233  swopolem  4235  swopo  4236  sowlin  4250  sotricim  4253  sotritrieq  4255  seex  4265  frind  4282  wetriext  4499  vtoclr  4595  posng  4619  brcog  4714  brcogw  4716  opelcnvg  4727  dfdmf  4740  breldmg  4753  dfrnf  4788  dmcoss  4816  resieq  4837  dfres2  4879  elimag  4893  elreimasng  4913  elimasn  4914  intirr  4933  poirr2  4939  poltletr  4947  dffun6f  5144  dffun4f  5147  fun11  5198  brprcneu  5422  fv3  5452  tz6.12c  5459  relelfvdm  5461  funbrfv  5468  fnbrfvb  5470  funfvdm2f  5494  fndmdif  5533  dff3im  5573  fmptco  5594  foeqcnvco  5699  isorel  5717  isocnv  5720  isotr  5725  isopolem  5731  isosolem  5733  f1oiso  5735  f1oiso2  5736  caovordig  5944  caovordg  5946  caovord  5950  caofrss  6014  caoftrn  6015  poxp  6137  tposoprab  6185  ertr  6452  ecopovsym  6533  ecopovtrn  6534  ecopovsymg  6536  ecopovtrng  6537  th3qlem2  6540  domeng  6654  eqeng  6668  snfig  6716  nneneq  6759  nnfi  6774  ssfilem  6777  domfiexmid  6780  dif1enen  6782  diffitest  6789  findcard  6790  findcard2  6791  findcard2s  6792  diffisn  6795  tridc  6801  fimax2gtrilemstep  6802  inffiexmid  6808  unsnfi  6815  fiintim  6825  fisseneq  6828  isbth  6863  supmoti  6888  eqsupti  6891  supubti  6894  suplubti  6895  suplub2ti  6896  supmaxti  6899  supsnti  6900  isotilem  6901  isoti  6902  supisolem  6903  supisoex  6904  cardcl  7054  isnumi  7055  cardval3ex  7058  exmidfodomrlemr  7075  exmidfodomrlemrALT  7076  nqtri3or  7228  ltsonq  7230  ltanqg  7232  ltmnqg  7233  ltexnqq  7240  nsmallnqq  7244  subhalfnqq  7246  ltbtwnnqq  7247  prarloclemarch2  7251  nqnq0pi  7270  prcdnql  7316  prcunqu  7317  prnminu  7321  genpcdl  7351  genprndl  7353  genprndu  7354  genpdisj  7355  nqprm  7374  nqprrnd  7375  nqprdisj  7376  nqprloc  7377  nqprlu  7379  nqprl  7383  addnqprlemru  7390  addnqprlemfl  7391  addnqprlemfu  7392  mulnqprlemru  7406  mulnqprlemfl  7407  mulnqprlemfu  7408  1idpru  7423  ltnqpr  7425  ltnqpri  7426  prplnqu  7452  recexprlemelu  7455  recexprlemm  7456  recexprlemloc  7463  recexprlem1ssl  7465  recexprlemss1u  7468  cauappcvgprlemm  7477  cauappcvgprlemopu  7480  cauappcvgprlemupu  7481  cauappcvgprlemdisj  7483  cauappcvgprlemloc  7484  cauappcvgprlemladdfu  7486  cauappcvgprlemladdru  7488  cauappcvgprlemladdrl  7489  cauappcvgprlem2  7492  caucvgprlemnkj  7498  caucvgprlemnbj  7499  caucvgprlemm  7500  caucvgprlemopu  7503  caucvgprlemupu  7504  caucvgprlemdisj  7506  caucvgprlemloc  7507  caucvgprlemcl  7508  caucvgprlemladdfu  7509  caucvgprlemladdrl  7510  caucvgprlem2  7512  caucvgprprlemelu  7518  caucvgprprlemcbv  7519  caucvgprprlemval  7520  caucvgprprlemnbj  7525  caucvgprprlemmu  7527  caucvgprprlemexbt  7538  caucvgprprlemaddq  7540  caucvgprprlem1  7541  caucvgprprlem2  7542  suplocexprlemmu  7550  suplocexprlemru  7551  suplocexprlemdisj  7552  suplocexprlemloc  7553  suplocexprlemub  7555  suplocexpr  7557  lttrsr  7594  ltsosr  7596  ltasrg  7602  recexgt0sr  7605  mulgt0sr  7610  aptisr  7611  mulextsr1  7613  srpospr  7615  caucvgsrlemgt1  7627  caucvgsrlemoffres  7632  caucvgsr  7634  map2psrprg  7637  suplocsrlemb  7638  suplocsrlempr  7639  suplocsrlem  7640  axprecex  7712  axpre-ltwlin  7715  axpre-lttrn  7716  axpre-apti  7717  axpre-ltadd  7718  axpre-mulgt0  7719  axpre-mulext  7720  axcaucvglemcau  7730  axcaucvglemres  7731  axcaucvg  7732  axpre-suploclemres  7733  axpre-suploc  7734  ltxrlt  7854  lttri3  7868  ltne  7873  eqle  7879  ltordlem  8268  reapti  8365  apreim  8389  squeeze0  8686  lbreu  8727  lble  8729  suprleubex  8736  sup3exmid  8739  nnge1  8767  nn2ge  8777  nn1gt1  8778  nnsub  8783  nominpos  8981  nn0ge0  9026  elnnnn0b  9045  nn0ge2m1nn  9061  zdclt  9152  suprzclex  9173  peano2uz2  9182  peano5uzti  9183  dfuzi  9185  uzind  9186  uzind3  9188  eluz1  9354  uzind4  9410  indstr  9415  supinfneg  9417  infsupneg  9418  indstr2  9430  ublbneg  9432  elpq  9467  elpqb  9468  elrp  9472  mnfltxr  9602  nn0pnfge0  9607  xrltnsym  9609  xrlttr  9611  xrltso  9612  xrlttri3  9613  xrltne  9626  ngtmnft  9630  nmnfgt  9631  xrrebnd  9632  z2ge  9639  xltnegi  9648  xltadd1  9689  xsubge0  9694  xleaddadd  9700  ixxval  9709  elixx1  9710  elioo2  9734  iccid  9738  iccsupr  9779  repos  9783  fzval  9823  elfz1  9826  fzm1  9911  exbtwnzlemstep  10056  exbtwnzlemex  10058  qbtwnre  10065  qbtwnxr  10066  flval  10076  apbtwnz  10078  modqid2  10155  modqmuladdnn0  10172  exp3val  10326  expge0  10360  expge1  10361  facdiv  10516  facwordi  10518  hashinfom  10556  hashennn  10558  hashunlem  10582  zfz1iso  10616  ovshftex  10623  shftfibg  10624  shftfib  10627  shftfn  10628  2shfti  10635  sqrt0rlem  10807  resqrexlemex  10829  rsqrmo  10831  resqrtcl  10833  rersqrtthlem  10834  sqrtsq  10848  cau3lem  10918  caubnd2  10921  maxleim  11009  maxabslemval  11012  maxleast  11017  maxleb  11020  fimaxre2  11030  minmax  11033  xrmaxleim  11045  xrmaxiflemval  11051  xrmaxaddlem  11061  xrminmax  11066  xrbdtri  11077  climi  11088  climeu  11097  climmo  11099  2clim  11102  addcn2  11111  mulcn2  11113  reccn2ap  11114  cn1lem  11115  summodc  11184  zsumdc  11185  fsum3  11188  cvgratz  11333  ntrivcvgap0  11350  prodmodc  11379  zproddc  11380  fprodseq  11384  dvdsabsb  11548  0dvds  11549  alzdvds  11588  dvdsext  11589  fzo0dvdseq  11591  2tp1odd  11617  2teven  11620  divalglemnn  11651  divalglemeunn  11654  divalglemeuneg  11656  zsupcllemstep  11674  gcdval  11684  gcddvds  11688  bezoutlemstep  11721  bezoutlemmain  11722  bezoutlemex  11725  bezoutlemeu  11731  bezoutlemsup  11733  dfgcd3  11734  bezout  11735  dvdsgcd  11736  dfgcd2  11738  dvdssq  11755  lcmval  11780  lcmcllem  11784  dvdslcm  11786  lcmledvds  11787  lcmgcdlem  11794  lcmdvds  11796  coprmgcdb  11805  coprmdvds2  11810  cncongr1  11820  cncongr2  11821  isprm  11826  dvdsnprmd  11842  dvdsprm  11853  exprmfct  11854  isprm6  11861  prmexpb  11865  prmfac1  11866  rpexp  11867  sqrt2irr  11876  oddpwdclemdc  11887  oddpwdc  11888  sqpweven  11889  2sqpwodd  11890  sqne2sq  11891  oddennn  11941  evenennn  11942  exmidunben  11975  comet  12707  metcnpi  12723  metcnpi2  12724  metcnpi3  12725  addcncntoplem  12759  cncfi  12773  elcncf1di  12774  mulcncflem  12798  dedekindeulemuub  12803  dedekindeulemloc  12805  dedekindeulemlu  12807  dedekindeulemeu  12808  dedekindeu  12809  suplociccreex  12810  suplociccex  12811  dedekindicclemuub  12812  dedekindicclemloc  12814  dedekindicclemlu  12816  dedekindicclemeu  12817  dedekindicclemicc  12818  dedekindicc  12819  ivthinclemlopn  12822  ivthinclemlr  12823  ivthinclemuopn  12824  ivthinclemur  12825  ivthinclemloc  12827  ivthinc  12829  limcimo  12842  cnplimclemr  12846  limccnp2lem  12853  limccoap  12855  eldvap  12859  logltb  13003  sbthom  13396  trilpo  13411  trirec0  13412  apdiff  13416  neapmkv  13425