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

Theorem breq1d 3803
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 3796 . 2 (𝐴 = 𝐵 → (𝐴𝑅𝐶𝐵𝑅𝐶))
31, 2syl 14 1 (𝜑 → (𝐴𝑅𝐶𝐵𝑅𝐶))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 103   = wceq 1285   class class class wbr 3793
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 663  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2064
This theorem depends on definitions:  df-bi 115  df-3an 922  df-tru 1288  df-nf 1391  df-sb 1687  df-clab 2069  df-cleq 2075  df-clel 2078  df-nfc 2209  df-v 2604  df-un 2978  df-sn 3412  df-pr 3413  df-op 3415  df-br 3794
This theorem is referenced by:  eqbrtrd  3813  syl6eqbr  3830  sbcbr2g  3845  pofun  4075  fmptco  5362  isorel  5479  isocnv  5482  isotr  5487  caovordig  5697  caovordg  5699  caovord  5703  xporderlem  5883  reldmtpos  5902  brtposg  5903  tpostpos  5913  tposoprab  5929  th3qlem2  6275  ensn1g  6344  fndmeng  6357  xpsneng  6366  xpcomco  6370  snnen2oprc  6395  unsnfidcel  6441  pm54.43  6518  ltsonq  6650  ltanqg  6652  ltmnqg  6653  archnqq  6669  prloc  6743  addnqprulem  6780  appdivnq  6815  mulnqpru  6821  mullocprlem  6822  1idpru  6843  cauappcvgprlemm  6897  cauappcvgprlemopl  6898  cauappcvgprlemlol  6899  cauappcvgprlemdisj  6903  cauappcvgprlemloc  6904  cauappcvgprlemladdfl  6907  cauappcvgprlemladdru  6908  cauappcvgprlemladdrl  6909  cauappcvgprlem1  6911  cauappcvgprlem2  6912  cauappcvgprlemlim  6913  cauappcvgpr  6914  caucvgprlemnkj  6918  caucvgprlemnbj  6919  caucvgprlemm  6920  caucvgprlemopl  6921  caucvgprlemlol  6922  caucvgprlemdisj  6926  caucvgprlemloc  6927  caucvgprlemcl  6928  caucvgprlemladdfu  6929  caucvgprlemladdrl  6930  caucvgprlem1  6931  caucvgprlem2  6932  caucvgpr  6934  caucvgprprlemell  6937  caucvgprprlemelu  6938  caucvgprprlemcbv  6939  caucvgprprlemval  6940  caucvgprprlemnkltj  6941  caucvgprprlemnkeqj  6942  caucvgprprlemnbj  6945  caucvgprprlemml  6946  caucvgprprlemmu  6947  caucvgprprlemopl  6949  caucvgprprlemlol  6950  caucvgprprlemopu  6951  caucvgprprlemloc  6955  caucvgprprlemclphr  6957  caucvgprprlemexbt  6958  caucvgprprlemexb  6959  caucvgprprlemaddq  6960  caucvgprprlem1  6961  caucvgprprlem2  6962  ltsosr  7003  ltasrg  7009  addgt0sr  7014  mulextsr1  7019  prsrlt  7025  caucvgsrlemgt1  7033  caucvgsrlemoffres  7038  caucvgsr  7040  pitonnlem2  7077  pitonn  7078  recidpipr  7086  axpre-ltadd  7114  axpre-mulext  7116  nntopi  7122  axcaucvglemval  7125  axcaucvglemcau  7126  axcaucvglemres  7127  ltaddnegr  7596  ltsubadd  7603  lesubadd  7605  ltaddsub2  7608  leaddsub2  7610  ltaddpos  7623  lesub2  7628  ltsub2  7630  ltnegcon2  7635  lenegcon2  7638  addge01  7643  subge0  7646  suble0  7647  lesub0  7650  apreap  7754  divap0b  7838  mulgt1  8008  ltmulgt11  8009  gt0div  8015  ge0div  8016  ltmuldiv  8019  ltmuldiv2  8020  lemuldiv2  8027  ltrec  8028  lerec2  8034  ltdiv23  8037  lediv23  8038  addltmul  8334  avglt1  8336  avgle1  8338  div4p1lem1div2  8351  ztri3or  8475  zlem1lt  8488  zgt0ge1  8490  qapne  8805  divlt1lt  8882  divle1le  8883  xrltso  8947  xltnegi  8978  nn0disj  9225  qavgle  9345  frec2uzf1od  9488  expivallem  9574  expap0  9603  leexp2r  9627  sqap0  9639  nn0opthlem1d  9744  sizeennnuni  9803  sizeunlem  9828  shftfvalg  9844  shftfibg  9846  shftfval  9847  shftfib  9849  shftfn  9850  2shfti  9857  shftidt2  9858  caucvgre  10005  cvg1nlemcau  10008  cvg1nlemres  10009  resqrexlemdecn  10036  resqrexlemoverl  10045  resqrexlemglsq  10046  resqrexlemsqa  10048  resqrexlemex  10049  abs00ap  10086  absdiflt  10116  absdifle  10117  lenegsq  10119  cau3lem  10138  minmax  10250  clim  10258  clim2  10260  clim0  10262  clim0c  10263  climi0  10266  climuni  10270  2clim  10278  climshftlemg  10279  climshft  10281  climabs0  10284  climcn1  10285  climcn2  10286  addcn2  10287  subcn2  10288  mulcn2  10289  climcau  10322  serif0  10327  sumeq1  10330  sumeq2d  10334  sumeq2  10335  isumrb  10339  halfleoddlt  10438  gcddvds  10499  dvdssq  10564  lcmgcdlem  10603  lcmdvds  10605  isprm  10635  prmgt1  10657  isprm6  10670  pw2dvdslemn  10687  pw2dvdseu  10690  oddpwdclemxy  10691  oddpwdclemndvds  10693  oddpwdclemodd  10694  qdencn  10943
  Copyright terms: Public domain W3C validator