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

Theorem breq2d 3849
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 3841 . 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 103    = wceq 1289   class class class wbr 3837
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 665  ax-5 1381  ax-7 1382  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-8 1440  ax-10 1441  ax-11 1442  ax-i12 1443  ax-bndl 1444  ax-4 1445  ax-17 1464  ax-i9 1468  ax-ial 1472  ax-i5r 1473  ax-ext 2070
This theorem depends on definitions:  df-bi 115  df-3an 926  df-tru 1292  df-nf 1395  df-sb 1693  df-clab 2075  df-cleq 2081  df-clel 2084  df-nfc 2217  df-v 2621  df-un 3001  df-sn 3447  df-pr 3448  df-op 3450  df-br 3838
This theorem is referenced by:  breqtrd  3861  sbcbr1g  3888  pofun  4130  csbfv12g  5324  isorel  5569  isocnv  5572  isotr  5577  caovordig  5792  caovordg  5794  caovord  5798  xporderlem  5978  th3qlem2  6375  phplem3g  6552  supsnti  6679  inflbti  6698  enqdc1  6900  ltanqg  6938  ltmnqg  6939  archnqq  6955  prarloclemarch2  6957  prloc  7029  addnqprllem  7065  addlocprlemgt  7072  appdivnq  7101  mulnqprl  7106  1idprl  7128  ltexprlemloc  7145  caucvgprlemcanl  7182  cauappcvgprlemm  7183  cauappcvgprlemladdru  7194  cauappcvgprlemladdrl  7195  cauappcvgprlem1  7197  cauappcvgprlemlim  7199  cauappcvgpr  7200  archrecnq  7201  caucvgprlemnkj  7204  caucvgprlemnbj  7205  caucvgprlemm  7206  caucvgprlemcl  7214  caucvgprlemladdrl  7216  caucvgpr  7220  caucvgprprlemell  7223  caucvgprprlemelu  7224  caucvgprprlemcbv  7225  caucvgprprlemval  7226  caucvgprprlemnkeqj  7228  caucvgprprlemml  7232  caucvgprprlemmu  7233  caucvgprprlemopl  7235  caucvgprprlemlol  7236  caucvgprprlemopu  7237  caucvgprprlemloc  7241  caucvgprprlemclphr  7243  caucvgprprlemexbt  7244  caucvgprprlem1  7247  caucvgprprlem2  7248  caucvgprpr  7250  ltposr  7288  ltasrg  7295  mulgt0sr  7302  mulextsr1lem  7304  mulextsr1  7305  prsrlt  7311  caucvgsrlemcl  7313  caucvgsrlemfv  7315  caucvgsrlembound  7318  caucvgsrlemgt1  7319  caucvgsrlemoffres  7324  caucvgsr  7326  pitonnlem2  7363  pitonn  7364  recidpipr  7372  axpre-ltadd  7400  axpre-mulgt0  7401  axpre-mulext  7402  axarch  7405  nntopi  7408  axcaucvglemval  7411  axcaucvglemcau  7412  axcaucvglemres  7413  ltaddneg  7881  ltsubadd2  7890  lesubadd2  7892  ltaddsub  7893  leaddsub  7895  ltaddpos2  7910  posdif  7912  lesub1  7913  ltsub1  7915  ltnegcon1  7920  lenegcon1  7923  addge02  7930  leaddle0  7934  possumd  8022  sublt0d  8023  apreap  8040  prodgt02  8286  prodge02  8288  ltmulgt12  8298  lemulge12  8300  ltdivmul  8309  ledivmul  8310  ltdivmul2  8311  lt2mul2div  8312  ledivmul2  8313  ltrec  8316  ltrec1  8321  ltdiv23  8325  lediv23  8326  nnge1  8417  halfpos  8617  lt2halves  8621  addltmul  8622  avglt2  8625  avgle2  8627  nnrecl  8641  zltlem1  8777  gtndiv  8811  qapne  9093  nnledivrp  9206  xltnegi  9266  divelunit  9388  eluzgtdifelfzo  9573  qtri3or  9619  exbtwnzlemstep  9624  exbtwnzlemshrink  9625  exbtwnzlemex  9626  exbtwnz  9627  rebtwn2zlemstep  9629  rebtwn2zlemshrink  9630  rebtwn2z  9631  flqlelt  9648  flqbi  9662  2tnp1ge0ge0  9673  q2submod  9757  frec2uzltd  9775  frec2uzlt2d  9776  frec2uzf1od  9778  monoord  9869  isermono  9871  ser3ge0  9917  expnbnd  10042  facwordi  10113  hashunlem  10177  zfz1isolemiso  10209  iseqcoll  10212  caucvgrelemcau  10378  caucvgre  10379  cvg1nlemcau  10382  cvg1nlemres  10383  recvguniq  10393  resqrexlemover  10408  resqrexlemgt0  10418  resqrexlemoverl  10419  resqrexlemglsq  10420  resqrexlemsqa  10422  resqrexlemex  10423  maxleastlt  10613  minmax  10625  lemininf  10628  ltmininf  10629  climserle  10698  isummolem3  10734  isummolem2a  10735  isummo  10737  zisum  10738  fisum  10742  fsum00  10819  fsumabs  10822  cvgratnnlemnexp  10879  cvgratnnlemmn  10880  summodnegmod  10920  modmulconst  10921  dvdsaddr  10933  dvdssub  10934  dvdssubr  10935  dvdslelemd  10937  dvdsfac  10954  dvdsmod  10956  oddp1even  10969  ltoddhalfle  10986  opoe  10988  omoe  10989  divalg2  11019  divalgmod  11020  ndvdssub  11023  ndvdsadd  11024  bezoutlembi  11087  dvdssqim  11106  dvdsmulgcd  11107  dvdssq  11113  nn0seqcvgd  11116  coprmdvds  11167  coprmdvds2  11168  rpmul  11173  cncongr1  11178  divgcdodd  11215  isprm6  11219  prmdvdsexp  11220  prmdvdsexpr  11222  prmfac1  11224  oddpwdclemxy  11240  oddpwdclemodd  11243  sqpweven  11246  2sqpwodd  11247  sqne2sq  11248  hashdvds  11290  phiprmpw  11291
  Copyright terms: Public domain W3C validator