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

Theorem breq1 3823
Description: Equality theorem for a binary relation. (Contributed by NM, 31-Dec-1993.)
Assertion
Ref Expression
breq1 (𝐴 = 𝐵 → (𝐴𝑅𝐶𝐵𝑅𝐶))

Proof of Theorem breq1
StepHypRef Expression
1 opeq1 3605 . . 3 (𝐴 = 𝐵 → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐶⟩)
21eleq1d 2153 . 2 (𝐴 = 𝐵 → (⟨𝐴, 𝐶⟩ ∈ 𝑅 ↔ ⟨𝐵, 𝐶⟩ ∈ 𝑅))
3 df-br 3821 . 2 (𝐴𝑅𝐶 ↔ ⟨𝐴, 𝐶⟩ ∈ 𝑅)
4 df-br 3821 . 2 (𝐵𝑅𝐶 ↔ ⟨𝐵, 𝐶⟩ ∈ 𝑅)
52, 3, 43bitr4g 221 1 (𝐴 = 𝐵 → (𝐴𝑅𝐶𝐵𝑅𝐶))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 103   = wceq 1287  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  breq1i  3827  breq1d  3830  nbrne2  3838  brab1  3865  pocl  4104  swopolem  4106  swopo  4107  issod  4120  sowlin  4121  sotritrieq  4126  frirrg  4151  wetriext  4365  vtoclr  4454  brcog  4571  brcogw  4573  opelcnvg  4584  dfdmf  4597  eldmg  4599  dfrnf  4644  dfres2  4731  imasng  4764  coi1  4912  dffun6f  4994  funmo  4996  fun11  5046  fveq2  5268  funfveu  5281  sefvex  5289  nfunsn  5301  fvmptss2  5342  f1ompt  5413  fmptco  5427  dff13  5508  foeqcnvco  5530  isorel  5548  isocnv  5551  isotr  5556  isoini  5558  isopolem  5562  isosolem  5564  f1oiso  5566  f1oiso2  5567  caovordig  5767  caovordg  5769  caovord3d  5772  caovord  5773  caovord3  5775  caofrss  5836  caoftrn  5837  poxp  5954  brtpos2  5970  rntpos  5976  tpostpos  5983  ertr  6259  ecopovsym  6340  ecopovtrn  6341  ecopovsymg  6343  ecopovtrng  6344  th3qlem2  6347  isfi  6430  en0  6464  en1  6468  en1bg  6469  endisj  6492  xpcomco  6494  dom0  6506  ssenen  6519  nneneq  6525  domfiexmid  6546  findcard  6556  findcard2  6557  findcard2s  6558  isinfinf  6565  tridc  6567  fimax2gtrilemstep  6568  fimax2gtri  6569  fisseneq  6592  en1eqsnbi  6607  isbth  6620  supmoti  6632  eqsupti  6635  supubti  6638  suplubti  6639  supsnti  6644  isotilem  6645  isoti  6646  supisolem  6647  supisoex  6648  infminti  6666  isnumi  6754  cardval3ex  6757  oncardval  6758  cardonle  6759  exmidfodomrlemr  6772  exmidfodomrlemrALT  6773  nqtri3or  6899  ltsonq  6901  ltanqg  6903  ltmnqg  6904  ltexnqq  6911  subhalfnqq  6917  ltbtwnnqq  6918  archnqq  6920  nqnq0pi  6941  prcdnql  6987  prcunqu  6988  prnmaxl  6991  genpcuu  7023  genprndl  7024  genprndu  7025  nqprm  7045  nqprrnd  7046  nqprdisj  7047  nqprloc  7048  nqpru  7055  addnqprlemrl  7060  addnqprlemfl  7062  addnqprlemfu  7063  prmuloc2  7070  mulnqprlemrl  7076  mulnqprlemfl  7078  mulnqprlemfu  7079  1idprl  7093  ltnqpr  7096  ltnqpri  7097  prplnqu  7123  recexprlemell  7125  recexprlemm  7127  recexprlemdisj  7133  recexprlemloc  7134  recexprlem1ssu  7137  recexprlemss1l  7138  aptiprlemu  7143  archpr  7146  cauappcvgprlemm  7148  cauappcvgprlemladdfl  7158  cauappcvgprlem2  7163  cauappcvgpr  7165  caucvgprlemnkj  7169  caucvgprlemnbj  7170  caucvgprlemcl  7179  caucvgprlem2  7183  caucvgpr  7185  caucvgprprlemelu  7189  caucvgprprlemcbv  7190  caucvgprprlemval  7191  caucvgprprlemnbj  7196  caucvgprprlemmu  7198  caucvgprprlemopu  7202  caucvgprprlemexbt  7209  caucvgprprlemaddq  7211  caucvgprprlem1  7212  caucvgprprlem2  7213  caucvgprpr  7215  lttrsr  7252  ltsosr  7254  1ne0sr  7256  ltasrg  7260  aptisr  7268  mulextsr1  7270  archsr  7271  caucvgsrlemgt1  7284  caucvgsrlemoffres  7289  caucvgsr  7291  axpre-ltwlin  7362  axpre-lttrn  7363  axpre-apti  7364  axpre-ltadd  7365  axpre-mulext  7367  axcaucvglemcau  7377  axcaucvglemres  7378  axcaucvg  7379  ltxrlt  7496  lttri3  7509  lt0ne0d  7932  reapti  7997  apreim  8021  recexap  8061  lbreu  8341  lble  8343  suprleubex  8350  nnsub  8395  nominpos  8586  nn0n0n1ge2b  8759  zextle  8770  fzind  8794  btwnz  8798  uzval  8953  supinfneg  9015  infsupneg  9016  ublbneg  9030  lbzbi  9033  qreccl  9059  xrltnsym  9195  xrlttr  9197  xrltso  9198  xrlttri3  9199  nltpnft  9211  xrrebnd  9213  xltnegi  9229  ixxval  9246  elixx1  9247  elioo2  9271  iccid  9275  fzval  9358  elfz1  9361  qtri3or  9582  exbtwnzlemstep  9587  exbtwnzlemshrink  9588  exbtwnzlemex  9589  exbtwnz  9590  rebtwn2zlemstep  9592  rebtwn2zlemshrink  9593  rebtwn2z  9594  qbtwnre  9596  qbtwnxr  9597  flval  9607  flqlelt  9611  flqbi  9625  flqeqceilz  9653  modqid2  9686  iseqf1olemqsum  9833  iseqf1oleml  9836  iseqf1o  9837  expcl2lemap  9865  expclzaplem  9877  expclzap  9878  expap0i  9885  hashinfuni  10081  hashennnuni  10083  hashunlem  10108  zfz1isolemiso  10140  zfz1isolem1  10141  zfz1iso  10142  absle  10417  maxleast  10541  rexanre  10548  rexico  10549  fimaxre2  10551  minmax  10554  climshft  10585  isummolem3  10659  isummolem2a  10660  isummo  10662  zisum  10663  fisum  10665  absdvdsb  10689  zdvdsdc  10692  dvdsabseq  10723  dvdsdivcl  10726  dvdsext  10731  divalglemnn  10793  divalglemeunn  10796  divalglemeuneg  10798  divalgmod  10802  ndvdssub  10805  zsupcllemstep  10816  gcdsupex  10824  gcdsupcl  10825  gcddvds  10830  dvdslegcd  10831  bezoutlemmain  10862  bezoutlemex  10865  bezoutlemzz  10866  bezoutlemmo  10870  bezoutlemeu  10871  bezoutlemle  10872  bezoutlemsup  10873  dfgcd3  10874  dfgcd2  10878  gcdzeq  10886  dvdssq  10895  nn0seqcvgd  10898  algcvgblem  10906  lcmval  10920  lcmdvds  10936  lcmgcdeq  10940  coprmgcdb  10945  ncoprmgcdne1b  10946  coprmdvds1  10948  1nprm  10971  1idssfct  10972  isprm2lem  10973  isprm2  10974  dvdsprime  10979  nprm  10980  3prm  10985  dvdsprm  10993  exprmfct  10994  coprm  10998  sqrt2irr  11016
  Copyright terms: Public domain W3C validator