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

Theorem breq1d 3765
Description: Equality deduction for a binary relation. (Contributed by NM, 8-Feb-1996.)
Hypothesis
Ref Expression
breq1d.1
Assertion
Ref Expression
breq1d  R C  R C

Proof of Theorem breq1d
StepHypRef Expression
1 breq1d.1 . 2
2 breq1 3758 . 2  R C  R C
31, 2syl 14 1  R C  R C
Colors of variables: wff set class
Syntax hints:   wi 4   wb 98   wceq 1242   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-bndl 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:  eqbrtrd  3775  syl6eqbr  3792  sbcbr2g  3807  pofun  4040  fmptco  5273  isorel  5391  isocnv  5394  isotr  5399  caovordig  5608  caovordg  5610  caovord  5614  xporderlem  5793  reldmtpos  5809  brtposg  5810  tpostpos  5820  tposoprab  5836  th3qlem2  6145  ensn1g  6213  fndmeng  6225  xpsneng  6232  xpcomco  6236  ltsonq  6382  ltanqg  6384  ltmnqg  6385  archnqq  6400  prloc  6474  addnqprulem  6511  appdivnq  6544  mulnqpru  6550  mullocprlem  6551  1idpru  6567  cauappcvgprlemm  6617  cauappcvgprlemopl  6618  cauappcvgprlemlol  6619  cauappcvgprlemdisj  6623  cauappcvgprlemloc  6624  cauappcvgprlemladdfl  6627  cauappcvgprlemladdru  6628  cauappcvgprlemladdrl  6629  cauappcvgprlem1  6631  cauappcvgprlem2  6632  cauappcvgprlemlim  6633  cauappcvgpr  6634  caucvgprlemnkj  6637  caucvgprlemnbj  6638  caucvgprlemm  6639  caucvgprlemopl  6640  caucvgprlemlol  6641  caucvgprlemdisj  6645  caucvgprlemloc  6646  caucvgprlemcl  6647  caucvgprlemladdfu  6648  caucvgprlemladdrl  6649  caucvgprlem1  6650  caucvgprlem2  6651  caucvgpr  6653  ltsosr  6692  ltasrg  6698  addgt0sr  6703  mulextsr1  6707  pitonnlem2  6743  pitonn  6744  axpre-ltadd  6770  axpre-mulext  6772  ltsubadd  7222  lesubadd  7224  ltaddsub2  7227  leaddsub2  7229  ltaddpos  7242  lesub2  7247  ltsub2  7249  ltnegcon2  7254  lenegcon2  7257  addge01  7262  subge0  7265  suble0  7266  lesub0  7269  apreap  7371  divap0b  7444  mulgt1  7610  ltmulgt11  7611  gt0div  7617  ge0div  7618  ltmuldiv  7621  ltmuldiv2  7622  lemuldiv2  7629  ltrec  7630  lerec2  7636  ltdiv23  7639  lediv23  7640  addltmul  7938  avglt1  7940  avgle1  7942  ztri3or  8064  zlem1lt  8076  zgt0ge1  8078  qapne  8350  xrltso  8487  xltnegi  8518  nn0disj  8765  frec2uzf1od  8873  expivallem  8910  expap0  8939  leexp2r  8962
  Copyright terms: Public domain W3C validator