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

Theorem breq2 3933
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 3706 . . 3  |-  ( A  =  B  ->  <. C ,  A >.  =  <. C ,  B >. )
21eleq1d 2208 . 2  |-  ( A  =  B  ->  ( <. C ,  A >.  e.  R  <->  <. C ,  B >.  e.  R ) )
3 df-br 3930 . 2  |-  ( C R A  <->  <. C ,  A >.  e.  R )
4 df-br 3930 . 2  |-  ( C R B  <->  <. C ,  B >.  e.  R )
52, 3, 43bitr4g 222 1  |-  ( A  =  B  ->  ( C R A  <->  C R B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 104    = wceq 1331    e. wcel 1480   <.cop 3530   class class class wbr 3929
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 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121
This theorem depends on definitions:  df-bi 116  df-3an 964  df-tru 1334  df-nf 1437  df-sb 1736  df-clab 2126  df-cleq 2132  df-clel 2135  df-nfc 2270  df-v 2688  df-un 3075  df-sn 3533  df-pr 3534  df-op 3536  df-br 3930
This theorem is referenced by:  breq12  3934  breq2i  3937  breq2d  3941  nbrne1  3947  brralrspcev  3986  brimralrspcev  3987  pocl  4225  swopolem  4227  swopo  4228  sowlin  4242  sotricim  4245  sotritrieq  4247  seex  4257  frind  4274  wetriext  4491  vtoclr  4587  posng  4611  brcog  4706  brcogw  4708  opelcnvg  4719  dfdmf  4732  breldmg  4745  dfrnf  4780  dmcoss  4808  resieq  4829  dfres2  4871  elimag  4885  elreimasng  4905  elimasn  4906  intirr  4925  poirr2  4931  poltletr  4939  dffun6f  5136  dffun4f  5139  fun11  5190  brprcneu  5414  fv3  5444  tz6.12c  5451  relelfvdm  5453  funbrfv  5460  fnbrfvb  5462  funfvdm2f  5486  fndmdif  5525  dff3im  5565  fmptco  5586  foeqcnvco  5691  isorel  5709  isocnv  5712  isotr  5717  isopolem  5723  isosolem  5725  f1oiso  5727  f1oiso2  5728  caovordig  5936  caovordg  5938  caovord  5942  caofrss  6006  caoftrn  6007  poxp  6129  tposoprab  6177  ertr  6444  ecopovsym  6525  ecopovtrn  6526  ecopovsymg  6528  ecopovtrng  6529  th3qlem2  6532  domeng  6646  eqeng  6660  snfig  6708  nneneq  6751  nnfi  6766  ssfilem  6769  domfiexmid  6772  dif1enen  6774  diffitest  6781  findcard  6782  findcard2  6783  findcard2s  6784  diffisn  6787  tridc  6793  fimax2gtrilemstep  6794  inffiexmid  6800  unsnfi  6807  fiintim  6817  fisseneq  6820  isbth  6855  supmoti  6880  eqsupti  6883  supubti  6886  suplubti  6887  suplub2ti  6888  supmaxti  6891  supsnti  6892  isotilem  6893  isoti  6894  supisolem  6895  supisoex  6896  cardcl  7037  isnumi  7038  cardval3ex  7041  exmidfodomrlemr  7058  exmidfodomrlemrALT  7059  nqtri3or  7211  ltsonq  7213  ltanqg  7215  ltmnqg  7216  ltexnqq  7223  nsmallnqq  7227  subhalfnqq  7229  ltbtwnnqq  7230  prarloclemarch2  7234  nqnq0pi  7253  prcdnql  7299  prcunqu  7300  prnminu  7304  genpcdl  7334  genprndl  7336  genprndu  7337  genpdisj  7338  nqprm  7357  nqprrnd  7358  nqprdisj  7359  nqprloc  7360  nqprlu  7362  nqprl  7366  addnqprlemru  7373  addnqprlemfl  7374  addnqprlemfu  7375  mulnqprlemru  7389  mulnqprlemfl  7390  mulnqprlemfu  7391  1idpru  7406  ltnqpr  7408  ltnqpri  7409  prplnqu  7435  recexprlemelu  7438  recexprlemm  7439  recexprlemloc  7446  recexprlem1ssl  7448  recexprlemss1u  7451  cauappcvgprlemm  7460  cauappcvgprlemopu  7463  cauappcvgprlemupu  7464  cauappcvgprlemdisj  7466  cauappcvgprlemloc  7467  cauappcvgprlemladdfu  7469  cauappcvgprlemladdru  7471  cauappcvgprlemladdrl  7472  cauappcvgprlem2  7475  caucvgprlemnkj  7481  caucvgprlemnbj  7482  caucvgprlemm  7483  caucvgprlemopu  7486  caucvgprlemupu  7487  caucvgprlemdisj  7489  caucvgprlemloc  7490  caucvgprlemcl  7491  caucvgprlemladdfu  7492  caucvgprlemladdrl  7493  caucvgprlem2  7495  caucvgprprlemelu  7501  caucvgprprlemcbv  7502  caucvgprprlemval  7503  caucvgprprlemnbj  7508  caucvgprprlemmu  7510  caucvgprprlemexbt  7521  caucvgprprlemaddq  7523  caucvgprprlem1  7524  caucvgprprlem2  7525  suplocexprlemmu  7533  suplocexprlemru  7534  suplocexprlemdisj  7535  suplocexprlemloc  7536  suplocexprlemub  7538  suplocexpr  7540  lttrsr  7577  ltsosr  7579  ltasrg  7585  recexgt0sr  7588  mulgt0sr  7593  aptisr  7594  mulextsr1  7596  srpospr  7598  caucvgsrlemgt1  7610  caucvgsrlemoffres  7615  caucvgsr  7617  map2psrprg  7620  suplocsrlemb  7621  suplocsrlempr  7622  suplocsrlem  7623  axprecex  7695  axpre-ltwlin  7698  axpre-lttrn  7699  axpre-apti  7700  axpre-ltadd  7701  axpre-mulgt0  7702  axpre-mulext  7703  axcaucvglemcau  7713  axcaucvglemres  7714  axcaucvg  7715  axpre-suploclemres  7716  axpre-suploc  7717  ltxrlt  7837  lttri3  7851  ltne  7856  eqle  7862  ltordlem  8251  reapti  8348  apreim  8372  squeeze0  8669  lbreu  8710  lble  8712  suprleubex  8719  sup3exmid  8722  nnge1  8750  nn2ge  8760  nn1gt1  8761  nnsub  8766  nominpos  8964  nn0ge0  9009  elnnnn0b  9028  nn0ge2m1nn  9044  zdclt  9135  suprzclex  9156  peano2uz2  9165  peano5uzti  9166  dfuzi  9168  uzind  9169  uzind3  9171  eluz1  9337  uzind4  9390  indstr  9395  supinfneg  9397  infsupneg  9398  indstr2  9410  ublbneg  9412  elrp  9450  mnfltxr  9579  nn0pnfge0  9584  xrltnsym  9586  xrlttr  9588  xrltso  9589  xrlttri3  9590  xrltne  9603  ngtmnft  9607  nmnfgt  9608  xrrebnd  9609  z2ge  9616  xltnegi  9625  xltadd1  9666  xsubge0  9671  xleaddadd  9677  ixxval  9686  elixx1  9687  elioo2  9711  iccid  9715  iccsupr  9756  repos  9760  fzval  9799  elfz1  9802  fzm1  9887  exbtwnzlemstep  10032  exbtwnzlemex  10034  qbtwnre  10041  qbtwnxr  10042  flval  10052  apbtwnz  10054  modqid2  10131  modqmuladdnn0  10148  exp3val  10302  expge0  10336  expge1  10337  facdiv  10491  facwordi  10493  hashinfom  10531  hashennn  10533  hashunlem  10557  zfz1iso  10591  ovshftex  10598  shftfibg  10599  shftfib  10602  shftfn  10603  2shfti  10610  sqrt0rlem  10782  resqrexlemex  10804  rsqrmo  10806  resqrtcl  10808  rersqrtthlem  10809  sqrtsq  10823  cau3lem  10893  caubnd2  10896  maxleim  10984  maxabslemval  10987  maxleast  10992  maxleb  10995  fimaxre2  11005  minmax  11008  xrmaxleim  11020  xrmaxiflemval  11026  xrmaxaddlem  11036  xrminmax  11041  xrbdtri  11052  climi  11063  climeu  11072  climmo  11074  2clim  11077  addcn2  11086  mulcn2  11088  reccn2ap  11089  cn1lem  11090  summodc  11159  zsumdc  11160  fsum3  11163  cvgratz  11308  ntrivcvgap0  11325  prodmodc  11354  dvdsabsb  11518  0dvds  11519  alzdvds  11558  dvdsext  11559  fzo0dvdseq  11561  2tp1odd  11587  2teven  11590  divalglemnn  11621  divalglemeunn  11624  divalglemeuneg  11626  zsupcllemstep  11644  gcdval  11654  gcddvds  11658  bezoutlemstep  11691  bezoutlemmain  11692  bezoutlemex  11695  bezoutlemeu  11701  bezoutlemsup  11703  dfgcd3  11704  bezout  11705  dvdsgcd  11706  dfgcd2  11708  dvdssq  11725  lcmval  11750  lcmcllem  11754  dvdslcm  11756  lcmledvds  11757  lcmgcdlem  11764  lcmdvds  11766  coprmgcdb  11775  coprmdvds2  11780  cncongr1  11790  cncongr2  11791  isprm  11796  dvdsnprmd  11812  dvdsprm  11823  exprmfct  11824  isprm6  11831  prmexpb  11835  prmfac1  11836  rpexp  11837  sqrt2irr  11846  oddpwdclemdc  11857  oddpwdc  11858  sqpweven  11859  2sqpwodd  11860  sqne2sq  11861  oddennn  11911  evenennn  11912  exmidunben  11945  comet  12677  metcnpi  12693  metcnpi2  12694  metcnpi3  12695  addcncntoplem  12729  cncfi  12743  elcncf1di  12744  mulcncflem  12768  dedekindeulemuub  12773  dedekindeulemloc  12775  dedekindeulemlu  12777  dedekindeulemeu  12778  dedekindeu  12779  suplociccreex  12780  suplociccex  12781  dedekindicclemuub  12782  dedekindicclemloc  12784  dedekindicclemlu  12786  dedekindicclemeu  12787  dedekindicclemicc  12788  dedekindicc  12789  ivthinclemlopn  12792  ivthinclemlr  12793  ivthinclemuopn  12794  ivthinclemur  12795  ivthinclemloc  12797  ivthinc  12799  limcimo  12812  cnplimclemr  12816  limccnp2lem  12823  limccoap  12825  eldvap  12829  logltb  12969  sbthom  13274  trilpo  13289  apdiff  13292
  Copyright terms: Public domain W3C validator