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

Theorem breq1 3796
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 3578 . . 3 (𝐴 = 𝐵 → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐶⟩)
21eleq1d 2148 . 2 (𝐴 = 𝐵 → (⟨𝐴, 𝐶⟩ ∈ 𝑅 ↔ ⟨𝐵, 𝐶⟩ ∈ 𝑅))
3 df-br 3794 . 2 (𝐴𝑅𝐶 ↔ ⟨𝐴, 𝐶⟩ ∈ 𝑅)
4 df-br 3794 . 2 (𝐵𝑅𝐶 ↔ ⟨𝐵, 𝐶⟩ ∈ 𝑅)
52, 3, 43bitr4g 221 1 (𝐴 = 𝐵 → (𝐴𝑅𝐶𝐵𝑅𝐶))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 103   = wceq 1285  wcel 1434  cop 3409   class class class wbr 3793
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 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2064
This theorem depends on definitions:  df-bi 115  df-3an 922  df-tru 1288  df-nf 1391  df-sb 1687  df-clab 2069  df-cleq 2075  df-clel 2078  df-nfc 2209  df-v 2604  df-un 2978  df-sn 3412  df-pr 3413  df-op 3415  df-br 3794
This theorem is referenced by:  breq12  3798  breq1i  3800  breq1d  3803  nbrne2  3811  brab1  3838  pocl  4066  swopolem  4068  swopo  4069  issod  4082  sowlin  4083  sotritrieq  4088  frirrg  4113  wetriext  4327  vtoclr  4414  brcog  4530  brcogw  4532  opelcnvg  4543  dfdmf  4556  eldmg  4558  dfrnf  4603  dfres2  4688  imasng  4720  coi1  4866  dffun6f  4945  funmo  4947  fun11  4997  fveq2  5209  funfveu  5219  sefvex  5227  nfunsn  5239  fvmptss2  5279  f1ompt  5352  fmptco  5362  dff13  5439  foeqcnvco  5461  isorel  5479  isocnv  5482  isotr  5487  isoini  5488  isopolem  5492  isosolem  5494  f1oiso  5496  f1oiso2  5497  caovordig  5697  caovordg  5699  caovord3d  5702  caovord  5703  caovord3  5705  caofrss  5766  caoftrn  5767  poxp  5884  brtpos2  5900  rntpos  5906  tpostpos  5913  ertr  6187  ecopovsym  6268  ecopovtrn  6269  ecopovsymg  6271  ecopovtrng  6272  th3qlem2  6275  isfi  6308  en0  6342  en1  6346  en1bg  6347  endisj  6368  xpcomco  6370  nneneq  6392  domfiexmid  6413  findcard  6422  findcard2  6423  findcard2s  6424  supmoti  6465  eqsupti  6468  supubti  6471  suplubti  6472  supsnti  6477  isotilem  6478  isoti  6479  supisolem  6480  supisoex  6481  infminti  6499  isnumi  6510  cardval3ex  6513  oncardval  6514  cardonle  6515  nqtri3or  6648  ltsonq  6650  ltanqg  6652  ltmnqg  6653  ltexnqq  6660  subhalfnqq  6666  ltbtwnnqq  6667  archnqq  6669  nqnq0pi  6690  prcdnql  6736  prcunqu  6737  prnmaxl  6740  genpcuu  6772  genprndl  6773  genprndu  6774  nqprm  6794  nqprrnd  6795  nqprdisj  6796  nqprloc  6797  nqpru  6804  addnqprlemrl  6809  addnqprlemfl  6811  addnqprlemfu  6812  prmuloc2  6819  mulnqprlemrl  6825  mulnqprlemfl  6827  mulnqprlemfu  6828  1idprl  6842  ltnqpr  6845  ltnqpri  6846  prplnqu  6872  recexprlemell  6874  recexprlemm  6876  recexprlemdisj  6882  recexprlemloc  6883  recexprlem1ssu  6886  recexprlemss1l  6887  aptiprlemu  6892  archpr  6895  cauappcvgprlemm  6897  cauappcvgprlemladdfl  6907  cauappcvgprlem2  6912  cauappcvgpr  6914  caucvgprlemnkj  6918  caucvgprlemnbj  6919  caucvgprlemcl  6928  caucvgprlem2  6932  caucvgpr  6934  caucvgprprlemelu  6938  caucvgprprlemcbv  6939  caucvgprprlemval  6940  caucvgprprlemnbj  6945  caucvgprprlemmu  6947  caucvgprprlemopu  6951  caucvgprprlemexbt  6958  caucvgprprlemaddq  6960  caucvgprprlem1  6961  caucvgprprlem2  6962  caucvgprpr  6964  lttrsr  7001  ltsosr  7003  1ne0sr  7005  ltasrg  7009  aptisr  7017  mulextsr1  7019  archsr  7020  caucvgsrlemgt1  7033  caucvgsrlemoffres  7038  caucvgsr  7040  axpre-ltwlin  7111  axpre-lttrn  7112  axpre-apti  7113  axpre-ltadd  7114  axpre-mulext  7116  axcaucvglemcau  7126  axcaucvglemres  7127  axcaucvg  7128  ltxrlt  7245  lttri3  7258  lt0ne0d  7681  reapti  7746  apreim  7770  recexap  7810  lbreu  8090  lble  8092  suprleubex  8099  nnsub  8144  nominpos  8335  nn0n0n1ge2b  8508  zextle  8519  fzind  8543  btwnz  8547  uzval  8702  supinfneg  8764  infsupneg  8765  ublbneg  8779  lbzbi  8782  qreccl  8808  xrltnsym  8944  xrlttr  8946  xrltso  8947  xrlttri3  8948  nltpnft  8960  xrrebnd  8962  xltnegi  8978  ixxval  8995  elixx1  8996  elioo2  9020  iccid  9024  fzval  9107  elfz1  9110  qtri3or  9329  exbtwnzlemstep  9334  exbtwnzlemshrink  9335  exbtwnzlemex  9336  exbtwnz  9337  rebtwn2zlemstep  9339  rebtwn2zlemshrink  9340  rebtwn2z  9341  qbtwnre  9343  qbtwnxr  9344  flval  9354  flqlelt  9358  flqbi  9372  flqeqceilz  9400  modqid2  9433  expcl2lemap  9585  expclzaplem  9597  expclzap  9598  expap0i  9605  sizeinfuni  9801  sizeennnuni  9803  sizeunlem  9828  absle  10113  maxleast  10237  rexanre  10244  rexico  10245  fimaxre2  10247  minmax  10250  climshft  10281  absdvdsb  10358  zdvdsdc  10361  dvdsabseq  10392  dvdsdivcl  10395  dvdsext  10400  divalglemnn  10462  divalglemeunn  10465  divalglemeuneg  10467  divalgmod  10471  ndvdssub  10474  zsupcllemstep  10485  gcdsupex  10493  gcdsupcl  10494  gcddvds  10499  dvdslegcd  10500  bezoutlemmain  10531  bezoutlemex  10534  bezoutlemzz  10535  bezoutlemmo  10539  bezoutlemeu  10540  bezoutlemle  10541  bezoutlemsup  10542  dfgcd3  10543  dfgcd2  10547  gcdzeq  10555  dvdssq  10564  nn0seqcvgd  10567  algcvgblem  10575  lcmval  10589  lcmdvds  10605  lcmgcdeq  10609  coprmgcdb  10614  ncoprmgcdne1b  10615  coprmdvds1  10617  1nprm  10640  1idssfct  10641  isprm2lem  10642  isprm2  10643  dvdsprime  10648  nprm  10649  3prm  10654  dvdsprm  10662  exprmfct  10663  coprm  10667  sqrt2irr  10685
  Copyright terms: Public domain W3C validator