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

Theorem breq1 3741
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 3523 . . 3 (A = B → ⟨A, 𝐶⟩ = ⟨B, 𝐶⟩)
21eleq1d 2088 . 2 (A = B → (⟨A, 𝐶 𝑅 ↔ ⟨B, 𝐶 𝑅))
3 df-br 3739 . 2 (A𝑅𝐶 ↔ ⟨A, 𝐶 𝑅)
4 df-br 3739 . 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 1228   wcel 1374  cop 3353   class class class wbr 3738
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 617  ax-5 1316  ax-7 1317  ax-gen 1318  ax-ie1 1363  ax-ie2 1364  ax-8 1376  ax-10 1377  ax-11 1378  ax-i12 1379  ax-bnd 1380  ax-4 1381  ax-17 1400  ax-i9 1404  ax-ial 1409  ax-i5r 1410  ax-ext 2004
This theorem depends on definitions:  df-bi 110  df-3an 875  df-tru 1231  df-nf 1330  df-sb 1628  df-clab 2009  df-cleq 2015  df-clel 2018  df-nfc 2149  df-v 2537  df-un 2899  df-sn 3356  df-pr 3357  df-op 3359  df-br 3739
This theorem is referenced by:  breq12  3743  breq1i  3745  breq1d  3748  nbrne2  3756  brab1  3783  pocl  4014  swopolem  4016  swopo  4017  issod  4030  sowlin  4031  sotritrieq  4036  vtoclr  4315  brcog  4429  brcogw  4431  opelcnvg  4442  dfdmf  4455  eldmg  4457  dfrnf  4502  dfres2  4585  imasng  4617  coi1  4763  dffun6f  4841  funmo  4843  fun11  4892  fveq2  5103  funfveu  5113  sefvex  5121  nfunsn  5132  fvmptss2  5172  f1ompt  5245  fmptco  5255  dff13  5332  foeqcnvco  5355  isorel  5373  isocnv  5376  isotr  5381  isoini  5382  isopolem  5386  isosolem  5388  f1oiso  5390  f1oiso2  5391  caovordig  5589  caovordg  5591  caovord3d  5594  caovord  5595  caovord3  5597  caofrss  5658  caoftrn  5659  poxp  5775  brtpos2  5788  rntpos  5794  tpostpos  5801  ertr  6032  ecopovsym  6113  ecopovtrn  6114  ecopovsymg  6116  ecopovtrng  6117  th3qlem2  6120  nqtri3or  6255  ltsonq  6257  ltanqg  6259  ltmnqg  6260  ltexnqq  6266  subhalfnqq  6271  ltbtwnnqq  6272  archnqq  6274  nqnq0pi  6293  prcdnql  6338  prcunqu  6339  prnmaxl  6342  genpcuu  6375  genprndl  6376  genprndu  6377  nqprm  6397  nqprrnd  6398  nqprdisj  6399  nqprloc  6400  prmuloc2  6411  1idprl  6429  recexprlemell  6456  recexprlemm  6458  recexprlemdisj  6464  recexprlemloc  6465  recexprlem1ssu  6468  recexprlemss1l  6469  lttrsr  6509  ltsosr  6511  1ne0sr  6513  ltasrg  6517  axpre-ltwlin  6577  axpre-lttrn  6578  axpre-ltadd  6579  ltxrlt  6686
  Copyright terms: Public domain W3C validator