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

Theorem breq1 3767
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 3549 . . 3  |-  ( A  =  B  ->  <. A ,  C >.  =  <. B ,  C >. )
21eleq1d 2106 . 2  |-  ( A  =  B  ->  ( <. A ,  C >.  e.  R  <->  <. B ,  C >.  e.  R ) )
3 df-br 3765 . 2  |-  ( A R C  <->  <. A ,  C >.  e.  R )
4 df-br 3765 . 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 3378   class class class wbr 3764
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 2559  df-un 2922  df-sn 3381  df-pr 3382  df-op 3384  df-br 3765
This theorem is referenced by:  breq12  3769  breq1i  3771  breq1d  3774  nbrne2  3782  brab1  3809  pocl  4040  swopolem  4042  swopo  4043  issod  4056  sowlin  4057  sotritrieq  4062  frirrg  4087  wetriext  4301  vtoclr  4388  brcog  4502  brcogw  4504  opelcnvg  4515  dfdmf  4528  eldmg  4530  dfrnf  4575  dfres2  4658  imasng  4690  coi1  4836  dffun6f  4915  funmo  4917  fun11  4966  fveq2  5178  funfveu  5188  sefvex  5196  nfunsn  5207  fvmptss2  5247  f1ompt  5320  fmptco  5330  dff13  5407  foeqcnvco  5430  isorel  5448  isocnv  5451  isotr  5456  isoini  5457  isopolem  5461  isosolem  5463  f1oiso  5465  f1oiso2  5466  caovordig  5666  caovordg  5668  caovord3d  5671  caovord  5672  caovord3  5674  caofrss  5735  caoftrn  5736  poxp  5853  brtpos2  5866  rntpos  5872  tpostpos  5879  ertr  6121  ecopovsym  6202  ecopovtrn  6203  ecopovsymg  6205  ecopovtrng  6206  th3qlem2  6209  isfi  6241  en0  6275  en1  6279  en1bg  6280  endisj  6298  xpcomco  6300  nneneq  6320  findcard  6345  findcard2  6346  findcard2s  6347  isnumi  6362  cardval3ex  6365  oncardval  6366  cardonle  6367  nqtri3or  6494  ltsonq  6496  ltanqg  6498  ltmnqg  6499  ltexnqq  6506  subhalfnqq  6512  ltbtwnnqq  6513  archnqq  6515  nqnq0pi  6536  prcdnql  6582  prcunqu  6583  prnmaxl  6586  genpcuu  6618  genprndl  6619  genprndu  6620  nqprm  6640  nqprrnd  6641  nqprdisj  6642  nqprloc  6643  nqpru  6650  addnqprlemrl  6655  addnqprlemfl  6657  addnqprlemfu  6658  prmuloc2  6665  mulnqprlemrl  6671  mulnqprlemfl  6673  mulnqprlemfu  6674  1idprl  6688  ltnqpr  6691  ltnqpri  6692  prplnqu  6718  recexprlemell  6720  recexprlemm  6722  recexprlemdisj  6728  recexprlemloc  6729  recexprlem1ssu  6732  recexprlemss1l  6733  aptiprlemu  6738  archpr  6741  cauappcvgprlemm  6743  cauappcvgprlemladdfl  6753  cauappcvgprlem2  6758  cauappcvgpr  6760  caucvgprlemnkj  6764  caucvgprlemnbj  6765  caucvgprlemcl  6774  caucvgprlem2  6778  caucvgpr  6780  caucvgprprlemelu  6784  caucvgprprlemcbv  6785  caucvgprprlemval  6786  caucvgprprlemnbj  6791  caucvgprprlemmu  6793  caucvgprprlemopu  6797  caucvgprprlemexbt  6804  caucvgprprlemaddq  6806  caucvgprprlem1  6807  caucvgprprlem2  6808  caucvgprpr  6810  lttrsr  6847  ltsosr  6849  1ne0sr  6851  ltasrg  6855  aptisr  6863  mulextsr1  6865  archsr  6866  caucvgsrlemgt1  6879  caucvgsrlemoffres  6884  caucvgsr  6886  axpre-ltwlin  6957  axpre-lttrn  6958  axpre-apti  6959  axpre-ltadd  6960  axpre-mulext  6962  axcaucvglemcau  6972  axcaucvglemres  6973  axcaucvg  6974  ltxrlt  7085  lttri3  7098  lt0ne0d  7505  reapti  7570  apreim  7594  recexap  7634  nnsub  7952  nominpos  8162  nn0n0n1ge2b  8320  zextle  8331  fzind  8353  btwnz  8357  uzval  8475  ublbneg  8548  lbzbi  8551  qreccl  8576  xrltnsym  8714  xrlttr  8716  xrltso  8717  xrlttri3  8718  nltpnft  8730  xrrebnd  8732  xltnegi  8748  ixxval  8765  elixx1  8766  elioo2  8790  iccid  8794  fzval  8876  elfz1  8879  qtri3or  9098  qbtwnzlemstep  9103  qbtwnzlemshrink  9104  qbtwnzlemex  9105  qbtwnz  9106  rebtwn2zlemstep  9107  rebtwn2zlemshrink  9108  rebtwn2z  9109  qbtwnre  9111  flval  9116  flqlelt  9118  flqbi  9132  flqeqceilz  9160  expcl2lemap  9267  expclzaplem  9279  expclzap  9280  expap0i  9287  absle  9685  climshft  9825  sqrt2irr  9878  nn0seqcvgd  9880  algcvgblem  9888
  Copyright terms: Public domain W3C validator