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

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

Proof of Theorem breq1
StepHypRef Expression
1 opeq1 3540 . . 3 (A = B → ⟨A, 𝐶⟩ = ⟨B, 𝐶⟩)
21eleq1d 2103 . 2 (A = B → (⟨A, 𝐶 𝑅 ↔ ⟨B, 𝐶 𝑅))
3 df-br 3756 . 2 (A𝑅𝐶 ↔ ⟨A, 𝐶 𝑅)
4 df-br 3756 . 2 (B𝑅𝐶 ↔ ⟨B, 𝐶 𝑅)
52, 3, 43bitr4g 212 1 (A = B → (A𝑅𝐶B𝑅𝐶))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 98   = wceq 1242   wcel 1390  cop 3370   class class class wbr 3755
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 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bnd 1396  ax-4 1397  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019
This theorem depends on definitions:  df-bi 110  df-3an 886  df-tru 1245  df-nf 1347  df-sb 1643  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-v 2553  df-un 2916  df-sn 3373  df-pr 3374  df-op 3376  df-br 3756
This theorem is referenced by:  breq12  3760  breq1i  3762  breq1d  3765  nbrne2  3773  brab1  3800  pocl  4031  swopolem  4033  swopo  4034  issod  4047  sowlin  4048  sotritrieq  4053  vtoclr  4331  brcog  4445  brcogw  4447  opelcnvg  4458  dfdmf  4471  eldmg  4473  dfrnf  4518  dfres2  4601  imasng  4633  coi1  4779  dffun6f  4858  funmo  4860  fun11  4909  fveq2  5121  funfveu  5131  sefvex  5139  nfunsn  5150  fvmptss2  5190  f1ompt  5263  fmptco  5273  dff13  5350  foeqcnvco  5373  isorel  5391  isocnv  5394  isotr  5399  isoini  5400  isopolem  5404  isosolem  5406  f1oiso  5408  f1oiso2  5409  caovordig  5608  caovordg  5610  caovord3d  5613  caovord  5614  caovord3  5616  caofrss  5677  caoftrn  5678  poxp  5794  brtpos2  5807  rntpos  5813  tpostpos  5820  ertr  6057  ecopovsym  6138  ecopovtrn  6139  ecopovsymg  6141  ecopovtrng  6142  th3qlem2  6145  isfi  6177  en0  6211  en1  6215  en1bg  6216  endisj  6234  xpcomco  6236  nqtri3or  6380  ltsonq  6382  ltanqg  6384  ltmnqg  6385  ltexnqq  6391  subhalfnqq  6397  ltbtwnnqq  6398  archnqq  6400  nqnq0pi  6420  prcdnql  6466  prcunqu  6467  prnmaxl  6470  genpcuu  6502  genprndl  6503  genprndu  6504  nqprm  6524  nqprrnd  6525  nqprdisj  6526  nqprloc  6527  addnqprlemrl  6537  addnqprlemfl  6539  addnqprlemfu  6540  prmuloc2  6547  1idprl  6565  recexprlemell  6593  recexprlemm  6595  recexprlemdisj  6601  recexprlemloc  6602  recexprlem1ssu  6605  recexprlemss1l  6606  aptiprlemu  6611  archpr  6614  cauappcvgprlemm  6616  cauappcvgprlemladdfl  6626  cauappcvgprlem2  6631  cauappcvgpr  6633  lttrsr  6670  ltsosr  6672  1ne0sr  6674  ltasrg  6678  aptisr  6685  mulextsr1  6687  archsr  6688  axpre-ltwlin  6747  axpre-lttrn  6748  axpre-apti  6749  axpre-ltadd  6750  axpre-mulext  6752  ltxrlt  6862  lttri3  6875  lt0ne0d  7280  reapti  7343  apreim  7367  recexap  7396  nnsub  7713  nominpos  7919  nn0n0n1ge2b  8076  zextle  8087  fzind  8109  btwnz  8113  uzval  8231  ublbneg  8304  lbzbi  8307  qreccl  8331  xrltnsym  8464  xrlttr  8466  xrltso  8467  xrlttri3  8468  nltpnft  8480  xrrebnd  8482  xltnegi  8498  ixxval  8515  elixx1  8516  elioo2  8540  iccid  8544  fzval  8626  elfz1  8629  expcl2lemap  8901  expclzaplem  8913  expclzap  8914  expap0i  8921
  Copyright terms: Public domain W3C validator