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

Theorem breq2d 4292
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 4284 . 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 1362   class class class wbr 4280
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-rab 2714  df-v 2964  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-nul 3626  df-if 3780  df-sn 3866  df-pr 3868  df-op 3872  df-br 4281
This theorem is referenced by:  breqtrd  4304  sbcbr1g  4335  pofun  4644  csbfv12  5713  csbfv12gOLD  5714  isorel  6004  soisores  6005  soisoi  6006  isocnv  6008  isotr  6014  f1owe  6031  caovordig  6257  caovordg  6259  caovord  6263  f1oweALT  6550  frxp  6671  xporderlem  6672  fnwelem  6676  th3qlem2  7195  difsnen  7381  domdifsn  7382  unfilem3  7566  domunfican  7572  marypha1lem  7671  marypha1  7672  wemapwe  7916  oef1o  7918  r1sdom  7969  sdomsdomcardi  8129  alephordi  8232  pwcdadom  8373  sornom  8434  axdclem  8676  pwcfsdom  8735  elgch  8776  winalim2  8850  rankcf  8931  inatsk  8932  pinq  9083  nqereu  9085  ltaddnq  9130  ltrnq  9135  archnq  9136  addclprlem1  9172  mulclprlem  9175  1idpr  9185  ltaprlem  9200  ltapr  9201  prlem936  9203  ltasr  9254  mulgt0sr  9259  sqgt0sr  9260  map2psrpr  9264  axpre-ltadd  9321  axpre-mulgt0  9322  axpre-sup  9323  ltsubadd2  9797  lesubadd2  9799  ltaddpos2  9817  posdif  9819  lesub1  9820  ltnegcon1  9827  lenegcon1  9830  addge02  9837  leaddle0  9841  mulge0  9844  msqge0  9848  ltordlem  9852  prodgt0  10161  prodgt02  10162  prodge02  10164  ltmulgt12  10177  lemulge12  10179  mulge0b  10186  mulle0b  10187  ltdivmul  10191  ledivmul  10192  ledivmulOLD  10193  ltdivmul2  10194  lt2mul2div  10195  ledivmul2  10196  ledivmul2OLD  10197  ltrec  10200  ltrec1  10206  ltdiv23  10210  lediv23  10211  nnge1  10335  halfpos  10542  lt2halves  10546  addltmul  10547  avglt2  10550  avgle2  10552  nnrecl  10564  zltlem1  10684  gtndiv  10706  rebtwnz  10939  xrmax1  11134  max1ALT  11145  qbtwnre  11156  xralrple  11162  xltnegi  11173  xmulval  11182  xsubge0  11211  xposdif  11212  xlesubadd  11213  divelunit  11413  fllelt  11630  flbi  11647  btwnzge0  11656  dfceil2  11663  ceilval2  11664  2submod  11743  om2uzlti  11756  monoord  11819  sermono  11821  expval  11850  expnbnd  11976  discr1  11983  discr  11984  facwordi  12048  hashtpg  12169  seqcoll  12199  seqcoll2  12200  swrdccat3blem  12369  cnpart  12712  sqrlem6  12720  sqrmo  12724  resqreu  12725  resqrcl  12726  resqrthlem  12727  sqrneg  12740  sqreulem  12830  sqreu  12831  sqrthlem  12833  eqsqrd  12838  limsuple  12939  rlimcld2  13039  rlimrege0  13040  o1compt  13048  climserle  13123  caurcvgr  13134  fsum00  13243  fsumabs  13246  climcndslem2  13295  climcnds  13296  supcvg  13300  georeclim  13314  geoisumr  13320  cvgrat  13325  sin01bnd  13451  cos01bnd  13452  ruclem1  13495  ruclem9  13502  ruclem12  13505  dvdsaddr  13554  dvdssub  13555  dvdssubr  13556  dvdsfac  13570  dvdsmod  13572  oddp1even  13576  divalglem0  13579  divalglem2  13581  divalglem4  13582  divalglem5  13583  divalglem9  13587  divalg  13589  divalg2  13591  divalgmod  13592  ndvdssub  13593  ndvdsadd  13594  bitsfval  13601  bitsval  13602  bits0  13606  bitsp1  13609  bitsfzolem  13612  bitsfzo  13613  bitscmp  13616  bitsinv1lem  13619  bitsshft  13653  gcdcllem1  13677  dvdslegcd  13682  bezoutlem4  13707  dvdssqim  13719  dvdsmulgcd  13720  dvdssq  13726  nn0seqcvgd  13727  coprmdvds  13770  coprmdvds2  13771  isprm6  13777  prmdvdsexp  13782  prmdvdsexpr  13784  prmfac1  13786  divgcdodd  13787  rpmul  13791  hashdvds  13832  phiprmpw  13833  eulerthlem2  13839  prmdiv  13842  prmdiveq  13843  odzval  13845  odzcllem  13846  odzdvds  13849  opoe  13860  omoe  13861  pythagtriplem11  13874  pythagtriplem13  13876  pythagtrip  13883  pceulem  13894  pczndvds2  13915  pcdvdsb  13917  pc2dvds  13927  pcz  13929  pcprmpw2  13930  pcaddlem  13932  pcmpt  13936  prmpwdvds  13947  pockthlem  13948  prmreclem2  13960  prmreclem4  13962  4sqlem11  13998  vdwlem9  14032  rami  14058  ramlb  14062  0ram  14063  ramz2  14067  ramub1lem1  14069  imasleval  14461  subsubc  14745  pospo  15125  mulgval  15608  oddvdsnn0  16026  odmulg  16036  pgpfi1  16073  pgpfi  16083  slwispgp  16089  pgpssslw  16092  subgslw  16094  sylow2alem2  16096  sylow2blem3  16100  fislw  16103  efgi  16195  efgval2  16200  efgsrel  16210  efgredlemb  16222  lt6abl  16350  dprdval  16458  dprdvalOLD  16460  dprd2dlem2  16512  dprd2da  16514  dprd2d2  16516  ablfacrplem  16539  ablfac1a  16543  ablfac1b  16544  ablfac1eulem  16546  ablfac1eu  16547  pgpfac1lem3a  16550  ablfaclem3  16561  dvdsrtr  16677  dvdsrmul1  16678  unitpropd  16722  isabvd  16828  mplval  17434  ressmplbas2  17467  mplbaspropd  17588  zndvds0  17824  znunit  17837  cygth  17845  frlmup1  18067  lmisfree  18112  hmphindis  19211  ordthmeolem  19215  psmettri2  19726  ismet2  19749  xmettri2  19756  imasdsf1olem  19789  imasf1oxmet  19791  comet  19929  stdbdxmet  19931  nmogelb  20136  nmolb  20137  metdsge  20266  metdseq0  20271  iihalf2  20346  bndth  20371  evth  20372  ipcau2  20590  tchcphlem1  20591  tchcphlem2  20592  iscau3  20630  iscmet3  20645  bcthlem1  20676  bcth  20681  minveclem3b  20756  minveclem3  20757  minveclem4  20760  minveclem5  20761  pjthlem1  20765  pjthlem2  20766  pmltpclem1  20773  pmltpc  20775  ivthlem2  20777  ivthlem3  20778  ovolgelb  20804  ovolunlem1  20821  ovoliunlem2  20827  ovolshftlem1  20833  ovolscalem1  20837  ovolicc1  20840  ovolicc2lem3  20843  ioombl1lem4  20883  mbfmulc2lem  20966  mbfposb  20972  mbfaddlem  20979  mbfsup  20983  mbfinf  20984  mbflimsup  20985  i1fposd  21026  itg1ge0a  21030  mbfi1fseqlem4  21037  mbfi1fseqlem6  21039  mbfi1flimlem  21041  mbfi1flim  21042  itg2const2  21060  itg2seq  21061  itg2monolem1  21069  itg2i1fseq  21074  itg2addlem  21077  ibllem  21083  isibl  21084  isibl2  21085  iblitg  21087  dfitg  21088  cbvitg  21094  itgeq2  21096  itgvallem  21103  iblneg  21121  itgneg  21122  itggt0  21160  dvlip  21306  c1lip1  21310  dvfsumle  21334  dvfsumlem2  21340  dvfsumlem4  21342  dvfsum2  21347  mdeglt  21420  degltp1le  21428  deg1suble  21463  ply1divex  21492  plypf1  21564  dgrlb  21588  coemulc  21606  dgrsub  21623  quotval  21642  plydivlem4  21646  quotcan  21659  vieta1lem2  21661  aalioulem2  21683  aaliou3lem9  21700  ulmcn  21748  dvradcnv  21770  sincosq1sgn  21844  sincosq2sgn  21845  sincosq4sgn  21847  logltb  21932  cxpge0  22012  cxple2  22026  logreclem  22098  jensen  22266  emcllem7  22279  wilthlem1  22290  ftalem2  22295  ftalem3  22296  ftalem7  22300  fta  22301  sgmval  22364  mumul  22403  dvdsppwf1o  22410  musum  22415  chtublem  22434  chtub  22435  perfect1  22451  bcmono  22500  bclbnd  22503  bposlem1  22507  bposlem5  22511  lgslem1  22519  lgsval  22523  lgsdilem  22545  lgsne0  22556  lgsqrlem2  22565  lgsqrlem4  22567  lgseisenlem1  22572  lgseisenlem2  22573  lgsquadlem1  22577  lgsquadlem2  22578  lgsquadlem3  22579  lgsquad2lem2  22582  m1lgs  22585  2sqlem4  22590  2sqlem8a  22594  2sqblem  22600  dchrisumlema  22621  dchrisumlem2  22623  dchrisumlem3  22624  chpdifbndlem2  22687  pntrsumbnd2  22700  pntpbnd1  22719  pntibndlem3  22725  pntlemi  22737  pntleme  22741  pntlem3  22742  pnt3  22745  ostth2lem2  22767  ostth3  22771  ostth  22772  tgcgrxfr  22850  legtrid  22897  brbtwn2  22973  axlowdim2  23028  axlowdim  23029  axcontlem2  23033  axcontlem3  23034  axcontlem4  23035  axcontlem9  23040  axcontlem10  23041  axcontlem11  23042  axcontlem12  23043  ebtwntg  23050  eupath2lem3  23422  eupath2  23423  konigsberg  23430  nmounbseqi  23999  nmounbseqiOLD  24000  isblo3i  24023  blo3i  24024  blocnilem  24026  siilem2  24074  normlem6  24339  normgt0  24351  norm3dif  24374  norm3lemt  24376  pjhthlem1  24616  pjige0  24916  nmcexi  25252  lnconi  25259  lnopcnbd  25262  lnfncnbd  25283  riesz1  25291  cnlnadjlem2  25294  cnlnadjlem8  25300  leopg  25348  leop2  25350  leoppos  25352  leopadd  25358  leopmuli  25359  leopmul2i  25361  pjssge0i  25392  pjdifnormi  25393  pjssposi  25398  pjssdif1i  25401  chcv1  25581  cvexch  25600  atcvatlem  25611  atcvat3i  25622  atdmd  25624  cdj3i  25667  addltmulALT  25672  xrofsup  25877  xrge0addgt0  25976  omndadd  25992  omndmul2  25998  ogrpinvlt  26010  isarchi3  26027  archirng  26028  archirngz  26029  archiexdiv  26030  isorng  26119  orngmul  26123  ofldchr  26134  isarchiofld  26137  elrhmunit  26140  rearchi  26163  unitdivcld  26184  esumlub  26364  esumfsup  26372  esumcvg  26388  dya2ub  26538  itgeq12dv  26559  oddpwdc  26584  eulerpartlems  26590  prob01  26643  orvcval  26687  ballotlemfc0  26722  ballotlemfcc  26723  ballotleme  26726  ballotlem4  26728  ballotlem1c  26737  ballotlemsval  26738  ballotlemieq  26746  sgnmulsgp  26780  signsply0  26799  signslema  26810  signsvfpn  26833  lgamgulmlem1  26862  lgamgulmlem2  26863  lgamgulmlem3  26864  lgamgulmlem5  26866  lgambdd  26870  lgamcvglem  26873  erdszelem8  26933  erdsze2lem2  26939  abs2sqle  27171  abs2sqlt  27172  possumd  27242  pdivsq  27401  dvdspw  27402  poseq  27560  soseq  27561  sltval  27634  cgrdegen  27881  brofs  27882  segconeu  27888  btwntriv2  27889  transportprops  27911  brifs  27920  ifscgr  27921  brcgr3  27923  cgrxfr  27932  brcolinear2  27935  colineardim1  27938  brfs  27956  idinside  27961  btwnconn1lem11  27974  btwnconn1lem12  27975  btwnconn1lem14  27977  brsegle  27985  seglerflx  27989  seglemin  27990  segleantisym  27992  btwnsegle  27994  outsideofeu  28008  outsidele  28009  fvray  28018  ltflcei  28260  lxflflp1  28262  cos2h  28264  tan2h  28265  heicant  28267  mblfinlem2  28270  mblfinlem3  28271  mblfinlem4  28272  dvtanlem  28282  itg2addnclem  28284  itg2addnclem2  28285  itg2gt0cn  28288  itggt0cn  28305  ftc1anclem5  28312  dvasin  28321  areacirclem1  28325  areacirclem4  28328  areacirclem5  28329  areacirc  28330  nn0prpwlem  28358  nn0prpw  28359  seqpo  28484  incsequz2  28486  mettrifi  28494  heibor1lem  28549  rrncmslem  28572  elpell1qr2  29055  monotuz  29124  monotoddzzfi  29125  monotoddzz  29126  oddcomabszz  29127  rmxypos  29132  mzpcong  29157  congrep  29158  acongsym  29161  acongneg2  29162  acongtr  29163  acongeq12d  29164  dvdsabsmod0  29177  divalgmodcl  29178  jm2.18  29179  jm2.19lem2  29181  jm2.19lem3  29182  jm2.19lem4  29183  jm2.19  29184  jm2.25  29190  jm2.15nn0  29194  jm2.16nn0  29195  jm2.27  29199  rmydioph  29205  expdiophlem1  29212  expdiophlem2  29213  fnwe2lem2  29246  evth2f  29579  evthf  29591  rfcnpre3  29597  fmul01  29603  fmul01lt1lem1  29607  climinf  29622  climinff  29627  stoweidlem3  29641  stoweidlem7  29645  stoweidlem15  29653  stoweidlem16  29654  stoweidlem18  29656  stoweidlem26  29664  stoweidlem27  29665  stoweidlem28  29666  stoweidlem31  29669  stoweidlem34  29672  stoweidlem36  29674  stoweidlem37  29675  stoweidlem41  29679  stoweidlem44  29682  stoweidlem45  29683  stoweidlem46  29684  stoweidlem48  29686  stoweidlem51  29689  stoweidlem55  29693  stoweidlem59  29697  stoweidlem60  29698  stoweidlem62  29700  nn01to3  30030  subsubelfzo0  30053  eluzgtdifelfzo  30062  clwlkisclwwlklem2a4  30289  clwlkisclwwlklem2a  30290  ltsubsubaddltsub  30310  nbhashuvtx1  30376  frgrareggt1  30552  nn0le2is012  30594  lcoop  30651  islininds  30686  ldepsnlinc  30756  lsatcv0eq  32262  oposlem  32397  oplecon1b  32416  opltcon1b  32420  atlatmstc  32534  cvlexch1  32543  cvlexch2  32544  cvlexchb2  32546  cvlatexchb2  32550  cvlatexch2  32552  cvlatcvr2  32557  cvlsupr2  32558  ishlat1  32567  hlsuprexch  32595  cvrexch  32634  cvrat  32636  atcvr0eq  32640  atcvrj0  32642  atltcvr  32649  cvrat3  32656  cvrat4  32657  cvrat42  32658  3noncolr2  32663  hlatcon2  32666  4noncolr3  32667  3dimlem1  32672  3dimlem2  32673  3dimlem3a  32674  3dimlem3  32675  3dimlem3OLDN  32676  3dimlem4a  32677  3dimlem4  32678  3dimlem4OLDN  32679  3dim1lem5  32680  3dim2  32682  3dim3  32683  ps-1  32691  ps-2  32692  3atlem5  32701  3atlem6  32702  lplni2  32751  lplnnle2at  32755  lplnnleat  32756  lplnnlelln  32757  lplnribN  32765  lplnexllnN  32778  lvoli2  32795  lvolnle3at  32796  lvolnleat  32797  lvolnlelln  32798  lvolnlelpln  32799  4atlem9  32817  4atlem10a  32818  4atlem11a  32821  4atlem11  32823  4atlem12a  32824  dalempnes  32865  dalemqnet  32866  dalem1  32873  dalemswapyzps  32904  dalemrotps  32905  dalem30  32916  dalem35  32921  lineset  32952  islinei  32954  psubspset  32958  psubspi2N  32962  snatpsubN  32964  2llnma1  33001  elpaddn0  33014  elpaddri  33016  elpaddat  33018  elpadd2at  33020  paddcom  33027  paddasslem12  33045  pmapjat1  33067  llnexchb2  33083  lhp2at0nle  33249  lhprelat3N  33254  4atexlemswapqr  33277  4atexlemcnd  33286  lautle  33298  lautcvr  33306  ltrnel  33353  ltrneq2  33362  trlnle  33400  cdlemc3  33407  cdlemd6  33417  cdleme3  33451  cdleme7aa  33456  cdleme7  33463  cdleme11c  33475  cdleme15c  33490  cdleme20y  33516  cdleme20m  33537  cdleme21b  33540  cdleme21c  33541  cdleme21at  33542  cdleme36a  33674  cdleme43bN  33704  cdleme43dN  33706  cdleme46f2g2  33707  cdleme46f2g1  33708  cdlemeg46c  33727  cdlemeg46nlpq  33731  cdlemb3  33820  cdlemg4d  33827  cdlemg6d  33835  cdlemg10c  33853  cdlemg12  33864  cdlemg27b  33910  djhcvat42  34630
  Copyright terms: Public domain W3C validator