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

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

Proof of Theorem breq2d
StepHypRef Expression
1 breq1d.1 . 2 (𝜑𝐴 = 𝐵)
2 breq2 3797 . 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:  breqtrd  3817  sbcbr1g  3844  pofun  4075  csbfv12g  5241  isorel  5479  isocnv  5482  isotr  5487  caovordig  5697  caovordg  5699  caovord  5703  xporderlem  5883  th3qlem2  6275  phplem3g  6391  supsnti  6477  inflbti  6496  enqdc1  6614  ltanqg  6652  ltmnqg  6653  archnqq  6669  prarloclemarch2  6671  prloc  6743  addnqprllem  6779  addlocprlemgt  6786  appdivnq  6815  mulnqprl  6820  1idprl  6842  ltexprlemloc  6859  caucvgprlemcanl  6896  cauappcvgprlemm  6897  cauappcvgprlemladdru  6908  cauappcvgprlemladdrl  6909  cauappcvgprlem1  6911  cauappcvgprlemlim  6913  cauappcvgpr  6914  archrecnq  6915  caucvgprlemnkj  6918  caucvgprlemnbj  6919  caucvgprlemm  6920  caucvgprlemcl  6928  caucvgprlemladdrl  6930  caucvgpr  6934  caucvgprprlemell  6937  caucvgprprlemelu  6938  caucvgprprlemcbv  6939  caucvgprprlemval  6940  caucvgprprlemnkeqj  6942  caucvgprprlemml  6946  caucvgprprlemmu  6947  caucvgprprlemopl  6949  caucvgprprlemlol  6950  caucvgprprlemopu  6951  caucvgprprlemloc  6955  caucvgprprlemclphr  6957  caucvgprprlemexbt  6958  caucvgprprlem1  6961  caucvgprprlem2  6962  caucvgprpr  6964  ltposr  7002  ltasrg  7009  mulgt0sr  7016  mulextsr1lem  7018  mulextsr1  7019  prsrlt  7025  caucvgsrlemcl  7027  caucvgsrlemfv  7029  caucvgsrlembound  7032  caucvgsrlemgt1  7033  caucvgsrlemoffres  7038  caucvgsr  7040  pitonnlem2  7077  pitonn  7078  recidpipr  7086  axpre-ltadd  7114  axpre-mulgt0  7115  axpre-mulext  7116  axarch  7119  nntopi  7122  axcaucvglemval  7125  axcaucvglemcau  7126  axcaucvglemres  7127  ltaddneg  7595  ltsubadd2  7604  lesubadd2  7606  ltaddsub  7607  leaddsub  7609  ltaddpos2  7624  posdif  7626  lesub1  7627  ltsub1  7629  ltnegcon1  7634  lenegcon1  7637  addge02  7644  leaddle0  7648  possumd  7736  sublt0d  7737  apreap  7754  prodgt02  7998  prodge02  8000  ltmulgt12  8010  lemulge12  8012  ltdivmul  8021  ledivmul  8022  ltdivmul2  8023  lt2mul2div  8024  ledivmul2  8025  ltrec  8028  ltrec1  8033  ltdiv23  8037  lediv23  8038  nnge1  8129  halfpos  8329  lt2halves  8333  addltmul  8334  avglt2  8337  avgle2  8339  nnrecl  8353  zltlem1  8489  gtndiv  8523  qapne  8805  nnledivrp  8918  xltnegi  8978  divelunit  9100  eluzgtdifelfzo  9283  qtri3or  9329  exbtwnzlemstep  9334  exbtwnzlemshrink  9335  exbtwnzlemex  9336  exbtwnz  9337  rebtwn2zlemstep  9339  rebtwn2zlemshrink  9340  rebtwn2z  9341  flqlelt  9358  flqbi  9372  2tnp1ge0ge0  9383  q2submod  9467  frec2uzltd  9485  frec2uzlt2d  9486  frec2uzf1od  9488  monoord  9551  isermono  9553  expnbnd  9693  facwordi  9764  sizeunlem  9828  caucvgrelemcau  10004  caucvgre  10005  cvg1nlemcau  10008  cvg1nlemres  10009  recvguniq  10019  resqrexlemover  10034  resqrexlemgt0  10044  resqrexlemoverl  10045  resqrexlemglsq  10046  resqrexlemsqa  10048  resqrexlemex  10049  maxleastlt  10239  minmax  10250  lemininf  10253  ltmininf  10254  climserile  10321  summodnegmod  10371  modmulconst  10372  dvdsaddr  10384  dvdssub  10385  dvdssubr  10386  dvdslelemd  10388  dvdsfac  10405  dvdsmod  10407  oddp1even  10420  ltoddhalfle  10437  opoe  10439  omoe  10440  divalg2  10470  divalgmod  10471  ndvdssub  10474  ndvdsadd  10475  bezoutlembi  10538  dvdssqim  10557  dvdsmulgcd  10558  dvdssq  10564  nn0seqcvgd  10567  coprmdvds  10618  coprmdvds2  10619  rpmul  10624  cncongr1  10629  divgcdodd  10666  isprm6  10670  prmdvdsexp  10671  prmdvdsexpr  10673  prmfac1  10675  oddpwdclemxy  10691  oddpwdclemodd  10694  sqpweven  10697  2sqpwodd  10698  sqne2sq  10699
  Copyright terms: Public domain W3C validator