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

Theorem breq2d 4037
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 4029 . 2  |-  ( A  =  B  ->  ( C R A  <->  C R B ) )
31, 2syl 17 1  |-  ( ph  ->  ( C R A  <-> 
C R B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 6    <-> wb 178    = wceq 1624   class class class wbr 4025
This theorem is referenced by:  breqtrd  4049  sbcbr1g  4076  pofun  4330  isorel  5785  soisores  5786  soisoi  5787  isocnv  5789  isotr  5795  f1owe  5812  f1oweALT  5813  caovordig  5987  caovordg  5989  caovord  5993  frxp  6187  xporderlem  6188  fnwelem  6192  th3qlem2  6761  difsnen  6940  domdifsn  6941  unfilem3  7119  domunfican  7125  marypha1lem  7182  marypha1  7183  r1sdom  7442  sdomsdomcardi  7600  alephordi  7697  pwcdadom  7838  sornom  7899  axdclem  8142  pwcfsdom  8201  elgch  8240  winalim2  8314  rankcf  8395  inatsk  8396  pinq  8547  nqereu  8549  ltaddnq  8594  ltrnq  8599  archnq  8600  addclprlem1  8636  mulclprlem  8639  1idpr  8649  ltaprlem  8664  ltapr  8665  prlem936  8667  ltasr  8718  mulgt0sr  8723  sqgt0sr  8724  map2psrpr  8728  axpre-ltadd  8785  axpre-mulgt0  8786  axpre-sup  8787  ltsubadd2  9241  lesubadd2  9243  ltaddpos2  9261  posdif  9263  lesub1  9264  ltnegcon1  9271  lenegcon1  9274  addge02  9281  mulge0  9287  msqge0  9291  ltordlem  9294  prodgt0  9597  prodgt02  9598  prodge02  9600  ltmulgt12  9613  lemulge12  9615  ltdivmul  9624  ledivmul  9625  ledivmulOLD  9626  ltdivmul2  9627  lt2mul2div  9628  ledivmul2  9629  ledivmul2OLD  9630  ltrec  9633  ltrec1  9639  ltdiv23  9643  lediv23  9644  nnge1  9768  halfpos  9938  lt2halves  9942  addltmul  9943  avglt2  9946  avgle2  9948  nnrecl  9959  zltlem1  10066  gtndiv  10085  rebtwnz  10311  xrmax1  10499  max1ALT  10510  qbtwnre  10521  xralrple  10527  xltnegi  10538  xmulval  10547  xsubge0  10576  xposdif  10577  xlesubadd  10578  fllelt  10924  flbi  10941  btwnzge0  10948  om2uzlti  11008  monoord  11071  sermono  11073  expval  11101  expnbnd  11225  discr1  11232  discr  11233  facwordi  11297  seqcoll  11396  seqcoll2  11397  cnpart  11720  sqrlem6  11728  sqrmo  11732  resqreu  11733  resqrcl  11734  resqrthlem  11735  sqrneg  11748  sqreulem  11838  sqreu  11839  sqrthlem  11841  eqsqrd  11846  limsuple  11947  rlimcld2  12047  rlimrege0  12048  o1compt  12056  climserle  12131  caurcvgr  12141  fsum00  12251  fsumabs  12254  climcndslem2  12304  climcnds  12305  supcvg  12309  georeclim  12323  geoisumr  12329  cvgrat  12334  sin01bnd  12460  cos01bnd  12461  ruclem1  12504  ruclem9  12511  ruclem12  12514  dvdsaddr  12563  dvdssub  12564  dvdssubr  12565  dvdsfac  12578  dvdsmod  12580  oddp1even  12584  divalglem0  12587  divalglem2  12589  divalglem4  12590  divalglem5  12591  divalglem9  12595  divalg  12597  divalg2  12599  divalgmod  12600  ndvdssub  12601  ndvdsadd  12602  bitsfval  12609  bitsval  12610  bits0  12614  bitsp1  12617  bitsfzolem  12620  bitsfzo  12621  bitscmp  12624  bitsinv1lem  12627  bitsshft  12661  gcdcllem1  12685  dvdslegcd  12690  bezoutlem4  12715  dvdssqim  12727  dvdsmulgcd  12728  dvdssq  12734  nn0seqcvgd  12735  coprmdvds  12776  coprmdvds2  12777  isprm6  12783  prmdvdsexp  12788  prmdvdsexpr  12790  prmfac1  12792  divgcdodd  12793  rpmul  12797  hashdvds  12838  phiprmpw  12839  eulerthlem2  12845  prmdiv  12848  prmdiveq  12849  odzval  12851  odzcllem  12852  odzdvds  12855  opoe  12859  omoe  12860  pythagtriplem11  12873  pythagtriplem13  12875  pythagtrip  12882  pceulem  12893  pczndvds2  12914  pcdvdsb  12916  pc2dvds  12926  pcz  12928  pcprmpw2  12929  pcaddlem  12931  pcmpt  12935  prmpwdvds  12946  pockthlem  12947  prmreclem2  12959  prmreclem4  12961  4sqlem11  12997  vdwlem9  13031  rami  13057  ramlb  13061  0ram  13062  ramz2  13066  ramub1lem1  13068  imasleval  13438  subsubc  13722  pospo  14102  mulgval  14564  oddvdsnn0  14854  odmulg  14864  pgpfi1  14901  pgpfi  14911  slwispgp  14917  pgpssslw  14920  subgslw  14922  sylow2alem2  14924  sylow2blem3  14928  fislw  14931  efgi  15023  efgval2  15028  efgsrel  15038  efgredlemb  15050  lt6abl  15176  dprdval  15233  dprd2dlem2  15270  dprd2da  15272  dprd2d2  15274  ablfacrplem  15295  ablfac1a  15299  ablfac1b  15300  ablfac1eulem  15302  ablfac1eu  15303  pgpfac1lem3a  15306  ablfaclem3  15317  dvdsrtr  15429  dvdsrmul1  15430  unitpropd  15474  isabvd  15580  zndvds0  16499  znunit  16512  cygth  16520  hmphindis  17483  ordthmeolem  17487  ismet2  17893  xmettri2  17900  imasdsf1olem  17932  imasf1oxmet  17934  comet  18054  stdbdxmet  18056  nmogelb  18220  nmolb  18221  metdsge  18348  metdseq0  18353  iihalf2  18426  bndth  18451  evth  18452  ipcau2  18659  tchcphlem1  18660  tchcphlem2  18661  iscau3  18699  iscmet3  18714  bcthlem1  18741  bcth  18746  minveclem3b  18787  minveclem3  18788  minveclem4  18791  minveclem5  18792  pjthlem1  18796  pjthlem2  18797  pmltpclem1  18803  pmltpc  18805  ivthlem2  18807  ivthlem3  18808  ovolgelb  18834  ovolunlem1  18851  ovoliunlem2  18857  ovolshftlem1  18863  ovolscalem1  18867  ovolicc1  18870  ovolicc2lem3  18873  ioombl1lem4  18913  mbfmulc2lem  18997  mbfposb  19003  mbfaddlem  19010  mbfsup  19014  mbfinf  19015  mbflimsup  19016  i1fposd  19057  itg1ge0a  19061  mbfi1fseqlem4  19068  mbfi1fseqlem6  19070  mbfi1flimlem  19072  mbfi1flim  19073  itg2const2  19091  itg2seq  19092  itg2monolem1  19100  itg2i1fseq  19105  itg2addlem  19108  ibllem  19114  isibl  19115  isibl2  19116  iblitg  19118  dfitg  19119  cbvitg  19125  itgeq2  19127  itgvallem  19134  iblneg  19152  itgneg  19153  itggt0  19191  dvlip  19335  c1lip1  19339  dvfsumle  19363  dvfsumlem2  19369  dvfsumlem4  19371  dvfsum2  19376  mdeglt  19446  degltp1le  19454  deg1suble  19488  ply1divex  19517  plypf1  19589  dgrlb  19613  coemulc  19631  dgrsub  19648  quotval  19667  plydivlem4  19671  quotcan  19684  vieta1lem2  19686  aalioulem2  19708  aaliou3lem9  19725  ulmcn  19771  dvradcnv  19792  sincosq1sgn  19861  sincosq2sgn  19862  sincosq4sgn  19864  logltb  19948  cxpge0  20025  cxple2  20039  logreclem  20111  jensen  20278  emcllem7  20290  wilthlem1  20301  ftalem2  20306  ftalem3  20307  ftalem7  20311  fta  20312  sgmval  20375  mumul  20414  dvdsppwf1o  20421  musum  20426  chtublem  20445  chtub  20446  perfect1  20462  bcmono  20511  bclbnd  20514  bposlem1  20518  bposlem5  20522  lgslem1  20530  lgsval  20534  lgsdilem  20556  lgsne0  20567  lgsqrlem2  20576  lgsqrlem4  20578  lgseisenlem1  20583  lgseisenlem2  20584  lgsquadlem1  20588  lgsquadlem2  20589  lgsquadlem3  20590  lgsquad2lem2  20593  m1lgs  20596  2sqlem4  20601  2sqlem8a  20605  2sqblem  20611  dchrisumlema  20632  dchrisumlem2  20634  dchrisumlem3  20635  chpdifbndlem2  20698  pntrsumbnd2  20711  pntpbnd1  20730  pntibndlem3  20736  pntlemi  20748  pntleme  20752  pntlem3  20753  pnt3  20756  ostth2lem2  20778  ostth3  20782  ostth  20783  nmounbseqi  21348  nmounbseqiOLD  21349  isblo3i  21372  blo3i  21373  blocnilem  21375  siilem2  21423  normlem6  21687  normgt0  21699  norm3dif  21722  norm3lemt  21724  pjhthlem1  21963  pjige0  22263  nmcexi  22599  lnconi  22606  lnopcnbd  22609  lnfncnbd  22630  riesz1  22638  cnlnadjlem2  22641  cnlnadjlem8  22647  leopg  22695  leop2  22697  leoppos  22699  leopadd  22705  leopmuli  22706  leopmul2i  22708  pjssge0i  22739  pjdifnormi  22740  pjssposi  22745  pjssdif1i  22748  chcv1  22928  cvexch  22947  atcvatlem  22958  atcvat3i  22969  atdmd  22971  cdj3i  23014  addltmulALT  23019  bcm1n  23025  ballotlemfc0  23045  ballotlemfcc  23046  ballotleme  23049  ballotlem4  23051  ballotlemic  23059  ballotlem1c  23060  ballotlemsval  23061  ballotlemieq  23069  erdszelem8  23134  erdsze2lem2  23140  eupath2lem3  23308  eupath2  23309  konigsberg  23316  abs2sqle  23421  abs2sqlt  23422  divelunit  23484  mulge0b  23490  mulle0b  23491  pdivsq  23506  dvdspw  23507  poseq  23655  soseq  23656  sltval  23703  brbtwn2  23941  axlowdim2  23996  axlowdim  23997  axcontlem2  24001  axcontlem3  24002  axcontlem4  24003  axcontlem9  24008  axcontlem10  24009  axcontlem11  24010  axcontlem12  24011  cgrdegen  24035  brofs  24036  segconeu  24042  btwntriv2  24043  transportprops  24065  brifs  24074  ifscgr  24075  brcgr3  24077  cgrxfr  24086  brcolinear2  24089  colineardim1  24092  brfs  24110  idinside  24115  btwnconn1lem11  24128  btwnconn1lem12  24129  btwnconn1lem14  24131  brsegle  24139  seglerflx  24143  seglemin  24144  segleantisym  24146  btwnsegle  24148  outsideofeu  24162  outsidele  24163  fvray  24172  oriso  24614  geme2  24675  iintlem1  25010  isibcg  25591  nn0prpwlem  25638  nn0prpw  25639  seqpo  25857  incsequz2  25859  mettrifi  25873  heibor1lem  25933  rrncmslem  25956  elpell1qr2  26357  monotuz  26426  monotoddzzfi  26427  monotoddzz  26428  oddcomabszz  26429  rmxypos  26434  mzpcong  26459  congrep  26460  acongsym  26463  acongneg2  26464  acongtr  26465  acongeq12d  26466  dvdsabsmod0  26479  divalgmodcl  26480  jm2.18  26481  jm2.19lem2  26483  jm2.19lem3  26484  jm2.19lem4  26485  jm2.19  26486  jm2.25  26492  jm2.15nn0  26496  jm2.16nn0  26497  jm2.27  26501  rmydioph  26507  expdiophlem1  26514  expdiophlem2  26515  fnwe2lem2  26548  lmisfree  26712  evth2f  27086  evthf  27098  rfcnpre3  27104  fmul01  27110  fmul01lt1lem1  27114  climinf  27132  climinff  27137  stoweidlem3  27152  stoweidlem7  27156  stoweidlem13  27162  stoweidlem15  27164  stoweidlem16  27165  stoweidlem18  27167  stoweidlem24  27173  stoweidlem26  27175  stoweidlem27  27176  stoweidlem28  27177  stoweidlem31  27180  stoweidlem34  27183  stoweidlem36  27185  stoweidlem37  27186  stoweidlem41  27190  stoweidlem44  27193  stoweidlem45  27194  stoweidlem46  27195  stoweidlem48  27197  stoweidlem51  27200  stoweidlem55  27204  stoweidlem59  27208  stoweidlem60  27209  stoweidlem62  27211  lsatcv0eq  28505  oposlem  28641  oplecon1b  28659  opltcon1b  28663  atlatmstc  28777  cvlexch1  28786  cvlexch2  28787  cvlexchb2  28789  cvlatexchb2  28793  cvlatexch2  28795  cvlatcvr2  28800  cvlsupr2  28801  ishlat1  28810  hlsuprexch  28838  cvrexch  28877  cvrat  28879  atcvr0eq  28883  atcvrj0  28885  atltcvr  28892  cvrat3  28899  cvrat4  28900  cvrat42  28901  3noncolr2  28906  hlatcon2  28909  4noncolr3  28910  3dimlem1  28915  3dimlem2  28916  3dimlem3a  28917  3dimlem3  28918  3dimlem3OLDN  28919  3dimlem4a  28920  3dimlem4  28921  3dimlem4OLDN  28922  3dim1lem5  28923  3dim2  28925  3dim3  28926  ps-1  28934  ps-2  28935  3atlem5  28944  3atlem6  28945  lplni2  28994  lplnnle2at  28998  lplnnleat  28999  lplnnlelln  29000  lplnribN  29008  lplnexllnN  29021  lvoli2  29038  lvolnle3at  29039  lvolnleat  29040  lvolnlelln  29041  lvolnlelpln  29042  4atlem9  29060  4atlem10a  29061  4atlem11a  29064  4atlem11  29066  4atlem12a  29067  dalempnes  29108  dalemqnet  29109  dalem1  29116  dalemswapyzps  29147  dalemrotps  29148  dalem30  29159  dalem35  29164  lineset  29195  islinei  29197  psubspset  29201  psubspi2N  29205  snatpsubN  29207  2llnma1  29244  elpaddn0  29257  elpaddri  29259  elpaddat  29261  elpadd2at  29263  paddcom  29270  paddasslem12  29288  pmapjat1  29310  llnexchb2  29326  lhp2at0nle  29492  lhprelat3N  29497  4atexlemswapqr  29520  4atexlemcnd  29529  lautle  29541  lautcvr  29549  ltrnel  29596  ltrneq2  29605  trlnle  29643  cdlemc3  29650  cdlemd6  29660  cdleme3  29694  cdleme7aa  29699  cdleme7  29706  cdleme11c  29718  cdleme15c  29733  cdleme20y  29759  cdleme20m  29780  cdleme21b  29783  cdleme21c  29784  cdleme21at  29785  cdleme36a  29917  cdleme43bN  29947  cdleme43dN  29949  cdleme46f2g2  29950  cdleme46f2g1  29951  cdlemeg46c  29970  cdlemeg46nlpq  29974  cdlemb3  30063  cdlemg4d  30070  cdlemg6d  30078  cdlemg10c  30096  cdlemg12  30107  cdlemg27b  30153  djhcvat42  30873
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1534  ax-5 1545  ax-17 1604  ax-9 1637  ax-8 1645  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1868  ax-ext 2266
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 938  df-tru 1312  df-ex 1530  df-nf 1533  df-sb 1632  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-rab 2554  df-v 2792  df-dif 3157  df-un 3159  df-in 3161  df-ss 3168  df-nul 3458  df-if 3568  df-sn 3648  df-pr 3649  df-op 3651  df-br 4026
  Copyright terms: Public domain W3C validator