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

Theorem breq1d 3765
Description: Equality deduction for a binary relation. (Contributed by NM, 8-Feb-1996.)
Hypothesis
Ref Expression
breq1d.1 (φA = B)
Assertion
Ref Expression
breq1d (φ → (A𝑅𝐶B𝑅𝐶))

Proof of Theorem breq1d
StepHypRef Expression
1 breq1d.1 . 2 (φA = B)
2 breq1 3758 . 2 (A = B → (A𝑅𝐶B𝑅𝐶))
31, 2syl 14 1 (φ → (A𝑅𝐶B𝑅𝐶))
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-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:  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  6473  addnqprulem  6510  appdivnq  6543  mulnqpru  6549  mullocprlem  6550  1idpru  6566  cauappcvgprlemm  6616  cauappcvgprlemopl  6617  cauappcvgprlemlol  6618  cauappcvgprlemdisj  6622  cauappcvgprlemloc  6623  cauappcvgprlemladdfl  6626  cauappcvgprlemladdru  6627  cauappcvgprlemladdrl  6628  cauappcvgprlem1  6630  cauappcvgprlem2  6631  cauappcvgprlemlim  6632  cauappcvgpr  6633  ltsosr  6672  ltasrg  6678  addgt0sr  6683  mulextsr1  6687  pitonnlem2  6723  pitonn  6724  axpre-ltadd  6750  axpre-mulext  6752  ltsubadd  7202  lesubadd  7204  ltaddsub2  7207  leaddsub2  7209  ltaddpos  7222  lesub2  7227  ltsub2  7229  ltnegcon2  7234  lenegcon2  7237  addge01  7242  subge0  7245  suble0  7246  lesub0  7249  apreap  7351  divap0b  7424  mulgt1  7590  ltmulgt11  7591  gt0div  7597  ge0div  7598  ltmuldiv  7601  ltmuldiv2  7602  lemuldiv2  7609  ltrec  7610  lerec2  7616  ltdiv23  7619  lediv23  7620  addltmul  7918  avglt1  7920  avgle1  7922  ztri3or  8044  zlem1lt  8056  zgt0ge1  8058  qapne  8330  xrltso  8467  xltnegi  8498  nn0disj  8745  frec2uzf1od  8853  expivallem  8890  expap0  8919  leexp2r  8942
  Copyright terms: Public domain W3C validator