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

Theorem breq1 3840
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 3617 . . 3  |-  ( A  =  B  ->  <. A ,  C >.  =  <. B ,  C >. )
21eleq1d 2156 . 2  |-  ( A  =  B  ->  ( <. A ,  C >.  e.  R  <->  <. B ,  C >.  e.  R ) )
3 df-br 3838 . 2  |-  ( A R C  <->  <. A ,  C >.  e.  R )
4 df-br 3838 . 2  |-  ( B R C  <->  <. B ,  C >.  e.  R )
52, 3, 43bitr4g 221 1  |-  ( A  =  B  ->  ( A R C  <->  B R C ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 103    = wceq 1289    e. wcel 1438   <.cop 3444   class class class wbr 3837
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 665  ax-5 1381  ax-7 1382  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-8 1440  ax-10 1441  ax-11 1442  ax-i12 1443  ax-bndl 1444  ax-4 1445  ax-17 1464  ax-i9 1468  ax-ial 1472  ax-i5r 1473  ax-ext 2070
This theorem depends on definitions:  df-bi 115  df-3an 926  df-tru 1292  df-nf 1395  df-sb 1693  df-clab 2075  df-cleq 2081  df-clel 2084  df-nfc 2217  df-v 2621  df-un 3001  df-sn 3447  df-pr 3448  df-op 3450  df-br 3838
This theorem is referenced by:  breq12  3842  breq1i  3844  breq1d  3847  nbrne2  3855  brab1  3882  pocl  4121  swopolem  4123  swopo  4124  issod  4137  sowlin  4138  sotritrieq  4143  frirrg  4168  wetriext  4382  vtoclr  4474  brcog  4591  brcogw  4593  opelcnvg  4604  dfdmf  4617  eldmg  4619  dfrnf  4664  dfres2  4751  imasng  4784  coi1  4933  dffun6f  5015  funmo  5017  fun11  5067  fveq2  5289  funfveu  5302  sefvex  5310  nfunsn  5322  fvmptss2  5363  f1ompt  5434  fmptco  5448  dff13  5529  foeqcnvco  5551  isorel  5569  isocnv  5572  isotr  5577  isoini  5579  isopolem  5583  isosolem  5585  f1oiso  5587  f1oiso2  5588  caovordig  5792  caovordg  5794  caovord3d  5797  caovord  5798  caovord3  5800  caofrss  5861  caoftrn  5862  poxp  5979  brtpos2  5998  rntpos  6004  tpostpos  6011  ertr  6287  ecopovsym  6368  ecopovtrn  6369  ecopovsymg  6371  ecopovtrng  6372  th3qlem2  6375  isfi  6458  en0  6492  en1  6496  en1bg  6497  endisj  6520  xpcomco  6522  dom0  6534  ssenen  6547  nneneq  6553  domfiexmid  6574  findcard  6584  findcard2  6585  findcard2s  6586  isinfinf  6593  tridc  6595  fimax2gtrilemstep  6596  fimax2gtri  6597  fisseneq  6621  en1eqsnbi  6637  isbth  6655  supmoti  6667  eqsupti  6670  supubti  6673  suplubti  6674  supsnti  6679  isotilem  6680  isoti  6681  supisolem  6682  supisoex  6683  infminti  6701  isnumi  6789  cardval3ex  6792  oncardval  6793  cardonle  6794  exmidfodomrlemr  6807  exmidfodomrlemrALT  6808  nqtri3or  6934  ltsonq  6936  ltanqg  6938  ltmnqg  6939  ltexnqq  6946  subhalfnqq  6952  ltbtwnnqq  6953  archnqq  6955  nqnq0pi  6976  prcdnql  7022  prcunqu  7023  prnmaxl  7026  genpcuu  7058  genprndl  7059  genprndu  7060  nqprm  7080  nqprrnd  7081  nqprdisj  7082  nqprloc  7083  nqpru  7090  addnqprlemrl  7095  addnqprlemfl  7097  addnqprlemfu  7098  prmuloc2  7105  mulnqprlemrl  7111  mulnqprlemfl  7113  mulnqprlemfu  7114  1idprl  7128  ltnqpr  7131  ltnqpri  7132  prplnqu  7158  recexprlemell  7160  recexprlemm  7162  recexprlemdisj  7168  recexprlemloc  7169  recexprlem1ssu  7172  recexprlemss1l  7173  aptiprlemu  7178  archpr  7181  cauappcvgprlemm  7183  cauappcvgprlemladdfl  7193  cauappcvgprlem2  7198  cauappcvgpr  7200  caucvgprlemnkj  7204  caucvgprlemnbj  7205  caucvgprlemcl  7214  caucvgprlem2  7218  caucvgpr  7220  caucvgprprlemelu  7224  caucvgprprlemcbv  7225  caucvgprprlemval  7226  caucvgprprlemnbj  7231  caucvgprprlemmu  7233  caucvgprprlemopu  7237  caucvgprprlemexbt  7244  caucvgprprlemaddq  7246  caucvgprprlem1  7247  caucvgprprlem2  7248  caucvgprpr  7250  lttrsr  7287  ltsosr  7289  1ne0sr  7291  ltasrg  7295  aptisr  7303  mulextsr1  7305  archsr  7306  caucvgsrlemgt1  7319  caucvgsrlemoffres  7324  caucvgsr  7326  axpre-ltwlin  7397  axpre-lttrn  7398  axpre-apti  7399  axpre-ltadd  7400  axpre-mulext  7402  axcaucvglemcau  7412  axcaucvglemres  7413  axcaucvg  7414  ltxrlt  7531  lttri3  7544  lt0ne0d  7967  reapti  8032  apreim  8056  recexap  8096  lbreu  8378  lble  8380  suprleubex  8387  nnsub  8432  nominpos  8623  nn0n0n1ge2b  8796  zextle  8807  fzind  8831  btwnz  8835  uzval  8990  supinfneg  9052  infsupneg  9053  ublbneg  9067  lbzbi  9070  qreccl  9096  xrltnsym  9232  xrlttr  9234  xrltso  9235  xrlttri3  9236  nltpnft  9248  xrrebnd  9250  xltnegi  9266  ixxval  9283  elixx1  9284  elioo2  9308  iccid  9312  fzval  9395  elfz1  9398  qtri3or  9619  exbtwnzlemstep  9624  exbtwnzlemshrink  9625  exbtwnzlemex  9626  exbtwnz  9627  rebtwn2zlemstep  9629  rebtwn2zlemshrink  9630  rebtwn2z  9631  qbtwnre  9633  qbtwnxr  9634  flval  9644  flqlelt  9648  flqbi  9662  flqeqceilz  9690  modqid2  9723  seq3f1olemqsum  9894  seq3f1oleml  9897  seq3f1o  9898  expcl2lemap  9932  expclzaplem  9944  expclzap  9945  expap0i  9952  hashinfuni  10150  hashennnuni  10152  hashunlem  10177  zfz1isolemiso  10209  zfz1isolem1  10210  zfz1iso  10211  absle  10487  maxleast  10611  rexanre  10618  rexico  10619  fimaxre2  10622  minmax  10625  climshft  10656  isummolem3  10734  isummolem2a  10735  isummo  10737  zisum  10738  fisum  10742  fsum3  10743  fisumcvg3  10752  fsumcl2lem  10755  fsumadd  10763  sumsnf  10766  fsummulc2  10805  absdvdsb  10896  zdvdsdc  10899  dvdsabseq  10930  dvdsdivcl  10933  dvdsext  10938  divalglemnn  11000  divalglemeunn  11003  divalglemeuneg  11005  divalgmod  11009  ndvdssub  11012  zsupcllemstep  11023  gcdsupex  11031  gcdsupcl  11032  gcddvds  11037  dvdslegcd  11038  bezoutlemmain  11069  bezoutlemex  11072  bezoutlemzz  11073  bezoutlemmo  11077  bezoutlemeu  11078  bezoutlemle  11079  bezoutlemsup  11080  dfgcd3  11081  dfgcd2  11085  gcdzeq  11093  dvdssq  11102  nn0seqcvgd  11105  algcvgblem  11113  lcmval  11127  lcmdvds  11143  lcmgcdeq  11147  coprmgcdb  11152  ncoprmgcdne1b  11153  coprmdvds1  11155  1nprm  11178  1idssfct  11179  isprm2lem  11180  isprm2  11181  dvdsprime  11186  nprm  11187  3prm  11192  dvdsprm  11200  exprmfct  11201  coprm  11205  sqrt2irr  11223
  Copyright terms: Public domain W3C validator