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

Theorem breq1 3764
Description: Equality theorem for a binary relation. (Contributed by NM, 31-Dec-1993.)
Assertion
Ref Expression
breq1  |-  ( A  =  B  ->  ( A R C  <->  B R C ) )

Proof of Theorem breq1
StepHypRef Expression
1 opeq1 3546 . . 3  |-  ( A  =  B  ->  <. A ,  C >.  =  <. B ,  C >. )
21eleq1d 2106 . 2  |-  ( A  =  B  ->  ( <. A ,  C >.  e.  R  <->  <. B ,  C >.  e.  R ) )
3 df-br 3762 . 2  |-  ( A R C  <->  <. A ,  C >.  e.  R )
4 df-br 3762 . 2  |-  ( B R C  <->  <. B ,  C >.  e.  R )
52, 3, 43bitr4g 212 1  |-  ( A  =  B  ->  ( A R C  <->  B R C ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 98    = wceq 1243    e. wcel 1393   <.cop 3375   class class class wbr 3761
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 630  ax-5 1336  ax-7 1337  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-10 1396  ax-11 1397  ax-i12 1398  ax-bndl 1399  ax-4 1400  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-i5r 1428  ax-ext 2022
This theorem depends on definitions:  df-bi 110  df-3an 887  df-tru 1246  df-nf 1350  df-sb 1646  df-clab 2027  df-cleq 2033  df-clel 2036  df-nfc 2167  df-v 2556  df-un 2919  df-sn 3378  df-pr 3379  df-op 3381  df-br 3762
This theorem is referenced by:  breq12  3766  breq1i  3768  breq1d  3771  nbrne2  3779  brab1  3806  pocl  4037  swopolem  4039  swopo  4040  issod  4053  sowlin  4054  sotritrieq  4059  frirrg  4082  vtoclr  4366  brcog  4480  brcogw  4482  opelcnvg  4493  dfdmf  4506  eldmg  4508  dfrnf  4553  dfres2  4636  imasng  4668  coi1  4814  dffun6f  4893  funmo  4895  fun11  4944  fveq2  5156  funfveu  5166  sefvex  5174  nfunsn  5185  fvmptss2  5225  f1ompt  5298  fmptco  5308  dff13  5385  foeqcnvco  5408  isorel  5426  isocnv  5429  isotr  5434  isoini  5435  isopolem  5439  isosolem  5441  f1oiso  5443  f1oiso2  5444  caovordig  5644  caovordg  5646  caovord3d  5649  caovord  5650  caovord3  5652  caofrss  5713  caoftrn  5714  poxp  5831  brtpos2  5844  rntpos  5850  tpostpos  5857  ertr  6099  ecopovsym  6180  ecopovtrn  6181  ecopovsymg  6183  ecopovtrng  6184  th3qlem2  6187  isfi  6219  en0  6253  en1  6257  en1bg  6258  endisj  6276  xpcomco  6278  nneneq  6298  findcard  6322  findcard2  6323  findcard2s  6324  isnumi  6334  cardval3ex  6337  oncardval  6338  cardonle  6339  nqtri3or  6466  ltsonq  6468  ltanqg  6470  ltmnqg  6471  ltexnqq  6478  subhalfnqq  6484  ltbtwnnqq  6485  archnqq  6487  nqnq0pi  6508  prcdnql  6554  prcunqu  6555  prnmaxl  6558  genpcuu  6590  genprndl  6591  genprndu  6592  nqprm  6612  nqprrnd  6613  nqprdisj  6614  nqprloc  6615  nqpru  6622  addnqprlemrl  6627  addnqprlemfl  6629  addnqprlemfu  6630  prmuloc2  6637  mulnqprlemrl  6643  mulnqprlemfl  6645  mulnqprlemfu  6646  1idprl  6660  ltnqpr  6663  ltnqpri  6664  prplnqu  6690  recexprlemell  6692  recexprlemm  6694  recexprlemdisj  6700  recexprlemloc  6701  recexprlem1ssu  6704  recexprlemss1l  6705  aptiprlemu  6710  archpr  6713  cauappcvgprlemm  6715  cauappcvgprlemladdfl  6725  cauappcvgprlem2  6730  cauappcvgpr  6732  caucvgprlemnkj  6736  caucvgprlemnbj  6737  caucvgprlemcl  6746  caucvgprlem2  6750  caucvgpr  6752  caucvgprprlemelu  6756  caucvgprprlemcbv  6757  caucvgprprlemval  6758  caucvgprprlemnbj  6763  caucvgprprlemmu  6765  caucvgprprlemopu  6769  caucvgprprlemexbt  6776  caucvgprprlemaddq  6778  caucvgprprlem1  6779  caucvgprprlem2  6780  caucvgprpr  6782  lttrsr  6819  ltsosr  6821  1ne0sr  6823  ltasrg  6827  aptisr  6835  mulextsr1  6837  archsr  6838  caucvgsrlemgt1  6851  caucvgsrlemoffres  6856  caucvgsr  6858  axpre-ltwlin  6929  axpre-lttrn  6930  axpre-apti  6931  axpre-ltadd  6932  axpre-mulext  6934  axcaucvglemcau  6944  axcaucvglemres  6945  axcaucvg  6946  ltxrlt  7056  lttri3  7069  lt0ne0d  7474  reapti  7537  apreim  7561  recexap  7601  nnsub  7919  nominpos  8126  nn0n0n1ge2b  8283  zextle  8294  fzind  8316  btwnz  8320  uzval  8438  ublbneg  8511  lbzbi  8514  qreccl  8538  xrltnsym  8672  xrlttr  8674  xrltso  8675  xrlttri3  8676  nltpnft  8688  xrrebnd  8690  xltnegi  8706  ixxval  8723  elixx1  8724  elioo2  8748  iccid  8752  fzval  8834  elfz1  8837  expcl2lemap  9136  expclzaplem  9148  expclzap  9149  expap0i  9156  absle  9554  climshft  9693  sqrt2irr  9746  nn0seqcvgd  9748  algcvgblem  9756
  Copyright terms: Public domain W3C validator