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

Theorem breq2d 4446
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 4438 . 2  |-  ( A  =  B  ->  ( C R A  <->  C R B ) )
31, 2syl 16 1  |-  ( ph  ->  ( C R A  <-> 
C R B ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    = wceq 1381   class class class wbr 4434
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 974  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-rab 2800  df-v 3095  df-dif 3462  df-un 3464  df-in 3466  df-ss 3473  df-nul 3769  df-if 3924  df-sn 4012  df-pr 4014  df-op 4018  df-br 4435
This theorem is referenced by:  breqtrd  4458  sbcbr1g  4489  pofun  4803  csbfv12  5888  csbfv12gOLD  5889  isorel  6204  soisores  6205  soisoi  6206  isocnv  6208  isotr  6214  f1owe  6231  caovordig  6462  caovordg  6464  caovord  6468  f1oweALT  6766  frxp  6892  xporderlem  6893  fnwelem  6897  difsnen  7598  domdifsn  7599  unfilem3  7785  domunfican  7792  marypha1lem  7892  marypha1  7893  wemapwe  8139  oef1o  8141  r1sdom  8192  sdomsdomcardi  8352  alephordi  8455  pwcdadom  8596  sornom  8657  axdclem  8899  pwcfsdom  8958  elgch  9000  winalim2  9074  rankcf  9155  inatsk  9156  pinq  9305  nqereu  9307  ltaddnq  9352  ltrnq  9357  archnq  9358  addclprlem1  9394  mulclprlem  9397  1idpr  9407  ltaprlem  9422  ltapr  9423  prlem936  9425  ltasr  9477  mulgt0sr  9482  sqgt0sr  9483  map2psrpr  9487  axpre-ltadd  9544  axpre-mulgt0  9545  axpre-sup  9546  ltsubadd2  10026  lesubadd2  10028  ltaddpos2  10046  posdif  10048  lesub1  10049  ltnegcon1  10056  lenegcon1  10059  addge02  10066  leaddle0  10070  mulge0  10073  msqge0  10077  ltordlem  10081  prodgt0  10390  prodgt02  10391  prodge02  10393  ltmulgt12  10406  lemulge12  10408  mulge0b  10415  mulle0b  10416  ltdivmul  10420  ledivmul  10421  ledivmulOLD  10422  ltdivmul2  10423  lt2mul2div  10424  ledivmul2  10425  ledivmul2OLD  10426  ltrec  10429  ltrec1  10435  ltdiv23  10439  lediv23  10440  nnge1  10565  halfpos  10772  lt2halves  10776  addltmul  10777  avglt2  10780  avgle2  10782  nnrecl  10796  zltlem1  10919  gtndiv  10943  nn01to3  11181  rebtwnz  11187  xrmax1  11382  max1ALT  11393  qbtwnre  11404  xralrple  11410  xltnegi  11421  xmulval  11430  xsubge0  11459  xposdif  11460  xlesubadd  11461  divelunit  11668  eluzgtdifelfzo  11854  fllelt  11910  flflp1  11920  flbi  11928  btwnzge0  11937  dfceil2  11944  ceilval2  11945  2submod  12024  om2uzlti  12037  monoord  12113  sermono  12115  expval  12144  expnbnd  12271  discr1  12278  discr  12279  facwordi  12343  seqcoll  12488  seqcoll2  12489  hashtpg  12499  swrdccat3blem  12696  cnpart  13049  sqrlem6  13057  sqrmo  13061  resqreu  13062  resqrtcl  13063  resqrtthlem  13064  sqrtneg  13077  sqreulem  13168  sqreu  13169  sqrtthlem  13171  eqsqrtd  13176  limsuple  13277  rlimcld2  13377  rlimrege0  13378  o1compt  13386  climserle  13461  caurcvgr  13472  fsum00  13588  fsumabs  13591  climcndslem2  13638  climcnds  13639  supcvg  13643  georeclim  13657  geoisumr  13663  cvgrat  13668  sin01bnd  13794  cos01bnd  13795  ruclem1  13838  ruclem9  13845  ruclem12  13848  dvdsaddr  13899  dvdssub  13900  dvdssubr  13901  dvdsfac  13915  dvdsmod  13917  oddp1even  13922  divalglem0  13925  divalglem2  13927  divalglem4  13928  divalglem5  13929  divalglem9  13933  divalg  13935  divalg2  13937  divalgmod  13938  ndvdssub  13939  ndvdsadd  13940  bitsfval  13947  bitsval  13948  bits0  13952  bitsp1  13955  bitsfzolem  13958  bitsfzo  13959  bitscmp  13962  bitsinv1lem  13965  bitsshft  13999  gcdcllem1  14023  dvdslegcd  14028  bezoutlem4  14053  dvdssqim  14065  dvdsmulgcd  14066  dvdssq  14072  nn0seqcvgd  14073  coprmdvds  14117  coprmdvds2  14118  isprm6  14124  prmdvdsexp  14129  prmdvdsexpr  14131  prmfac1  14133  divgcdodd  14134  rpmul  14138  hashdvds  14179  phiprmpw  14180  eulerthlem2  14186  prmdiv  14189  prmdiveq  14190  odzval  14192  odzcllem  14193  odzdvds  14196  opoe  14209  omoe  14210  pythagtriplem11  14223  pythagtriplem13  14225  pythagtrip  14232  pceulem  14243  pczndvds2  14264  pcdvdsb  14266  pc2dvds  14276  pcz  14278  pcprmpw2  14279  pcaddlem  14281  pcmpt  14285  prmpwdvds  14296  pockthlem  14297  prmreclem2  14309  prmreclem4  14311  4sqlem11  14347  vdwlem9  14381  rami  14407  ramlb  14411  0ram  14412  ramz2  14416  ramub1lem1  14418  imasleval  14812  subsubc  15093  pospo  15474  mulgval  16015  oddvdsnn0  16439  odmulg  16449  pgpfi1  16486  pgpfi  16496  slwispgp  16502  pgpssslw  16505  subgslw  16507  sylow2alem2  16509  sylow2blem3  16513  fislw  16516  efgi  16608  efgval2  16613  efgsrel  16623  efgredlemb  16635  lt6abl  16768  telgsums  16893  dprdval  16905  dprdvalOLD  16907  dprd2dlem2  16960  dprd2da  16962  dprd2d2  16964  ablfacrplem  16987  ablfac1a  16991  ablfac1b  16992  ablfac1eulem  16994  ablfac1eu  16995  pgpfac1lem3a  16998  ablfaclem3  17009  dvdsrtr  17172  dvdsrmul1  17173  unitpropd  17217  isabvd  17340  mplval  17955  ressmplbas2  17988  mplbaspropd  18149  zndvds0  18459  znunit  18472  cygth  18480  frlmup1  18702  lmisfree  18747  pmatcoe1fsupp  19072  fvmptnn04if  19220  hmphindis  20168  ordthmeolem  20172  psmettri2  20683  ismet2  20706  xmettri2  20713  imasdsf1olem  20746  imasf1oxmet  20748  comet  20886  stdbdxmet  20888  nmogelb  21093  nmolb  21094  metdsge  21223  metdseq0  21228  iihalf2  21303  bndth  21328  evth  21329  ipcau2  21547  tchcphlem1  21548  tchcphlem2  21549  iscau3  21587  iscmet3  21602  bcthlem1  21633  bcth  21638  minveclem3b  21713  minveclem3  21714  minveclem4  21717  minveclem5  21718  pjthlem1  21722  pjthlem2  21723  pmltpclem1  21730  pmltpc  21732  ivthlem2  21734  ivthlem3  21735  ovolgelb  21761  ovolunlem1  21778  ovoliunlem2  21784  ovolshftlem1  21790  ovolscalem1  21794  ovolicc1  21797  ovolicc2lem3  21800  ioombl1lem4  21841  mbfmulc2lem  21924  mbfposb  21930  mbfaddlem  21937  mbfsup  21941  mbfinf  21942  mbflimsup  21943  i1fposd  21984  itg1ge0a  21988  mbfi1fseqlem4  21995  mbfi1fseqlem6  21997  mbfi1flimlem  21999  mbfi1flim  22000  itg2const2  22018  itg2seq  22019  itg2monolem1  22027  itg2i1fseq  22032  itg2addlem  22035  ibllem  22041  isibl  22042  isibl2  22043  iblitg  22045  dfitg  22046  cbvitg  22052  itgeq2  22054  itgvallem  22061  iblneg  22079  itgneg  22080  itggt0  22118  dvlip  22264  c1lip1  22268  dvfsumle  22292  dvfsumlem2  22298  dvfsumlem4  22300  dvfsum2  22305  mdeglt  22335  degltp1le  22343  deg1suble  22378  ply1divex  22407  plypf1  22479  dgrlb  22503  coemulc  22521  dgrsub  22538  quotval  22557  plydivlem4  22561  quotcan  22574  vieta1lem2  22576  aalioulem2  22598  aaliou3lem9  22615  ulmcn  22663  dvradcnv  22685  sincosq1sgn  22760  sincosq2sgn  22761  sincosq4sgn  22763  logltb  22853  cxpge0  22933  cxple2  22947  logreclem  23019  jensen  23187  emcllem7  23200  wilthlem1  23211  ftalem2  23216  ftalem3  23217  ftalem7  23221  fta  23222  sgmval  23285  mumul  23324  dvdsppwf1o  23331  musum  23336  chtublem  23355  chtub  23356  perfect1  23372  bcmono  23421  bclbnd  23424  bposlem1  23428  bposlem5  23432  lgslem1  23440  lgsval  23444  lgsdilem  23466  lgsne0  23477  lgsqrlem2  23486  lgsqrlem4  23488  lgseisenlem1  23493  lgseisenlem2  23494  lgsquadlem1  23498  lgsquadlem2  23499  lgsquadlem3  23500  lgsquad2lem2  23503  m1lgs  23506  2sqlem4  23511  2sqlem8a  23515  2sqblem  23521  dchrisumlema  23542  dchrisumlem2  23544  dchrisumlem3  23545  chpdifbndlem2  23608  pntrsumbnd2  23621  pntpbnd1  23640  pntibndlem3  23646  pntlemi  23658  pntleme  23662  pntlem3  23663  pnt3  23666  ostth2lem2  23688  ostth3  23692  ostth  23693  tgcgrxfr  23778  islmib  24022  lmicom  24023  brbtwn2  24077  axlowdim2  24132  axlowdim  24133  axcontlem2  24137  axcontlem3  24138  axcontlem4  24139  axcontlem9  24144  axcontlem10  24145  axcontlem11  24146  axcontlem12  24147  ebtwntg  24154  ausisusgraedg  24225  clwlkisclwwlklem2a4  24653  clwlkisclwwlklem2a  24654  nbhashuvtx1  24784  eupath2lem3  24848  eupath2  24849  konigsberg  24856  frgrareggt1  24985  ex-ind-dvds  25039  nmounbseqi  25561  nmounbseqiOLD  25562  isblo3i  25585  blo3i  25586  blocnilem  25588  siilem2  25636  normlem6  25901  normgt0  25913  norm3dif  25936  norm3lemt  25938  pjhthlem1  26178  pjige0  26478  nmcexi  26814  lnconi  26821  lnopcnbd  26824  lnfncnbd  26845  riesz1  26853  cnlnadjlem2  26856  cnlnadjlem8  26862  leopg  26910  leop2  26912  leoppos  26914  leopadd  26920  leopmuli  26921  leopmul2i  26923  pjssge0i  26954  pjdifnormi  26955  pjssposi  26960  pjssdif1i  26963  chcv1  27143  cvexch  27162  atcvatlem  27173  atcvat3i  27184  atdmd  27186  cdj3i  27229  addltmulALT  27234  xrofsup  27451  xrge0addgt0  27551  omndadd  27566  omndmul2  27572  ogrpinvlt  27584  isinftm  27595  isarchi3  27601  archirng  27602  archirngz  27603  archiexdiv  27604  isorng  27659  orngmul  27663  ofldchr  27674  isarchiofld  27677  elrhmunit  27680  rearchi  27702  unitdivcld  27753  esumlub  27938  esumfsup  27946  esumcvg  27962  dya2ub  28111  itgeq12dv  28138  oddpwdc  28163  eulerpartlems  28169  prob01  28222  orvcval  28266  ballotlemfc0  28301  ballotlemfcc  28302  ballotleme  28305  ballotlem4  28307  ballotlem1c  28316  ballotlemsval  28317  ballotlemieq  28325  sgnmulsgp  28359  signsply0  28378  signslema  28389  signsvfpn  28412  lgamgulmlem1  28441  lgamgulmlem2  28442  lgamgulmlem3  28443  lgamgulmlem5  28445  lgambdd  28449  lgamcvglem  28452  erdszelem8  28512  erdsze2lem2  28518  abs2sqle  28916  abs2sqlt  28917  possumd  28987  pdivsq  29146  dvdspw  29147  poseq  29305  soseq  29306  sltval  29379  cgrdegen  29626  brofs  29627  segconeu  29633  btwntriv2  29634  transportprops  29656  brifs  29665  ifscgr  29666  brcgr3  29668  cgrxfr  29677  brcolinear2  29680  colineardim1  29683  brfs  29701  idinside  29706  btwnconn1lem11  29719  btwnconn1lem12  29720  btwnconn1lem14  29722  brsegle  29730  seglerflx  29734  seglemin  29735  segleantisym  29737  btwnsegle  29739  outsideofeu  29753  outsidele  29754  fvray  29763  ltflcei  30015  cos2h  30018  tan2h  30019  heicant  30021  mblfinlem2  30024  mblfinlem3  30025  mblfinlem4  30026  dvtanlem  30036  itg2addnclem  30038  itg2addnclem2  30039  itg2gt0cn  30042  itggt0cn  30059  ftc1anclem5  30066  dvasin  30075  areacirclem1  30079  areacirclem4  30082  areacirclem5  30083  areacirc  30084  nn0prpwlem  30112  nn0prpw  30113  seqpo  30212  incsequz2  30214  mettrifi  30222  heibor1lem  30277  rrncmslem  30300  elpell1qr2  30780  monotuz  30849  monotoddzzfi  30850  monotoddzz  30851  oddcomabszz  30852  rmxypos  30857  mzpcong  30882  congrep  30883  acongsym  30886  acongneg2  30887  acongtr  30888  acongeq12d  30889  dvdsabsmod0  30900  divalgmodcl  30901  jm2.18  30902  jm2.19lem2  30904  jm2.19lem3  30905  jm2.19lem4  30906  jm2.19  30907  jm2.25  30913  jm2.15nn0  30917  jm2.16nn0  30918  jm2.27  30922  rmydioph  30928  expdiophlem1  30935  expdiophlem2  30936  fnwe2lem2  30969  dvgrat  31166  hashnzfz  31198  evth2f  31341  evthf  31353  rfcnpre3  31359  ltaddneg  31433  sublt0d  31444  upbdrech2  31457  fmul01  31502  fmul01lt1lem1  31506  climinf  31520  climinff  31525  limcrecl  31543  limsupre  31555  limclner  31565  cncficcgt0  31598  stoweidlem3  31674  stoweidlem7  31678  stoweidlem15  31686  stoweidlem16  31687  stoweidlem18  31689  stoweidlem26  31697  stoweidlem27  31698  stoweidlem28  31699  stoweidlem31  31702  stoweidlem34  31705  stoweidlem36  31707  stoweidlem37  31708  stoweidlem41  31712  stoweidlem44  31715  stoweidlem45  31716  stoweidlem46  31717  stoweidlem48  31719  stoweidlem51  31722  stoweidlem55  31726  stoweidlem59  31730  stoweidlem60  31731  stoweidlem62  31733  fourierdlem42  31820  fourierdlem50  31828  fourierdlem54  31832  fourierdlem68  31846  fourierdlem79  31857  fourierdlem96  31874  fourierdlem97  31875  fourierdlem98  31876  fourierdlem99  31877  fourierdlem105  31883  fourierdlem108  31886  fourierdlem110  31888  fourierdlem111  31889  ltsubsubaddltsub  32162  subsubelfzo0  32176  nn0le2is012  32684  lcoop  32742  islininds  32777  ldepsnlinc  32839  lsatcv0eq  34495  oposlem  34630  oplecon1b  34649  opltcon1b  34653  atlatmstc  34767  cvlexch1  34776  cvlexch2  34777  cvlexchb2  34779  cvlatexchb2  34783  cvlatexch2  34785  cvlatcvr2  34790  cvlsupr2  34791  ishlat1  34800  hlsuprexch  34828  cvrexch  34867  cvrat  34869  atcvr0eq  34873  atcvrj0  34875  atltcvr  34882  cvrat3  34889  cvrat4  34890  cvrat42  34891  3noncolr2  34896  hlatcon2  34899  4noncolr3  34900  3dimlem1  34905  3dimlem2  34906  3dimlem3a  34907  3dimlem3  34908  3dimlem3OLDN  34909  3dimlem4a  34910  3dimlem4  34911  3dimlem4OLDN  34912  3dim1lem5  34913  3dim2  34915  3dim3  34916  ps-1  34924  ps-2  34925  3atlem5  34934  3atlem6  34935  lplni2  34984  lplnnle2at  34988  lplnnleat  34989  lplnnlelln  34990  lplnribN  34998  lplnexllnN  35011  lvoli2  35028  lvolnle3at  35029  lvolnleat  35030  lvolnlelln  35031  lvolnlelpln  35032  4atlem9  35050  4atlem10a  35051  4atlem11a  35054  4atlem11  35056  4atlem12a  35057  dalempnes  35098  dalemqnet  35099  dalem1  35106  dalemswapyzps  35137  dalemrotps  35138  dalem30  35149  dalem35  35154  lineset  35185  islinei  35187  psubspset  35191  psubspi2N  35195  snatpsubN  35197  2llnma1  35234  elpaddn0  35247  elpaddri  35249  elpaddat  35251  elpadd2at  35253  paddcom  35260  paddasslem12  35278  pmapjat1  35300  llnexchb2  35316  lhp2at0nle  35482  lhprelat3N  35487  4atexlemswapqr  35510  4atexlemcnd  35519  lautle  35531  lautcvr  35539  ltrnel  35586  ltrneq2  35595  trlnle  35634  cdlemc3  35641  cdlemd6  35651  cdleme3  35685  cdleme7aa  35690  cdleme7  35697  cdleme11c  35709  cdleme15c  35724  cdleme20yOLD  35751  cdleme20m  35772  cdleme21b  35775  cdleme21c  35776  cdleme21at  35777  cdleme36a  35909  cdleme43bN  35939  cdleme43dN  35941  cdleme46f2g2  35942  cdleme46f2g1  35943  cdlemeg46c  35962  cdlemeg46nlpq  35966  cdlemb3  36055  cdlemg4d  36062  cdlemg6d  36070  cdlemg10c  36088  cdlemg12  36099  cdlemg27b  36145  djhcvat42  36865  inductionexd  37620  leeq2d  37622  imo72b2lem0  37634  imo72b2lem2  37636  imo72b2lem1  37640  imo72b2  37645
  Copyright terms: Public domain W3C validator