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

Theorem breq2d 3776
Description: Equality deduction for a binary relation. (Contributed by NM, 8-Feb-1996.)
Hypothesis
Ref Expression
breq1d.1  |-  ( ph  ->  A  =  B )
Assertion
Ref Expression
breq2d  |-  ( ph  ->  ( C R A  <-> 
C R B ) )

Proof of Theorem breq2d
StepHypRef Expression
1 breq1d.1 . 2  |-  ( ph  ->  A  =  B )
2 breq2 3768 . 2  |-  ( A  =  B  ->  ( C R A  <->  C R B ) )
31, 2syl 14 1  |-  ( ph  ->  ( C R A  <-> 
C R B ) )
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:  breqtrd  3788  sbcbr1g  3815  pofun  4049  csbfv12g  5209  isorel  5448  isocnv  5451  isotr  5456  caovordig  5666  caovordg  5668  caovord  5672  xporderlem  5852  th3qlem2  6209  phplem3g  6319  enqdc1  6458  ltanqg  6496  ltmnqg  6497  archnqq  6513  prarloclemarch2  6515  prloc  6587  addnqprllem  6623  addlocprlemgt  6630  appdivnq  6659  mulnqprl  6664  1idprl  6686  ltexprlemloc  6703  caucvgprlemcanl  6740  cauappcvgprlemm  6741  cauappcvgprlemladdru  6752  cauappcvgprlemladdrl  6753  cauappcvgprlem1  6755  cauappcvgprlemlim  6757  cauappcvgpr  6758  archrecnq  6759  caucvgprlemnkj  6762  caucvgprlemnbj  6763  caucvgprlemm  6764  caucvgprlemcl  6772  caucvgprlemladdrl  6774  caucvgpr  6778  caucvgprprlemell  6781  caucvgprprlemelu  6782  caucvgprprlemcbv  6783  caucvgprprlemval  6784  caucvgprprlemnkeqj  6786  caucvgprprlemml  6790  caucvgprprlemmu  6791  caucvgprprlemopl  6793  caucvgprprlemlol  6794  caucvgprprlemopu  6795  caucvgprprlemloc  6799  caucvgprprlemclphr  6801  caucvgprprlemexbt  6802  caucvgprprlem1  6805  caucvgprprlem2  6806  caucvgprpr  6808  ltposr  6846  ltasrg  6853  mulgt0sr  6860  mulextsr1lem  6862  mulextsr1  6863  prsrlt  6869  caucvgsrlemcl  6871  caucvgsrlemfv  6873  caucvgsrlembound  6876  caucvgsrlemgt1  6877  caucvgsrlemoffres  6882  caucvgsr  6884  pitonnlem2  6921  pitonn  6922  recidpipr  6930  axpre-ltadd  6958  axpre-mulgt0  6959  axpre-mulext  6960  axarch  6963  nntopi  6966  axcaucvglemval  6969  axcaucvglemcau  6970  axcaucvglemres  6971  ltsubadd2  7426  lesubadd2  7428  ltaddsub  7429  leaddsub  7431  ltaddpos2  7446  posdif  7448  lesub1  7449  ltsub1  7451  ltnegcon1  7456  lenegcon1  7459  addge02  7466  leaddle0  7470  possumd  7558  sublt0d  7559  apreap  7576  prodgt02  7817  prodge02  7819  ltmulgt12  7829  lemulge12  7831  ltdivmul  7840  ledivmul  7841  ltdivmul2  7842  lt2mul2div  7843  ledivmul2  7844  ltrec  7847  ltrec1  7852  ltdiv23  7856  lediv23  7857  nnge1  7935  halfpos  8154  lt2halves  8158  addltmul  8159  avglt2  8162  avgle2  8164  nnrecl  8177  zltlem1  8299  gtndiv  8333  qapne  8572  xltnegi  8746  divelunit  8868  eluzgtdifelfzo  9051  qtri3or  9096  qbtwnzlemstep  9101  qbtwnzlemshrink  9102  qbtwnzlemex  9103  qbtwnz  9104  rebtwn2zlemstep  9105  rebtwn2zlemshrink  9106  rebtwn2z  9107  flqlelt  9116  flqbi  9130  2tnp1ge0ge0  9141  frec2uzltd  9163  frec2uzlt2d  9164  frec2uzf1od  9166  monoord  9209  isermono  9211  expnbnd  9346  caucvgrelemcau  9553  caucvgre  9554  cvg1nlemcau  9557  cvg1nlemres  9558  recvguniq  9567  resqrexlemover  9582  resqrexlemgt0  9592  resqrexlemoverl  9593  resqrexlemglsq  9594  resqrexlemsqa  9596  resqrexlemex  9597  climserile  9838  nn0seqcvgd  9853
  Copyright terms: Public domain W3C validator