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

Theorem breq2 3824
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 3606 . . 3  |-  ( A  =  B  ->  <. C ,  A >.  =  <. C ,  B >. )
21eleq1d 2153 . 2  |-  ( A  =  B  ->  ( <. C ,  A >.  e.  R  <->  <. C ,  B >.  e.  R ) )
3 df-br 3821 . 2  |-  ( C R A  <->  <. C ,  A >.  e.  R )
4 df-br 3821 . 2  |-  ( C R B  <->  <. C ,  B >.  e.  R )
52, 3, 43bitr4g 221 1  |-  ( A  =  B  ->  ( C R A  <->  C R B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 103    = wceq 1287    e. wcel 1436   <.cop 3434   class class class wbr 3820
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 663  ax-5 1379  ax-7 1380  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-8 1438  ax-10 1439  ax-11 1440  ax-i12 1441  ax-bndl 1442  ax-4 1443  ax-17 1462  ax-i9 1466  ax-ial 1470  ax-i5r 1471  ax-ext 2067
This theorem depends on definitions:  df-bi 115  df-3an 924  df-tru 1290  df-nf 1393  df-sb 1690  df-clab 2072  df-cleq 2078  df-clel 2081  df-nfc 2214  df-v 2617  df-un 2992  df-sn 3437  df-pr 3438  df-op 3440  df-br 3821
This theorem is referenced by:  breq12  3825  breq2i  3828  breq2d  3832  nbrne1  3837  pocl  4104  swopolem  4106  swopo  4107  sowlin  4121  sotricim  4124  sotritrieq  4126  seex  4136  frind  4153  wetriext  4365  vtoclr  4454  posng  4478  brcog  4571  brcogw  4573  opelcnvg  4584  dfdmf  4597  breldmg  4610  dfrnf  4644  dmcoss  4670  resieq  4691  dfres2  4731  elimag  4745  elreimasng  4765  elimasn  4766  intirr  4785  poirr2  4791  poltletr  4799  dffun6f  4994  dffun4f  4997  fun11  5046  brprcneu  5261  fv3  5291  tz6.12c  5297  relelfvdm  5299  funbrfv  5306  fnbrfvb  5308  funfvdm2f  5332  fndmdif  5367  dff3im  5407  fmptco  5427  foeqcnvco  5530  isorel  5548  isocnv  5551  isotr  5556  isopolem  5562  isosolem  5564  f1oiso  5566  f1oiso2  5567  caovordig  5767  caovordg  5769  caovord  5773  caofrss  5836  caoftrn  5837  poxp  5954  tposoprab  5999  ertr  6259  ecopovsym  6340  ecopovtrn  6341  ecopovsymg  6343  ecopovtrng  6344  th3qlem2  6347  domeng  6421  eqeng  6435  snfig  6483  nneneq  6525  nnfi  6540  ssfilem  6543  domfiexmid  6546  dif1enen  6548  diffitest  6555  findcard  6556  findcard2  6557  findcard2s  6558  diffisn  6561  tridc  6567  fimax2gtrilemstep  6568  inffiexmid  6574  unsnfi  6581  fisseneq  6592  isbth  6620  supmoti  6632  eqsupti  6635  supubti  6638  suplubti  6639  suplub2ti  6640  supmaxti  6643  supsnti  6644  isotilem  6645  isoti  6646  supisolem  6647  supisoex  6648  cardcl  6753  isnumi  6754  cardval3ex  6757  exmidfodomrlemr  6772  exmidfodomrlemrALT  6773  nqtri3or  6899  ltsonq  6901  ltanqg  6903  ltmnqg  6904  ltexnqq  6911  nsmallnqq  6915  subhalfnqq  6917  ltbtwnnqq  6918  prarloclemarch2  6922  nqnq0pi  6941  prcdnql  6987  prcunqu  6988  prnminu  6992  genpcdl  7022  genprndl  7024  genprndu  7025  genpdisj  7026  nqprm  7045  nqprrnd  7046  nqprdisj  7047  nqprloc  7048  nqprlu  7050  nqprl  7054  addnqprlemru  7061  addnqprlemfl  7062  addnqprlemfu  7063  mulnqprlemru  7077  mulnqprlemfl  7078  mulnqprlemfu  7079  1idpru  7094  ltnqpr  7096  ltnqpri  7097  prplnqu  7123  recexprlemelu  7126  recexprlemm  7127  recexprlemloc  7134  recexprlem1ssl  7136  recexprlemss1u  7139  cauappcvgprlemm  7148  cauappcvgprlemopu  7151  cauappcvgprlemupu  7152  cauappcvgprlemdisj  7154  cauappcvgprlemloc  7155  cauappcvgprlemladdfu  7157  cauappcvgprlemladdru  7159  cauappcvgprlemladdrl  7160  cauappcvgprlem2  7163  caucvgprlemnkj  7169  caucvgprlemnbj  7170  caucvgprlemm  7171  caucvgprlemopu  7174  caucvgprlemupu  7175  caucvgprlemdisj  7177  caucvgprlemloc  7178  caucvgprlemcl  7179  caucvgprlemladdfu  7180  caucvgprlemladdrl  7181  caucvgprlem2  7183  caucvgprprlemelu  7189  caucvgprprlemcbv  7190  caucvgprprlemval  7191  caucvgprprlemnbj  7196  caucvgprprlemmu  7198  caucvgprprlemexbt  7209  caucvgprprlemaddq  7211  caucvgprprlem1  7212  caucvgprprlem2  7213  lttrsr  7252  ltsosr  7254  ltasrg  7260  recexgt0sr  7263  mulgt0sr  7267  aptisr  7268  mulextsr1  7270  srpospr  7272  caucvgsrlemgt1  7284  caucvgsrlemoffres  7289  caucvgsr  7291  axprecex  7359  axpre-ltwlin  7362  axpre-lttrn  7363  axpre-apti  7364  axpre-ltadd  7365  axpre-mulgt0  7366  axpre-mulext  7367  axcaucvglemcau  7377  axcaucvglemres  7378  axcaucvg  7379  ltxrlt  7496  lttri3  7509  ltne  7514  eqle  7520  reapti  7997  apreim  8021  squeeze0  8300  lbreu  8341  lble  8343  suprleubex  8350  nnge1  8380  nn2ge  8389  nn1gt1  8390  nnsub  8395  nominpos  8586  nn0ge0  8631  elnnnn0b  8650  nn0ge2m1nn  8666  zdclt  8757  suprzclex  8777  peano2uz2  8786  peano5uzti  8787  dfuzi  8789  uzind  8790  uzind3  8792  eluz1  8955  uzind4  9008  indstr  9013  supinfneg  9015  infsupneg  9016  indstr2  9028  ublbneg  9030  elrp  9068  mnfltxr  9188  nn0pnfge0  9193  xrltnsym  9195  xrlttr  9197  xrltso  9198  xrlttri3  9199  xrltne  9210  ngtmnft  9212  xrrebnd  9213  z2ge  9220  xltnegi  9229  ixxval  9246  elixx1  9247  elioo2  9271  iccid  9275  iccsupr  9316  repos  9320  fzval  9358  elfz1  9361  fzm1  9444  exbtwnzlemstep  9587  exbtwnzlemex  9589  qbtwnre  9596  qbtwnxr  9597  flval  9607  apbtwnz  9609  modqid2  9686  modqmuladdnn0  9703  serige0  9850  expival  9855  expge0  9889  expge1  9890  facdiv  10042  facwordi  10044  hashinfom  10082  hashennn  10084  hashunlem  10108  zfz1iso  10142  ovshftex  10149  shftfibg  10150  shftfib  10153  shftfn  10154  2shfti  10161  sqrt0rlem  10331  resqrexlemex  10353  rsqrmo  10355  resqrtcl  10357  rersqrtthlem  10358  sqrtsq  10372  cau3lem  10442  caubnd2  10445  maxleim  10533  maxabslemval  10536  maxleast  10541  maxleb  10544  fimaxre2  10551  minmax  10554  climi  10568  climeu  10577  climmo  10579  2clim  10582  addcn2  10591  mulcn2  10593  cn1lem  10594  isummo  10662  zisum  10663  fisum  10665  dvdsabsb  10690  0dvds  10691  alzdvds  10730  dvdsext  10731  fzo0dvdseq  10733  2tp1odd  10759  2teven  10762  divalglemnn  10793  divalglemeunn  10796  divalglemeuneg  10798  zsupcllemstep  10816  gcdval  10826  gcddvds  10830  bezoutlemstep  10861  bezoutlemmain  10862  bezoutlemex  10865  bezoutlemeu  10871  bezoutlemsup  10873  dfgcd3  10874  bezout  10875  dvdsgcd  10876  dfgcd2  10878  dvdssq  10895  lcmval  10920  lcmcllem  10924  dvdslcm  10926  lcmledvds  10927  lcmgcdlem  10934  lcmdvds  10936  coprmgcdb  10945  coprmdvds2  10950  cncongr1  10960  cncongr2  10961  isprm  10966  dvdsnprmd  10982  dvdsprm  10993  exprmfct  10994  isprm6  11001  prmexpb  11005  prmfac1  11006  rpexp  11007  sqrt2irr  11016  oddpwdclemdc  11026  oddpwdc  11027  sqpweven  11028  2sqpwodd  11029  sqne2sq  11030  oddennn  11080  evenennn  11081
  Copyright terms: Public domain W3C validator