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

Theorem breq1d 3774
Description: Equality deduction for a binary relation. (Contributed by NM, 8-Feb-1996.)
Hypothesis
Ref Expression
breq1d.1 (𝜑𝐴 = 𝐵)
Assertion
Ref Expression
breq1d (𝜑 → (𝐴𝑅𝐶𝐵𝑅𝐶))

Proof of Theorem breq1d
StepHypRef Expression
1 breq1d.1 . 2 (𝜑𝐴 = 𝐵)
2 breq1 3767 . 2 (𝐴 = 𝐵 → (𝐴𝑅𝐶𝐵𝑅𝐶))
31, 2syl 14 1 (𝜑 → (𝐴𝑅𝐶𝐵𝑅𝐶))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 98   = wceq 1243   class class class wbr 3764
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 630  ax-5 1336  ax-7 1337  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-10 1396  ax-11 1397  ax-i12 1398  ax-bndl 1399  ax-4 1400  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-i5r 1428  ax-ext 2022
This theorem depends on definitions:  df-bi 110  df-3an 887  df-tru 1246  df-nf 1350  df-sb 1646  df-clab 2027  df-cleq 2033  df-clel 2036  df-nfc 2167  df-v 2559  df-un 2922  df-sn 3381  df-pr 3382  df-op 3384  df-br 3765
This theorem is referenced by:  eqbrtrd  3784  syl6eqbr  3801  sbcbr2g  3816  pofun  4049  fmptco  5330  isorel  5448  isocnv  5451  isotr  5456  caovordig  5666  caovordg  5668  caovord  5672  xporderlem  5852  reldmtpos  5868  brtposg  5869  tpostpos  5879  tposoprab  5895  th3qlem2  6209  ensn1g  6277  fndmeng  6289  xpsneng  6296  xpcomco  6300  snnen2oprc  6323  ltsonq  6496  ltanqg  6498  ltmnqg  6499  archnqq  6515  prloc  6589  addnqprulem  6626  appdivnq  6661  mulnqpru  6667  mullocprlem  6668  1idpru  6689  cauappcvgprlemm  6743  cauappcvgprlemopl  6744  cauappcvgprlemlol  6745  cauappcvgprlemdisj  6749  cauappcvgprlemloc  6750  cauappcvgprlemladdfl  6753  cauappcvgprlemladdru  6754  cauappcvgprlemladdrl  6755  cauappcvgprlem1  6757  cauappcvgprlem2  6758  cauappcvgprlemlim  6759  cauappcvgpr  6760  caucvgprlemnkj  6764  caucvgprlemnbj  6765  caucvgprlemm  6766  caucvgprlemopl  6767  caucvgprlemlol  6768  caucvgprlemdisj  6772  caucvgprlemloc  6773  caucvgprlemcl  6774  caucvgprlemladdfu  6775  caucvgprlemladdrl  6776  caucvgprlem1  6777  caucvgprlem2  6778  caucvgpr  6780  caucvgprprlemell  6783  caucvgprprlemelu  6784  caucvgprprlemcbv  6785  caucvgprprlemval  6786  caucvgprprlemnkltj  6787  caucvgprprlemnkeqj  6788  caucvgprprlemnbj  6791  caucvgprprlemml  6792  caucvgprprlemmu  6793  caucvgprprlemopl  6795  caucvgprprlemlol  6796  caucvgprprlemopu  6797  caucvgprprlemloc  6801  caucvgprprlemclphr  6803  caucvgprprlemexbt  6804  caucvgprprlemexb  6805  caucvgprprlemaddq  6806  caucvgprprlem1  6807  caucvgprprlem2  6808  ltsosr  6849  ltasrg  6855  addgt0sr  6860  mulextsr1  6865  prsrlt  6871  caucvgsrlemgt1  6879  caucvgsrlemoffres  6884  caucvgsr  6886  pitonnlem2  6923  pitonn  6924  recidpipr  6932  axpre-ltadd  6960  axpre-mulext  6962  nntopi  6968  axcaucvglemval  6971  axcaucvglemcau  6972  axcaucvglemres  6973  ltsubadd  7427  lesubadd  7429  ltaddsub2  7432  leaddsub2  7434  ltaddpos  7447  lesub2  7452  ltsub2  7454  ltnegcon2  7459  lenegcon2  7462  addge01  7467  subge0  7470  suble0  7471  lesub0  7474  apreap  7578  divap0b  7662  mulgt1  7829  ltmulgt11  7830  gt0div  7836  ge0div  7837  ltmuldiv  7840  ltmuldiv2  7841  lemuldiv2  7848  ltrec  7849  lerec2  7855  ltdiv23  7858  lediv23  7859  addltmul  8161  avglt1  8163  avgle1  8165  div4p1lem1div2  8177  ztri3or  8288  zlem1lt  8300  zgt0ge1  8302  qapne  8574  divlt1lt  8650  divle1le  8651  xrltso  8717  xltnegi  8748  nn0disj  8995  frec2uzf1od  9192  expivallem  9256  expap0  9285  leexp2r  9308  sqap0  9320  shftfvalg  9419  shftfibg  9421  shftfval  9422  shftfib  9424  shftfn  9425  2shfti  9432  shftidt2  9433  caucvgre  9580  cvg1nlemcau  9583  cvg1nlemres  9584  resqrexlemdecn  9610  resqrexlemoverl  9619  resqrexlemglsq  9620  resqrexlemsqa  9622  resqrexlemex  9623  abs00ap  9660  absdiflt  9688  absdifle  9689  lenegsq  9691  cau3lem  9710  clim  9802  clim2  9804  clim0  9806  clim0c  9807  climi0  9810  climuni  9814  2clim  9822  climshftlemg  9823  climshft  9825  climabs0  9828  climcn1  9829  climcn2  9830  addcn2  9831  subcn2  9832  mulcn2  9833  climcau  9866  serif0  9871  sumeq1  9874  qdencn  10124
  Copyright terms: Public domain W3C validator