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

Theorem breq2d 4429
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 4421 . 2  |-  ( A  =  B  ->  ( C R A  <->  C R B ) )
31, 2syl 17 1  |-  ( ph  ->  ( C R A  <-> 
C R B ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187    = wceq 1437   class class class wbr 4417
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1838  ax-10 1886  ax-11 1891  ax-12 1904  ax-13 2052  ax-ext 2398
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2406  df-cleq 2412  df-clel 2415  df-nfc 2570  df-rab 2782  df-v 3080  df-dif 3436  df-un 3438  df-in 3440  df-ss 3447  df-nul 3759  df-if 3907  df-sn 3994  df-pr 3996  df-op 4000  df-br 4418
This theorem is referenced by:  breqtrd  4441  sbcbr1g  4471  pofun  4782  csbfv12  5907  isorel  6223  soisores  6224  soisoi  6225  isocnv  6227  isotr  6233  f1owe  6250  caovordig  6479  caovordg  6481  caovord  6485  f1oweALT  6782  frxp  6908  xporderlem  6909  fnwelem  6913  difsnen  7651  domdifsn  7652  unfilem3  7834  domunfican  7841  marypha1lem  7944  marypha1  7945  inflb  8002  wemapwe  8192  oef1o  8193  r1sdom  8235  sdomsdomcardi  8395  alephordi  8494  pwcdadom  8635  sornom  8696  axdclem  8938  pwcfsdom  8997  elgch  9036  winalim2  9110  rankcf  9191  inatsk  9192  pinq  9341  nqereu  9343  ltaddnq  9388  ltrnq  9393  archnq  9394  addclprlem1  9430  mulclprlem  9433  1idpr  9443  ltaprlem  9458  ltapr  9459  prlem936  9461  ltasr  9513  mulgt0sr  9518  sqgt0sr  9519  map2psrpr  9523  axpre-ltadd  9580  axpre-mulgt0  9581  axpre-sup  9582  ltsubadd2  10074  lesubadd2  10076  ltaddpos2  10094  posdif  10096  lesub1  10097  ltnegcon1  10104  lenegcon1  10107  addge02  10114  leaddle0  10118  mulge0  10121  msqge0  10124  ltordlem  10128  sublt0d  10227  prodgt0  10439  prodgt02  10440  prodge02  10442  ltmulgt12  10455  lemulge12  10457  mulge0b  10464  mulle0b  10465  ltdivmul  10469  ledivmul  10470  ltdivmul2  10471  lt2mul2div  10472  ledivmul2  10473  ledivmul2OLD  10474  ltrec  10477  ltrec1  10482  ltdiv23  10486  lediv23  10487  nnge1  10624  halfpos  10832  lt2halves  10836  addltmul  10837  avglt2  10840  avgle2  10842  nnrecl  10856  zltlem1  10978  gtndiv  11002  nn01to3  11246  rebtwnz  11252  xrmax1  11459  max1ALT  11470  qbtwnre  11481  xralrple  11487  xltnegi  11498  xmulval  11507  xsubge0  11536  xposdif  11537  xlesubadd  11538  divelunit  11761  eluzgtdifelfzo  11962  fllelt  12019  flflp1  12029  flbi  12037  btwnzge0  12047  dfceil2  12054  ceilval2  12055  2submod  12137  om2uzlti  12150  monoord  12229  sermono  12231  expval  12260  expnbnd  12387  discr1  12394  discr  12395  facwordi  12460  seqcoll  12610  seqcoll2  12611  hashtpg  12621  swrdccat3blem  12825  cnpart  13271  sqrlem6  13279  sqrmo  13283  resqreu  13284  resqrtcl  13285  resqrtthlem  13286  sqrtneg  13299  sqreulem  13390  sqreu  13391  sqrtthlem  13393  eqsqrtd  13398  limsuple  13503  limsupleOLD  13504  rlimcld2  13609  rlimrege0  13610  o1compt  13618  climserle  13693  caurcvgr  13705  caurcvgrOLD  13706  fsum00  13825  fsumabs  13828  climcndslem2  13875  climcnds  13876  supcvg  13881  georeclim  13895  geoisumr  13901  cvgrat  13906  sin01bnd  14206  cos01bnd  14207  ruclem1  14250  ruclem9  14257  ruclem12  14260  dvdsaddr  14311  dvdssub  14312  dvdssubr  14313  dvdsfac  14327  dvdsmod  14329  oddp1even  14334  fproddvdsd  14337  divalglem0  14338  divalglem2  14340  divalglem4  14341  divalglem5  14342  divalglem9  14346  divalg  14348  divalg2  14350  divalgmod  14351  ndvdssub  14352  ndvdsadd  14353  bitsfval  14360  bitsval  14361  bits0  14365  bitsp1  14368  bitsfzolem  14371  bitsfzo  14372  bitscmp  14375  bitsinv1lem  14378  bitsshft  14412  gcdcllem1  14436  dvdslegcd  14441  bezoutlem4  14469  dvdssqim  14481  dvdsmulgcd  14482  dvdssq  14488  nn0seqcvgd  14489  lcmfunsnlem2lem2  14572  divgcdodd  14613  coprmdvds  14619  coprmdvds2  14620  isprm6  14626  prmdvdsexp  14627  prmdvdsexpr  14629  prmfac1  14631  rpmul  14635  hashdvds  14681  phiprmpw  14682  eulerthlem2  14688  prmdiv  14691  prmdiveq  14692  odzval  14694  odzcllem  14695  odzdvds  14698  opoe  14713  omoe  14714  pythagtriplem11  14727  pythagtriplem13  14729  pythagtrip  14736  pceulem  14747  pczndvds2  14768  pcdvdsb  14770  pc2dvds  14780  pcz  14782  pcprmpw2  14783  pcaddlem  14785  pcmpt  14789  prmpwdvds  14800  pockthlem  14801  prmreclem2  14813  prmreclem4  14815  4sqlem11  14851  vdwlem9  14891  rami  14924  ramlb  14929  0ram  14930  ramz2  14934  ramub1lem1  14936  prmdvdsprmo  14952  prmgaplcmlem1OLD  14964  prmdvdsprmorOLD  14967  prmgaplem7  14979  prmgaplem8  14980  imasleval  15391  subsubc  15702  pospo  16163  mulgval  16704  oddvdsnn0  17128  odmulg  17138  pgpfi1  17175  pgpfi  17185  slwispgp  17191  pgpssslw  17194  subgslw  17196  sylow2alem2  17198  sylow2blem3  17202  fislw  17205  efgi  17297  efgval2  17302  efgsrel  17312  efgredlemb  17324  lt6abl  17457  telgsums  17551  dprdval  17563  dprd2dlem2  17601  dprd2da  17603  dprd2d2  17605  ablfacrplem  17626  ablfac1a  17630  ablfac1b  17631  ablfac1eulem  17633  ablfac1eu  17634  pgpfac1lem3a  17637  ablfaclem3  17648  dvdsrtr  17808  dvdsrmul1  17809  unitpropd  17853  isabvd  17976  mplval  18580  ressmplbas2  18607  mplbaspropd  18758  zndvds0  19045  znunit  19058  cygth  19066  frlmup1  19280  lmisfree  19324  pmatcoe1fsupp  19649  fvmptnn04if  19797  hmphindis  20736  ordthmeolem  20740  psmettri2  21249  ismet2  21272  xmettri2  21279  imasdsf1olem  21312  imasf1oxmet  21314  comet  21452  stdbdxmet  21454  nmogelb  21641  nmolb  21642  metdsge  21770  metdseq0  21775  iihalf2  21850  bndth  21875  evth  21876  ipcau2  22094  tchcphlem1  22095  tchcphlem2  22096  iscau3  22134  iscmet3  22149  bcthlem1  22178  bcth  22183  minveclem3b  22256  minveclem3  22257  minveclem4  22260  minveclem5  22261  pjthlem1  22265  pjthlem2  22266  pmltpclem1  22273  pmltpc  22275  ivthlem2  22277  ivthlem3  22278  ovolgelb  22307  ovolunlem1  22324  ovoliunlem2  22330  ovolshftlem1  22336  ovolscalem1  22340  ovolicc1  22343  ovolicc2lem3  22346  ioombl1lem4  22388  mbfmulc2lem  22477  mbfposb  22483  mbfaddlem  22490  mbfsup  22494  mbfinf  22495  mbfinfOLD  22496  mbflimsup  22497  mbflimsupOLD  22498  i1fposd  22539  itg1ge0a  22543  mbfi1fseqlem4  22550  mbfi1fseqlem6  22552  mbfi1flimlem  22554  mbfi1flim  22555  itg2const2  22573  itg2seq  22574  itg2monolem1  22582  itg2i1fseq  22587  itg2addlem  22590  ibllem  22596  isibl  22597  isibl2  22598  iblitg  22600  dfitg  22601  cbvitg  22607  itgeq2  22609  itgvallem  22616  iblneg  22634  itgneg  22635  itggt0  22673  dvlip  22819  c1lip1  22823  dvfsumle  22847  dvfsumlem2  22853  dvfsumlem4  22855  dvfsum2  22860  mdeglt  22888  degltp1le  22896  deg1suble  22930  ply1divex  22959  plypf1  23031  dgrlb  23055  coemulc  23074  dgrsub  23091  quotval  23110  plydivlem4  23114  quotcan  23127  vieta1lem2  23129  aalioulem2  23151  aaliou3lem9  23168  ulmcn  23216  dvradcnv  23238  sincosq1sgn  23315  sincosq2sgn  23316  sincosq4sgn  23318  logltb  23411  cxpge0  23490  cxple2  23504  logreclem  23561  jensen  23776  emcllem7  23789  lgamgulmlem1  23816  lgamgulmlem2  23817  lgamgulmlem3  23818  lgamgulmlem5  23820  lgambdd  23824  lgamcvglem  23827  wilthlem1  23855  ftalem2  23860  ftalem3  23861  ftalem7  23865  fta  23866  sgmval  23929  mumul  23968  dvdsppwf1o  23975  musum  23980  chtublem  23999  chtub  24000  perfect1  24016  bcmono  24065  bclbnd  24068  bposlem1  24072  bposlem5  24076  lgslem1  24084  lgsval  24088  lgsdilem  24110  lgsne0  24121  lgsqrlem2  24130  lgsqrlem4  24132  lgseisenlem1  24137  lgseisenlem2  24138  lgsquadlem1  24142  lgsquadlem2  24143  lgsquadlem3  24144  lgsquad2lem2  24147  m1lgs  24150  2sqlem4  24155  2sqlem8a  24159  2sqblem  24165  dchrisumlema  24186  dchrisumlem2  24188  dchrisumlem3  24189  chpdifbndlem2  24252  pntrsumbnd2  24265  pntpbnd1  24284  pntibndlem3  24290  pntlemi  24302  pntleme  24306  pntlem3  24307  pnt3  24310  ostth2lem2  24332  ostth3  24336  ostth  24337  tgcgrxfr  24422  islmib  24682  lmicom  24683  trgcopyeu  24701  iscgra  24704  iscgra1  24705  iscgrad  24706  brbtwn2  24778  axlowdim2  24833  axlowdim  24834  axcontlem2  24838  axcontlem3  24839  axcontlem4  24840  axcontlem9  24845  axcontlem10  24846  axcontlem11  24847  axcontlem12  24848  ebtwntg  24855  ausisusgraedg  24926  clwlkisclwwlklem2a4  25354  clwlkisclwwlklem2a  25355  nbhashuvtx1  25485  eupath2lem3  25549  eupath2  25550  konigsberg  25557  frgrareggt1  25686  ex-ind-dvds  25741  nmounbseqi  26260  nmounbseqiALT  26261  isblo3i  26284  blo3i  26285  blocnilem  26287  siilem2  26335  normlem6  26600  normgt0  26612  norm3dif  26635  norm3lemt  26637  pjhthlem1  26876  pjige0  27176  nmcexi  27511  lnconi  27518  lnopcnbd  27521  lnfncnbd  27542  riesz1  27550  cnlnadjlem2  27553  cnlnadjlem8  27559  leopg  27607  leop2  27609  leoppos  27611  leopadd  27617  leopmuli  27618  leopmul2i  27620  pjssge0i  27651  pjdifnormi  27652  pjssposi  27657  pjssdif1i  27660  chcv1  27840  cvexch  27859  atcvatlem  27870  atcvat3i  27881  atdmd  27883  cdj3i  27926  addltmulALT  27931  xrofsup  28186  xrge0addgt0  28289  omndadd  28304  omndmul2  28310  ogrpinvlt  28322  isinftm  28333  isarchi3  28339  archirng  28340  archirngz  28341  archiexdiv  28342  isorng  28398  orngmul  28402  ofldchr  28413  isarchiofld  28416  elrhmunit  28419  rearchi  28441  fzto1st  28452  unitdivcld  28543  esumlub  28717  esumfsup  28727  esumcvg  28743  esum2d  28750  dya2ub  28928  omssubadd  28958  carsgmon  28972  itgeq12dv  28984  oddpwdc  29010  eulerpartlems  29016  prob01  29069  orvcval  29113  ballotlemfc0  29148  ballotlemfcc  29149  ballotleme  29152  ballotlem4  29154  ballotlem1c  29163  ballotlemsval  29164  ballotlemieq  29172  sgnmulsgp  29206  signsply0  29225  signslema  29236  signsvfpn  29259  erdszelem8  29706  erdsze2lem2  29712  abs2sqle  30109  abs2sqlt  30110  possumd  30150  pdivsq  30169  dvdspw  30170  poseq  30275  soseq  30276  sltval  30318  cgrdegen  30553  brofs  30554  segconeu  30560  btwntriv2  30561  transportprops  30583  brifs  30592  ifscgr  30593  brcgr3  30595  cgrxfr  30604  brcolinear2  30607  colineardim1  30610  brfs  30628  idinside  30633  btwnconn1lem11  30646  btwnconn1lem12  30647  btwnconn1lem14  30649  brsegle  30657  seglerflx  30661  seglemin  30662  segleantisym  30664  btwnsegle  30666  outsideofeu  30680  outsidele  30681  fvray  30690  nn0prpwlem  30760  nn0prpw  30761  ltflcei  31637  cos2h  31640  tan2h  31641  poimirlem5  31649  poimirlem6  31650  poimirlem7  31651  poimirlem8  31652  poimirlem10  31654  poimirlem11  31655  poimirlem12  31656  poimirlem15  31659  poimirlem16  31660  poimirlem17  31661  poimirlem18  31662  poimirlem19  31663  poimirlem20  31664  poimirlem21  31665  poimirlem22  31666  poimirlem25  31669  poimirlem27  31671  poimirlem28  31672  poimirlem29  31673  poimirlem30  31674  poimirlem31  31675  poimirlem32  31676  poimir  31677  heicant  31679  mblfinlem2  31682  mblfinlem3  31683  mblfinlem4  31684  dvtanlemOLD  31695  itg2addnclem  31697  itg2addnclem2  31698  itg2gt0cn  31701  itggt0cn  31718  ftc1anclem5  31725  dvasin  31732  areacirclem1  31736  areacirclem4  31739  areacirclem5  31740  areacirc  31741  seqpo  31780  incsequz2  31782  mettrifi  31790  heibor1lem  31845  rrncmslem  31868  lsatcv0eq  32322  oposlem  32457  oplecon1b  32476  opltcon1b  32480  atlatmstc  32594  cvlexch1  32603  cvlexch2  32604  cvlexchb2  32606  cvlatexchb2  32610  cvlatexch2  32612  cvlatcvr2  32617  cvlsupr2  32618  ishlat1  32627  hlsuprexch  32655  cvrexch  32694  cvrat  32696  atcvr0eq  32700  atcvrj0  32702  atltcvr  32709  cvrat3  32716  cvrat4  32717  cvrat42  32718  3noncolr2  32723  hlatcon2  32726  4noncolr3  32727  3dimlem1  32732  3dimlem2  32733  3dimlem3a  32734  3dimlem3  32735  3dimlem3OLDN  32736  3dimlem4a  32737  3dimlem4  32738  3dimlem4OLDN  32739  3dim1lem5  32740  3dim2  32742  3dim3  32743  ps-1  32751  ps-2  32752  3atlem5  32761  3atlem6  32762  lplni2  32811  lplnnle2at  32815  lplnnleat  32816  lplnnlelln  32817  lplnribN  32825  lplnexllnN  32838  lvoli2  32855  lvolnle3at  32856  lvolnleat  32857  lvolnlelln  32858  lvolnlelpln  32859  4atlem9  32877  4atlem10a  32878  4atlem11a  32881  4atlem11  32883  4atlem12a  32884  dalempnes  32925  dalemqnet  32926  dalem1  32933  dalemswapyzps  32964  dalemrotps  32965  dalem30  32976  dalem35  32981  lineset  33012  islinei  33014  psubspset  33018  psubspi2N  33022  snatpsubN  33024  2llnma1  33061  elpaddn0  33074  elpaddri  33076  elpaddat  33078  elpadd2at  33080  paddcom  33087  paddasslem12  33105  pmapjat1  33127  llnexchb2  33143  lhp2at0nle  33309  lhprelat3N  33314  4atexlemswapqr  33337  4atexlemcnd  33346  lautle  33358  lautcvr  33366  ltrnel  33413  ltrneq2  33422  trlnle  33461  cdlemc3  33468  cdlemd6  33478  cdleme3  33512  cdleme7aa  33517  cdleme7  33524  cdleme11c  33536  cdleme15c  33551  cdleme20yOLD  33578  cdleme20m  33599  cdleme21b  33602  cdleme21c  33603  cdleme21at  33604  cdleme36a  33736  cdleme43bN  33766  cdleme43dN  33768  cdleme46f2g2  33769  cdleme46f2g1  33770  cdlemeg46c  33789  cdlemeg46nlpq  33793  cdlemb3  33882  cdlemg4d  33889  cdlemg6d  33897  cdlemg10c  33915  cdlemg12  33926  cdlemg27b  33972  djhcvat42  34692  elpell1qr2  35428  monotuz  35499  monotoddzzfi  35500  monotoddzz  35501  oddcomabszz  35502  rmxypos  35507  mzpcong  35532  congrep  35533  acongsym  35536  acongneg2  35537  acongtr  35538  acongeq12d  35539  dvdsabsmod0OLD  35551  divalgmodcl  35552  jm2.18  35553  jm2.19lem2  35555  jm2.19lem3  35556  jm2.19lem4  35557  jm2.19  35558  jm2.25  35564  jm2.15nn0  35568  jm2.16nn0  35569  jm2.27  35573  rmydioph  35579  expdiophlem1  35586  expdiophlem2  35587  fnwe2lem2  35619  relexpmulg  35945  relexpxpmin  35952  frege124d  35996  frege72  36172  frege91  36191  inductionexd  36234  leeq2d  36237  imo72b2lem0  36249  imo72b2lem2  36251  imo72b2lem1  36255  imo72b2  36260  dvgrat  36302  hashnzfz  36310  evth2f  36980  evthf  36992  rfcnpre3  36998  ltaddneg  37121  upbdrech2  37139  supxrgelem  37173  supxrge  37174  fmul01  37234  fmul01lt1lem1  37238  climinf  37260  climinfOLD  37261  climinff  37266  climinffOLD  37267  limcrecl  37285  limsupre  37297  limsupreOLD  37298  limclner  37308  cncficcgt0  37342  stoweidlem3  37436  stoweidlem7  37440  stoweidlem15  37448  stoweidlem16  37449  stoweidlem18  37451  stoweidlem26  37459  stoweidlem27  37460  stoweidlem28  37461  stoweidlem31  37465  stoweidlem34  37468  stoweidlem36  37470  stoweidlem37  37471  stoweidlem41  37475  stoweidlem44  37478  stoweidlem45  37479  stoweidlem46  37480  stoweidlem48  37482  stoweidlem51  37485  stoweidlem55  37489  stoweidlem59  37493  stoweidlem60  37494  stoweidlem62  37496  stoweidlem62OLD  37497  fourierdlem42  37584  fourierdlem50  37592  fourierdlem54  37596  fourierdlem68  37610  fourierdlem79  37621  fourierdlem96  37638  fourierdlem97  37639  fourierdlem98  37640  fourierdlem99  37641  fourierdlem105  37647  fourierdlem108  37650  fourierdlem110  37652  fourierdlem111  37653  etransclem24  37694  etransclem25  37695  etransclem35  37705  etransclem37  37707  etransclem41  37711  etransclem44  37714  sge0gerp  37775  sge0pnffigt  37776  sge0gerpmpt  37782  omessle  37832  smonoord  38121  iccpartiltu  38139  iccpartlt  38141  iccpartgtl  38143  iccpartgt  38144  iccpartgel  38146  iccpartrn  38147  iccpartiun  38151  icceuelpartlem  38152  iccpartdisj  38154  iccpartnel  38155  bits0ALTV  38211  sgoldbaltlem1  38283  bgoldbtbndlem2  38304  bgoldbtbndlem3  38305  bgoldbtbnd  38307  ltsubsubaddltsub  38410  subsubelfzo0  38424  nn0le2is012  38921  lcoop  38977  islininds  39012  ldepsnlinc  39074  ltsubaddb  39084  ltsubsubb  39085  ltsubadd2b  39086  logle1b  39118  loglt1b  39119  bigoval  39134  elbigo2r  39138  logbge0b  39148  logblt1b  39149  fldivexpfllog2  39150  nnlog2ge0lt1  39151  fllog2  39153  nnpw2pmod  39168  dignn0ldlem  39187  dig2nn1st  39190
  Copyright terms: Public domain W3C validator