MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  breq2d Unicode version

Theorem breq2d 4035
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 4027 . 2  |-  ( A  =  B  ->  ( C R A  <->  C R B ) )
31, 2syl 15 1  |-  ( ph  ->  ( C R A  <-> 
C R B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    = wceq 1623   class class class wbr 4023
This theorem is referenced by:  breqtrd  4047  sbcbr1g  4074  pofun  4330  csbfv12g  5535  isorel  5823  soisores  5824  soisoi  5825  isocnv  5827  isotr  5833  f1owe  5850  f1oweALT  5851  caovordig  6025  caovordg  6027  caovord  6031  frxp  6225  xporderlem  6226  fnwelem  6230  th3qlem2  6765  difsnen  6944  domdifsn  6945  unfilem3  7123  domunfican  7129  marypha1lem  7186  marypha1  7187  r1sdom  7446  sdomsdomcardi  7604  alephordi  7701  pwcdadom  7842  sornom  7903  axdclem  8146  pwcfsdom  8205  elgch  8244  winalim2  8318  rankcf  8399  inatsk  8400  pinq  8551  nqereu  8553  ltaddnq  8598  ltrnq  8603  archnq  8604  addclprlem1  8640  mulclprlem  8643  1idpr  8653  ltaprlem  8668  ltapr  8669  prlem936  8671  ltasr  8722  mulgt0sr  8727  sqgt0sr  8728  map2psrpr  8732  axpre-ltadd  8789  axpre-mulgt0  8790  axpre-sup  8791  ltsubadd2  9245  lesubadd2  9247  ltaddpos2  9265  posdif  9267  lesub1  9268  ltnegcon1  9275  lenegcon1  9278  addge02  9285  mulge0  9291  msqge0  9295  ltordlem  9298  prodgt0  9601  prodgt02  9602  prodge02  9604  ltmulgt12  9617  lemulge12  9619  ltdivmul  9628  ledivmul  9629  ledivmulOLD  9630  ltdivmul2  9631  lt2mul2div  9632  ledivmul2  9633  ledivmul2OLD  9634  ltrec  9637  ltrec1  9643  ltdiv23  9647  lediv23  9648  nnge1  9772  halfpos  9942  lt2halves  9946  addltmul  9947  avglt2  9950  avgle2  9952  nnrecl  9963  zltlem1  10070  gtndiv  10089  rebtwnz  10315  xrmax1  10504  max1ALT  10515  qbtwnre  10526  xralrple  10532  xltnegi  10543  xmulval  10552  xsubge0  10581  xposdif  10582  xlesubadd  10583  fllelt  10929  flbi  10946  btwnzge0  10953  om2uzlti  11013  monoord  11076  sermono  11078  expval  11106  expnbnd  11230  discr1  11237  discr  11238  facwordi  11302  seqcoll  11401  seqcoll2  11402  cnpart  11725  sqrlem6  11733  sqrmo  11737  resqreu  11738  resqrcl  11739  resqrthlem  11740  sqrneg  11753  sqreulem  11843  sqreu  11844  sqrthlem  11846  eqsqrd  11851  limsuple  11952  rlimcld2  12052  rlimrege0  12053  o1compt  12061  climserle  12136  caurcvgr  12146  fsum00  12256  fsumabs  12259  climcndslem2  12309  climcnds  12310  supcvg  12314  georeclim  12328  geoisumr  12334  cvgrat  12339  sin01bnd  12465  cos01bnd  12466  ruclem1  12509  ruclem9  12516  ruclem12  12519  dvdsaddr  12568  dvdssub  12569  dvdssubr  12570  dvdsfac  12583  dvdsmod  12585  oddp1even  12589  divalglem0  12592  divalglem2  12594  divalglem4  12595  divalglem5  12596  divalglem9  12600  divalg  12602  divalg2  12604  divalgmod  12605  ndvdssub  12606  ndvdsadd  12607  bitsfval  12614  bitsval  12615  bits0  12619  bitsp1  12622  bitsfzolem  12625  bitsfzo  12626  bitscmp  12629  bitsinv1lem  12632  bitsshft  12666  gcdcllem1  12690  dvdslegcd  12695  bezoutlem4  12720  dvdssqim  12732  dvdsmulgcd  12733  dvdssq  12739  nn0seqcvgd  12740  coprmdvds  12781  coprmdvds2  12782  isprm6  12788  prmdvdsexp  12793  prmdvdsexpr  12795  prmfac1  12797  divgcdodd  12798  rpmul  12802  hashdvds  12843  phiprmpw  12844  eulerthlem2  12850  prmdiv  12853  prmdiveq  12854  odzval  12856  odzcllem  12857  odzdvds  12860  opoe  12864  omoe  12865  pythagtriplem11  12878  pythagtriplem13  12880  pythagtrip  12887  pceulem  12898  pczndvds2  12919  pcdvdsb  12921  pc2dvds  12931  pcz  12933  pcprmpw2  12934  pcaddlem  12936  pcmpt  12940  prmpwdvds  12951  pockthlem  12952  prmreclem2  12964  prmreclem4  12966  4sqlem11  13002  vdwlem9  13036  rami  13062  ramlb  13066  0ram  13067  ramz2  13071  ramub1lem1  13073  imasleval  13443  subsubc  13727  pospo  14107  mulgval  14569  oddvdsnn0  14859  odmulg  14869  pgpfi1  14906  pgpfi  14916  slwispgp  14922  pgpssslw  14925  subgslw  14927  sylow2alem2  14929  sylow2blem3  14933  fislw  14936  efgi  15028  efgval2  15033  efgsrel  15043  efgredlemb  15055  lt6abl  15181  dprdval  15238  dprd2dlem2  15275  dprd2da  15277  dprd2d2  15279  ablfacrplem  15300  ablfac1a  15304  ablfac1b  15305  ablfac1eulem  15307  ablfac1eu  15308  pgpfac1lem3a  15311  ablfaclem3  15322  dvdsrtr  15434  dvdsrmul1  15435  unitpropd  15479  isabvd  15585  zndvds0  16504  znunit  16517  cygth  16525  hmphindis  17488  ordthmeolem  17492  ismet2  17898  xmettri2  17905  imasdsf1olem  17937  imasf1oxmet  17939  comet  18059  stdbdxmet  18061  nmogelb  18225  nmolb  18226  metdsge  18353  metdseq0  18358  iihalf2  18431  bndth  18456  evth  18457  ipcau2  18664  tchcphlem1  18665  tchcphlem2  18666  iscau3  18704  iscmet3  18719  bcthlem1  18746  bcth  18751  minveclem3b  18792  minveclem3  18793  minveclem4  18796  minveclem5  18797  pjthlem1  18801  pjthlem2  18802  pmltpclem1  18808  pmltpc  18810  ivthlem2  18812  ivthlem3  18813  ovolgelb  18839  ovolunlem1  18856  ovoliunlem2  18862  ovolshftlem1  18868  ovolscalem1  18872  ovolicc1  18875  ovolicc2lem3  18878  ioombl1lem4  18918  mbfmulc2lem  19002  mbfposb  19008  mbfaddlem  19015  mbfsup  19019  mbfinf  19020  mbflimsup  19021  i1fposd  19062  itg1ge0a  19066  mbfi1fseqlem4  19073  mbfi1fseqlem6  19075  mbfi1flimlem  19077  mbfi1flim  19078  itg2const2  19096  itg2seq  19097  itg2monolem1  19105  itg2i1fseq  19110  itg2addlem  19113  ibllem  19119  isibl  19120  isibl2  19121  iblitg  19123  dfitg  19124  cbvitg  19130  itgeq2  19132  itgvallem  19139  iblneg  19157  itgneg  19158  itggt0  19196  dvlip  19340  c1lip1  19344  dvfsumle  19368  dvfsumlem2  19374  dvfsumlem4  19376  dvfsum2  19381  mdeglt  19451  degltp1le  19459  deg1suble  19493  ply1divex  19522  plypf1  19594  dgrlb  19618  coemulc  19636  dgrsub  19653  quotval  19672  plydivlem4  19676  quotcan  19689  vieta1lem2  19691  aalioulem2  19713  aaliou3lem9  19730  ulmcn  19776  dvradcnv  19797  sincosq1sgn  19866  sincosq2sgn  19867  sincosq4sgn  19869  logltb  19953  cxpge0  20030  cxple2  20044  logreclem  20116  jensen  20283  emcllem7  20295  wilthlem1  20306  ftalem2  20311  ftalem3  20312  ftalem7  20316  fta  20317  sgmval  20380  mumul  20419  dvdsppwf1o  20426  musum  20431  chtublem  20450  chtub  20451  perfect1  20467  bcmono  20516  bclbnd  20519  bposlem1  20523  bposlem5  20527  lgslem1  20535  lgsval  20539  lgsdilem  20561  lgsne0  20572  lgsqrlem2  20581  lgsqrlem4  20583  lgseisenlem1  20588  lgseisenlem2  20589  lgsquadlem1  20593  lgsquadlem2  20594  lgsquadlem3  20595  lgsquad2lem2  20598  m1lgs  20601  2sqlem4  20606  2sqlem8a  20610  2sqblem  20616  dchrisumlema  20637  dchrisumlem2  20639  dchrisumlem3  20640  chpdifbndlem2  20703  pntrsumbnd2  20716  pntpbnd1  20735  pntibndlem3  20741  pntlemi  20753  pntleme  20757  pntlem3  20758  pnt3  20761  ostth2lem2  20783  ostth3  20787  ostth  20788  nmounbseqi  21355  nmounbseqiOLD  21356  isblo3i  21379  blo3i  21380  blocnilem  21382  siilem2  21430  normlem6  21694  normgt0  21706  norm3dif  21729  norm3lemt  21731  pjhthlem1  21970  pjige0  22270  nmcexi  22606  lnconi  22613  lnopcnbd  22616  lnfncnbd  22637  riesz1  22645  cnlnadjlem2  22648  cnlnadjlem8  22654  leopg  22702  leop2  22704  leoppos  22706  leopadd  22712  leopmuli  22713  leopmul2i  22715  pjssge0i  22746  pjdifnormi  22747  pjssposi  22752  pjssdif1i  22755  chcv1  22935  cvexch  22954  atcvatlem  22965  atcvat3i  22976  atdmd  22978  cdj3i  23021  addltmulALT  23026  bcm1n  23032  ballotlemfc0  23051  ballotlemfcc  23052  ballotleme  23055  ballotlem4  23057  ballotlemic  23065  ballotlem1c  23066  ballotlemsval  23067  ballotlemieq  23075  itgeq12dv  23196  xlt2addrd  23253  xrofsup  23255  unitdivcld  23285  xrge0iifiso  23317  xrge0addgt0  23331  esumcvg  23454  measssd  23543  dya2ub  23575  prob01  23616  orvcval  23658  erdszelem8  23729  erdsze2lem2  23735  eupath2lem3  23903  eupath2  23904  konigsberg  23911  abs2sqle  24016  abs2sqlt  24017  divelunit  24080  mulge0b  24086  mulle0b  24087  pdivsq  24102  dvdspw  24103  poseq  24253  soseq  24254  sltval  24301  brbtwn2  24533  axlowdim2  24588  axlowdim  24589  axcontlem2  24593  axcontlem3  24594  axcontlem4  24595  axcontlem9  24600  axcontlem10  24601  axcontlem11  24602  axcontlem12  24603  cgrdegen  24627  brofs  24628  segconeu  24634  btwntriv2  24635  transportprops  24657  brifs  24666  ifscgr  24667  brcgr3  24669  cgrxfr  24678  brcolinear2  24681  colineardim1  24684  brfs  24702  idinside  24707  btwnconn1lem11  24720  btwnconn1lem12  24721  btwnconn1lem14  24723  brsegle  24731  seglerflx  24735  seglemin  24736  segleantisym  24738  btwnsegle  24740  outsideofeu  24754  outsidele  24755  fvray  24764  dvreasin  24923  areacirclem2  24925  areacirclem5  24929  areacirclem6  24930  areacirc  24931  oriso  25214  geme2  25275  iintlem1  25610  isibcg  26191  nn0prpwlem  26238  nn0prpw  26239  seqpo  26457  incsequz2  26459  mettrifi  26473  heibor1lem  26533  rrncmslem  26556  elpell1qr2  26957  monotuz  27026  monotoddzzfi  27027  monotoddzz  27028  oddcomabszz  27029  rmxypos  27034  mzpcong  27059  congrep  27060  acongsym  27063  acongneg2  27064  acongtr  27065  acongeq12d  27066  dvdsabsmod0  27079  divalgmodcl  27080  jm2.18  27081  jm2.19lem2  27083  jm2.19lem3  27084  jm2.19lem4  27085  jm2.19  27086  jm2.25  27092  jm2.15nn0  27096  jm2.16nn0  27097  jm2.27  27101  rmydioph  27107  expdiophlem1  27114  expdiophlem2  27115  fnwe2lem2  27148  lmisfree  27312  evth2f  27686  evthf  27698  rfcnpre3  27704  fmul01  27710  fmul01lt1lem1  27714  climinf  27732  climinff  27737  stoweidlem3  27752  stoweidlem7  27756  stoweidlem13  27762  stoweidlem15  27764  stoweidlem16  27765  stoweidlem18  27767  stoweidlem24  27773  stoweidlem26  27775  stoweidlem27  27776  stoweidlem28  27777  stoweidlem31  27780  stoweidlem34  27783  stoweidlem36  27785  stoweidlem37  27786  stoweidlem41  27790  stoweidlem44  27793  stoweidlem45  27794  stoweidlem46  27795  stoweidlem48  27797  stoweidlem51  27800  stoweidlem55  27804  stoweidlem59  27808  stoweidlem60  27809  stoweidlem62  27811  lsatcv0eq  29237  oposlem  29373  oplecon1b  29391  opltcon1b  29395  atlatmstc  29509  cvlexch1  29518  cvlexch2  29519  cvlexchb2  29521  cvlatexchb2  29525  cvlatexch2  29527  cvlatcvr2  29532  cvlsupr2  29533  ishlat1  29542  hlsuprexch  29570  cvrexch  29609  cvrat  29611  atcvr0eq  29615  atcvrj0  29617  atltcvr  29624  cvrat3  29631  cvrat4  29632  cvrat42  29633  3noncolr2  29638  hlatcon2  29641  4noncolr3  29642  3dimlem1  29647  3dimlem2  29648  3dimlem3a  29649  3dimlem3  29650  3dimlem3OLDN  29651  3dimlem4a  29652  3dimlem4  29653  3dimlem4OLDN  29654  3dim1lem5  29655  3dim2  29657  3dim3  29658  ps-1  29666  ps-2  29667  3atlem5  29676  3atlem6  29677  lplni2  29726  lplnnle2at  29730  lplnnleat  29731  lplnnlelln  29732  lplnribN  29740  lplnexllnN  29753  lvoli2  29770  lvolnle3at  29771  lvolnleat  29772  lvolnlelln  29773  lvolnlelpln  29774  4atlem9  29792  4atlem10a  29793  4atlem11a  29796  4atlem11  29798  4atlem12a  29799  dalempnes  29840  dalemqnet  29841  dalem1  29848  dalemswapyzps  29879  dalemrotps  29880  dalem30  29891  dalem35  29896  lineset  29927  islinei  29929  psubspset  29933  psubspi2N  29937  snatpsubN  29939  2llnma1  29976  elpaddn0  29989  elpaddri  29991  elpaddat  29993  elpadd2at  29995  paddcom  30002  paddasslem12  30020  pmapjat1  30042  llnexchb2  30058  lhp2at0nle  30224  lhprelat3N  30229  4atexlemswapqr  30252  4atexlemcnd  30261  lautle  30273  lautcvr  30281  ltrnel  30328  ltrneq2  30337  trlnle  30375  cdlemc3  30382  cdlemd6  30392  cdleme3  30426  cdleme7aa  30431  cdleme7  30438  cdleme11c  30450  cdleme15c  30465  cdleme20y  30491  cdleme20m  30512  cdleme21b  30515  cdleme21c  30516  cdleme21at  30517  cdleme36a  30649  cdleme43bN  30679  cdleme43dN  30681  cdleme46f2g2  30682  cdleme46f2g1  30683  cdlemeg46c  30702  cdlemeg46nlpq  30706  cdlemb3  30795  cdlemg4d  30802  cdlemg6d  30810  cdlemg10c  30828  cdlemg12  30839  cdlemg27b  30885  djhcvat42  31605
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-rab 2552  df-v 2790  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-br 4024
  Copyright terms: Public domain W3C validator