ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  breq2 Unicode version

Theorem breq2 3796
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
StepHypRef Expression
1 opeq2 3578 . . 3  |-  ( A  =  B  ->  <. C ,  A >.  =  <. C ,  B >. )
21eleq1d 2122 . 2  |-  ( A  =  B  ->  ( <. C ,  A >.  e.  R  <->  <. C ,  B >.  e.  R ) )
3 df-br 3793 . 2  |-  ( C R A  <->  <. C ,  A >.  e.  R )
4 df-br 3793 . 2  |-  ( C R B  <->  <. C ,  B >.  e.  R )
52, 3, 43bitr4g 216 1  |-  ( A  =  B  ->  ( C R A  <->  C R B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 102    = wceq 1259    e. wcel 1409   <.cop 3406   class class class wbr 3792
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-io 640  ax-5 1352  ax-7 1353  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-8 1411  ax-10 1412  ax-11 1413  ax-i12 1414  ax-bndl 1415  ax-4 1416  ax-17 1435  ax-i9 1439  ax-ial 1443  ax-i5r 1444  ax-ext 2038
This theorem depends on definitions:  df-bi 114  df-3an 898  df-tru 1262  df-nf 1366  df-sb 1662  df-clab 2043  df-cleq 2049  df-clel 2052  df-nfc 2183  df-v 2576  df-un 2950  df-sn 3409  df-pr 3410  df-op 3412  df-br 3793
This theorem is referenced by:  breq12  3797  breq2i  3800  breq2d  3804  nbrne1  3809  pocl  4068  swopolem  4070  swopo  4071  sowlin  4085  sotricim  4088  sotritrieq  4090  seex  4100  frind  4117  wetriext  4329  vtoclr  4416  posng  4440  brcog  4530  brcogw  4532  opelcnvg  4543  dfdmf  4556  breldmg  4569  dfrnf  4603  dmcoss  4629  resieq  4650  dfres2  4686  elimag  4700  elreimasng  4719  elimasn  4720  intirr  4739  poirr2  4745  poltletr  4753  dffun6f  4943  dffun4f  4946  fun11  4994  brprcneu  5199  fv3  5225  tz6.12c  5231  relelfvdm  5233  funbrfv  5240  fnbrfvb  5242  funfvdm2f  5266  fndmdif  5300  dff3im  5340  fmptco  5358  foeqcnvco  5458  isorel  5476  isocnv  5479  isotr  5484  isopolem  5489  isosolem  5491  f1oiso  5493  f1oiso2  5494  caovordig  5694  caovordg  5696  caovord  5700  caofrss  5763  caoftrn  5764  poxp  5881  tposoprab  5926  ertr  6152  ecopovsym  6233  ecopovtrn  6234  ecopovsymg  6236  ecopovtrng  6237  th3qlem2  6240  domeng  6264  eqeng  6277  snfig  6322  nneneq  6351  nnfi  6364  ssfiexmid  6367  diffitest  6375  findcard  6376  findcard2  6377  findcard2s  6378  diffisn  6381  supmoti  6399  eqsupti  6402  supubti  6405  suplubti  6406  supmaxti  6408  supsnti  6409  isotilem  6410  isoti  6411  supisolem  6412  supisoex  6413  cardcl  6419  isnumi  6420  cardval3ex  6423  nqtri3or  6552  ltsonq  6554  ltanqg  6556  ltmnqg  6557  ltexnqq  6564  nsmallnqq  6568  subhalfnqq  6570  ltbtwnnqq  6571  prarloclemarch2  6575  nqnq0pi  6594  prcdnql  6640  prcunqu  6641  prnminu  6645  genpcdl  6675  genprndl  6677  genprndu  6678  genpdisj  6679  nqprm  6698  nqprrnd  6699  nqprdisj  6700  nqprloc  6701  nqprlu  6703  nqprl  6707  addnqprlemru  6714  addnqprlemfl  6715  addnqprlemfu  6716  mulnqprlemru  6730  mulnqprlemfl  6731  mulnqprlemfu  6732  1idpru  6747  ltnqpr  6749  ltnqpri  6750  prplnqu  6776  recexprlemelu  6779  recexprlemm  6780  recexprlemloc  6787  recexprlem1ssl  6789  recexprlemss1u  6792  cauappcvgprlemm  6801  cauappcvgprlemopu  6804  cauappcvgprlemupu  6805  cauappcvgprlemdisj  6807  cauappcvgprlemloc  6808  cauappcvgprlemladdfu  6810  cauappcvgprlemladdru  6812  cauappcvgprlemladdrl  6813  cauappcvgprlem2  6816  caucvgprlemnkj  6822  caucvgprlemnbj  6823  caucvgprlemm  6824  caucvgprlemopu  6827  caucvgprlemupu  6828  caucvgprlemdisj  6830  caucvgprlemloc  6831  caucvgprlemcl  6832  caucvgprlemladdfu  6833  caucvgprlemladdrl  6834  caucvgprlem2  6836  caucvgprprlemelu  6842  caucvgprprlemcbv  6843  caucvgprprlemval  6844  caucvgprprlemnbj  6849  caucvgprprlemmu  6851  caucvgprprlemexbt  6862  caucvgprprlemaddq  6864  caucvgprprlem1  6865  caucvgprprlem2  6866  lttrsr  6905  ltsosr  6907  ltasrg  6913  recexgt0sr  6916  mulgt0sr  6920  aptisr  6921  mulextsr1  6923  srpospr  6925  caucvgsrlemgt1  6937  caucvgsrlemoffres  6942  caucvgsr  6944  axprecex  7012  axpre-ltwlin  7015  axpre-lttrn  7016  axpre-apti  7017  axpre-ltadd  7018  axpre-mulgt0  7019  axpre-mulext  7020  axcaucvglemcau  7030  axcaucvglemres  7031  axcaucvg  7032  ltxrlt  7144  lttri3  7157  ltne  7162  eqle  7168  reapti  7644  apreim  7668  squeeze0  7945  nnge1  8013  nn2ge  8022  nn1gt1  8023  nnsub  8028  nominpos  8219  nn0ge0  8264  elnnnn0b  8283  nn0ge2m1nn  8299  zdclt  8376  peano2uz2  8404  peano5uzti  8405  dfuzi  8407  uzind  8408  uzind3  8410  eluz1  8573  uzind4  8627  indstr  8632  indstr2  8643  ublbneg  8645  elrp  8683  mnfltxr  8808  nn0pnfge0  8813  xrltnsym  8815  xrlttr  8817  xrltso  8818  xrlttri3  8819  xrltne  8830  ngtmnft  8832  xrrebnd  8833  z2ge  8840  xltnegi  8849  ixxval  8866  elixx1  8867  elioo2  8891  iccid  8895  iccsupr  8936  repos  8940  fzval  8978  elfz1  8981  fzm1  9064  qbtwnre  9213  qbtwnxr  9214  flval  9224  modqid2  9301  modqmuladdnn0  9318  serige0  9417  expival  9422  expge0  9456  expge1  9457  facdiv  9606  facwordi  9608  ovshftex  9648  shftfibg  9649  shftfib  9652  shftfn  9653  2shfti  9660  sqrt0rlem  9830  resqrexlemex  9852  rsqrmo  9854  resqrtcl  9856  rersqrtthlem  9857  sqrtsq  9871  cau3lem  9941  caubnd2  9944  climi  10039  climeu  10048  climmo  10050  2clim  10053  addcn2  10062  mulcn2  10064  cn1lem  10065  dvdsabsb  10127  0dvds  10128  alzdvds  10166  dvdsext  10167  fzo0dvdseq  10169  2tp1odd  10196  2teven  10199  divalglemnn  10230  divalglemeunn  10233  divalglemeuneg  10235  sqrt2irr  10251  oddpwdclemdc  10261  oddpwdc  10262
  Copyright terms: Public domain W3C validator