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

Theorem breq2d 4459
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 4451 . 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 1379   class class class wbr 4447
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-rab 2823  df-v 3115  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-sn 4028  df-pr 4030  df-op 4034  df-br 4448
This theorem is referenced by:  breqtrd  4471  sbcbr1g  4502  pofun  4816  csbfv12  5899  csbfv12gOLD  5900  isorel  6208  soisores  6209  soisoi  6210  isocnv  6212  isotr  6218  f1owe  6235  caovordig  6462  caovordg  6464  caovord  6468  f1oweALT  6765  frxp  6890  xporderlem  6891  fnwelem  6895  difsnen  7596  domdifsn  7597  unfilem3  7782  domunfican  7789  marypha1lem  7889  marypha1  7890  wemapwe  8135  oef1o  8137  r1sdom  8188  sdomsdomcardi  8348  alephordi  8451  pwcdadom  8592  sornom  8653  axdclem  8895  pwcfsdom  8954  elgch  8996  winalim2  9070  rankcf  9151  inatsk  9152  pinq  9301  nqereu  9303  ltaddnq  9348  ltrnq  9353  archnq  9354  addclprlem1  9390  mulclprlem  9393  1idpr  9403  ltaprlem  9418  ltapr  9419  prlem936  9421  ltasr  9473  mulgt0sr  9478  sqgt0sr  9479  map2psrpr  9483  axpre-ltadd  9540  axpre-mulgt0  9541  axpre-sup  9542  ltsubadd2  10019  lesubadd2  10021  ltaddpos2  10039  posdif  10041  lesub1  10042  ltnegcon1  10049  lenegcon1  10052  addge02  10059  leaddle0  10063  mulge0  10066  msqge0  10070  ltordlem  10074  prodgt0  10383  prodgt02  10384  prodge02  10386  ltmulgt12  10399  lemulge12  10401  mulge0b  10408  mulle0b  10409  ltdivmul  10413  ledivmul  10414  ledivmulOLD  10415  ltdivmul2  10416  lt2mul2div  10417  ledivmul2  10418  ledivmul2OLD  10419  ltrec  10422  ltrec1  10428  ltdiv23  10432  lediv23  10433  nnge1  10558  halfpos  10765  lt2halves  10769  addltmul  10770  avglt2  10773  avgle2  10775  nnrecl  10789  zltlem1  10911  gtndiv  10934  nn01to3  11171  rebtwnz  11177  xrmax1  11372  max1ALT  11383  qbtwnre  11394  xralrple  11400  xltnegi  11411  xmulval  11420  xsubge0  11449  xposdif  11450  xlesubadd  11451  divelunit  11658  eluzgtdifelfzo  11842  fllelt  11898  flflp1  11908  flbi  11916  btwnzge0  11925  dfceil2  11932  ceilval2  11933  2submod  12012  om2uzlti  12025  monoord  12101  sermono  12103  expval  12132  expnbnd  12259  discr1  12266  discr  12267  facwordi  12331  seqcoll  12474  seqcoll2  12475  hashtpg  12485  swrdccat3blem  12679  cnpart  13032  sqrlem6  13040  sqrmo  13044  resqreu  13045  resqrtcl  13046  resqrtthlem  13047  sqrtneg  13060  sqreulem  13151  sqreu  13152  sqrtthlem  13154  eqsqrtd  13159  limsuple  13260  rlimcld2  13360  rlimrege0  13361  o1compt  13369  climserle  13444  caurcvgr  13455  fsum00  13571  fsumabs  13574  climcndslem2  13621  climcnds  13622  supcvg  13626  georeclim  13640  geoisumr  13646  cvgrat  13651  sin01bnd  13777  cos01bnd  13778  ruclem1  13821  ruclem9  13828  ruclem12  13831  dvdsaddr  13880  dvdssub  13881  dvdssubr  13882  dvdsfac  13896  dvdsmod  13898  oddp1even  13903  divalglem0  13906  divalglem2  13908  divalglem4  13909  divalglem5  13910  divalglem9  13914  divalg  13916  divalg2  13918  divalgmod  13919  ndvdssub  13920  ndvdsadd  13921  bitsfval  13928  bitsval  13929  bits0  13933  bitsp1  13936  bitsfzolem  13939  bitsfzo  13940  bitscmp  13943  bitsinv1lem  13946  bitsshft  13980  gcdcllem1  14004  dvdslegcd  14009  bezoutlem4  14034  dvdssqim  14046  dvdsmulgcd  14047  dvdssq  14053  nn0seqcvgd  14054  coprmdvds  14098  coprmdvds2  14099  isprm6  14105  prmdvdsexp  14110  prmdvdsexpr  14112  prmfac1  14114  divgcdodd  14115  rpmul  14119  hashdvds  14160  phiprmpw  14161  eulerthlem2  14167  prmdiv  14170  prmdiveq  14171  odzval  14173  odzcllem  14174  odzdvds  14177  opoe  14190  omoe  14191  pythagtriplem11  14204  pythagtriplem13  14206  pythagtrip  14213  pceulem  14224  pczndvds2  14245  pcdvdsb  14247  pc2dvds  14257  pcz  14259  pcprmpw2  14260  pcaddlem  14262  pcmpt  14266  prmpwdvds  14277  pockthlem  14278  prmreclem2  14290  prmreclem4  14292  4sqlem11  14328  vdwlem9  14362  rami  14388  ramlb  14392  0ram  14393  ramz2  14397  ramub1lem1  14399  imasleval  14792  subsubc  15076  pospo  15456  mulgval  15944  oddvdsnn0  16364  odmulg  16374  pgpfi1  16411  pgpfi  16421  slwispgp  16427  pgpssslw  16430  subgslw  16432  sylow2alem2  16434  sylow2blem3  16438  fislw  16441  efgi  16533  efgval2  16538  efgsrel  16548  efgredlemb  16560  lt6abl  16688  telgsums  16813  dprdval  16825  dprdvalOLD  16827  dprd2dlem2  16879  dprd2da  16881  dprd2d2  16883  ablfacrplem  16906  ablfac1a  16910  ablfac1b  16911  ablfac1eulem  16913  ablfac1eu  16914  pgpfac1lem3a  16917  ablfaclem3  16928  dvdsrtr  17085  dvdsrmul1  17086  unitpropd  17130  isabvd  17252  mplval  17855  ressmplbas2  17888  mplbaspropd  18049  zndvds0  18356  znunit  18369  cygth  18377  frlmup1  18599  lmisfree  18644  pmatcoe1fsupp  18969  fvmptnn04if  19117  hmphindis  20033  ordthmeolem  20037  psmettri2  20548  ismet2  20571  xmettri2  20578  imasdsf1olem  20611  imasf1oxmet  20613  comet  20751  stdbdxmet  20753  nmogelb  20958  nmolb  20959  metdsge  21088  metdseq0  21093  iihalf2  21168  bndth  21193  evth  21194  ipcau2  21412  tchcphlem1  21413  tchcphlem2  21414  iscau3  21452  iscmet3  21467  bcthlem1  21498  bcth  21503  minveclem3b  21578  minveclem3  21579  minveclem4  21582  minveclem5  21583  pjthlem1  21587  pjthlem2  21588  pmltpclem1  21595  pmltpc  21597  ivthlem2  21599  ivthlem3  21600  ovolgelb  21626  ovolunlem1  21643  ovoliunlem2  21649  ovolshftlem1  21655  ovolscalem1  21659  ovolicc1  21662  ovolicc2lem3  21665  ioombl1lem4  21706  mbfmulc2lem  21789  mbfposb  21795  mbfaddlem  21802  mbfsup  21806  mbfinf  21807  mbflimsup  21808  i1fposd  21849  itg1ge0a  21853  mbfi1fseqlem4  21860  mbfi1fseqlem6  21862  mbfi1flimlem  21864  mbfi1flim  21865  itg2const2  21883  itg2seq  21884  itg2monolem1  21892  itg2i1fseq  21897  itg2addlem  21900  ibllem  21906  isibl  21907  isibl2  21908  iblitg  21910  dfitg  21911  cbvitg  21917  itgeq2  21919  itgvallem  21926  iblneg  21944  itgneg  21945  itggt0  21983  dvlip  22129  c1lip1  22133  dvfsumle  22157  dvfsumlem2  22163  dvfsumlem4  22165  dvfsum2  22170  mdeglt  22200  degltp1le  22208  deg1suble  22243  ply1divex  22272  plypf1  22344  dgrlb  22368  coemulc  22386  dgrsub  22403  quotval  22422  plydivlem4  22426  quotcan  22439  vieta1lem2  22441  aalioulem2  22463  aaliou3lem9  22480  ulmcn  22528  dvradcnv  22550  sincosq1sgn  22624  sincosq2sgn  22625  sincosq4sgn  22627  logltb  22712  cxpge0  22792  cxple2  22806  logreclem  22878  jensen  23046  emcllem7  23059  wilthlem1  23070  ftalem2  23075  ftalem3  23076  ftalem7  23080  fta  23081  sgmval  23144  mumul  23183  dvdsppwf1o  23190  musum  23195  chtublem  23214  chtub  23215  perfect1  23231  bcmono  23280  bclbnd  23283  bposlem1  23287  bposlem5  23291  lgslem1  23299  lgsval  23303  lgsdilem  23325  lgsne0  23336  lgsqrlem2  23345  lgsqrlem4  23347  lgseisenlem1  23352  lgseisenlem2  23353  lgsquadlem1  23357  lgsquadlem2  23358  lgsquadlem3  23359  lgsquad2lem2  23362  m1lgs  23365  2sqlem4  23370  2sqlem8a  23374  2sqblem  23380  dchrisumlema  23401  dchrisumlem2  23403  dchrisumlem3  23404  chpdifbndlem2  23467  pntrsumbnd2  23480  pntpbnd1  23499  pntibndlem3  23505  pntlemi  23517  pntleme  23521  pntlem3  23522  pnt3  23525  ostth2lem2  23547  ostth3  23551  ostth  23552  tgcgrxfr  23637  legtrid  23705  islmib  23830  lmicom  23831  brbtwn2  23884  axlowdim2  23939  axlowdim  23940  axcontlem2  23944  axcontlem3  23945  axcontlem4  23946  axcontlem9  23951  axcontlem10  23952  axcontlem11  23953  axcontlem12  23954  ebtwntg  23961  ausisusgraedg  24032  clwlkisclwwlklem2a4  24460  clwlkisclwwlklem2a  24461  nbhashuvtx1  24591  eupath2lem3  24655  eupath2  24656  konigsberg  24663  frgrareggt1  24793  nmounbseqi  25368  nmounbseqiOLD  25369  isblo3i  25392  blo3i  25393  blocnilem  25395  siilem2  25443  normlem6  25708  normgt0  25720  norm3dif  25743  norm3lemt  25745  pjhthlem1  25985  pjige0  26285  nmcexi  26621  lnconi  26628  lnopcnbd  26631  lnfncnbd  26652  riesz1  26660  cnlnadjlem2  26663  cnlnadjlem8  26669  leopg  26717  leop2  26719  leoppos  26721  leopadd  26727  leopmuli  26728  leopmul2i  26730  pjssge0i  26761  pjdifnormi  26762  pjssposi  26767  pjssdif1i  26770  chcv1  26950  cvexch  26969  atcvatlem  26980  atcvat3i  26991  atdmd  26993  cdj3i  27036  addltmulALT  27041  xrofsup  27250  xrge0addgt0  27343  omndadd  27358  omndmul2  27364  ogrpinvlt  27376  isarchi3  27393  archirng  27394  archirngz  27395  archiexdiv  27396  isorng  27452  orngmul  27456  ofldchr  27467  isarchiofld  27470  elrhmunit  27473  rearchi  27495  unitdivcld  27519  esumlub  27708  esumfsup  27716  esumcvg  27732  dya2ub  27881  itgeq12dv  27908  oddpwdc  27933  eulerpartlems  27939  prob01  27992  orvcval  28036  ballotlemfc0  28071  ballotlemfcc  28072  ballotleme  28075  ballotlem4  28077  ballotlem1c  28086  ballotlemsval  28087  ballotlemieq  28095  sgnmulsgp  28129  signsply0  28148  signslema  28159  signsvfpn  28182  lgamgulmlem1  28211  lgamgulmlem2  28212  lgamgulmlem3  28213  lgamgulmlem5  28215  lgambdd  28219  lgamcvglem  28222  erdszelem8  28282  erdsze2lem2  28288  abs2sqle  28521  abs2sqlt  28522  possumd  28592  pdivsq  28751  dvdspw  28752  poseq  28910  soseq  28911  sltval  28984  cgrdegen  29231  brofs  29232  segconeu  29238  btwntriv2  29239  transportprops  29261  brifs  29270  ifscgr  29271  brcgr3  29273  cgrxfr  29282  brcolinear2  29285  colineardim1  29288  brfs  29306  idinside  29311  btwnconn1lem11  29324  btwnconn1lem12  29325  btwnconn1lem14  29327  brsegle  29335  seglerflx  29339  seglemin  29340  segleantisym  29342  btwnsegle  29344  outsideofeu  29358  outsidele  29359  fvray  29368  ltflcei  29620  cos2h  29623  tan2h  29624  heicant  29626  mblfinlem2  29629  mblfinlem3  29630  mblfinlem4  29631  dvtanlem  29641  itg2addnclem  29643  itg2addnclem2  29644  itg2gt0cn  29647  itggt0cn  29664  ftc1anclem5  29671  dvasin  29680  areacirclem1  29684  areacirclem4  29687  areacirclem5  29688  areacirc  29689  nn0prpwlem  29717  nn0prpw  29718  seqpo  29843  incsequz2  29845  mettrifi  29853  heibor1lem  29908  rrncmslem  29931  elpell1qr2  30412  monotuz  30481  monotoddzzfi  30482  monotoddzz  30483  oddcomabszz  30484  rmxypos  30489  mzpcong  30514  congrep  30515  acongsym  30518  acongneg2  30519  acongtr  30520  acongeq12d  30521  dvdsabsmod0  30532  divalgmodcl  30533  jm2.18  30534  jm2.19lem2  30536  jm2.19lem3  30537  jm2.19lem4  30538  jm2.19  30539  jm2.25  30545  jm2.15nn0  30549  jm2.16nn0  30550  jm2.27  30554  rmydioph  30560  expdiophlem1  30567  expdiophlem2  30568  fnwe2lem2  30601  hashnzfz  30825  evth2f  30968  evthf  30980  rfcnpre3  30986  ltaddneg  31061  sublt0d  31072  upbdrech2  31085  fmul01  31130  fmul01lt1lem1  31134  climinf  31148  climinff  31153  limcrecl  31171  limsupre  31183  limclner  31193  cncficcgt0  31227  volge0  31279  stoweidlem3  31303  stoweidlem7  31307  stoweidlem15  31315  stoweidlem16  31316  stoweidlem18  31318  stoweidlem26  31326  stoweidlem27  31327  stoweidlem28  31328  stoweidlem31  31331  stoweidlem34  31334  stoweidlem36  31336  stoweidlem37  31337  stoweidlem41  31341  stoweidlem44  31344  stoweidlem45  31345  stoweidlem46  31346  stoweidlem48  31348  stoweidlem51  31351  stoweidlem55  31355  stoweidlem59  31359  stoweidlem60  31360  stoweidlem62  31362  fourierdlem24  31431  fourierdlem42  31449  fourierdlem50  31457  fourierdlem54  31461  fourierdlem68  31475  fourierdlem79  31486  fourierdlem82  31489  fourierdlem93  31500  fourierdlem96  31503  fourierdlem97  31504  fourierdlem98  31505  fourierdlem99  31506  fourierdlem103  31510  fourierdlem104  31511  fourierdlem105  31512  fourierdlem108  31515  fourierdlem110  31517  fourierdlem111  31518  ltsubsubaddltsub  31793  subsubelfzo0  31807  nn0le2is012  32021  lcoop  32085  islininds  32120  ldepsnlinc  32190  lsatcv0eq  33844  oposlem  33979  oplecon1b  33998  opltcon1b  34002  atlatmstc  34116  cvlexch1  34125  cvlexch2  34126  cvlexchb2  34128  cvlatexchb2  34132  cvlatexch2  34134  cvlatcvr2  34139  cvlsupr2  34140  ishlat1  34149  hlsuprexch  34177  cvrexch  34216  cvrat  34218  atcvr0eq  34222  atcvrj0  34224  atltcvr  34231  cvrat3  34238  cvrat4  34239  cvrat42  34240  3noncolr2  34245  hlatcon2  34248  4noncolr3  34249  3dimlem1  34254  3dimlem2  34255  3dimlem3a  34256  3dimlem3  34257  3dimlem3OLDN  34258  3dimlem4a  34259  3dimlem4  34260  3dimlem4OLDN  34261  3dim1lem5  34262  3dim2  34264  3dim3  34265  ps-1  34273  ps-2  34274  3atlem5  34283  3atlem6  34284  lplni2  34333  lplnnle2at  34337  lplnnleat  34338  lplnnlelln  34339  lplnribN  34347  lplnexllnN  34360  lvoli2  34377  lvolnle3at  34378  lvolnleat  34379  lvolnlelln  34380  lvolnlelpln  34381  4atlem9  34399  4atlem10a  34400  4atlem11a  34403  4atlem11  34405  4atlem12a  34406  dalempnes  34447  dalemqnet  34448  dalem1  34455  dalemswapyzps  34486  dalemrotps  34487  dalem30  34498  dalem35  34503  lineset  34534  islinei  34536  psubspset  34540  psubspi2N  34544  snatpsubN  34546  2llnma1  34583  elpaddn0  34596  elpaddri  34598  elpaddat  34600  elpadd2at  34602  paddcom  34609  paddasslem12  34627  pmapjat1  34649  llnexchb2  34665  lhp2at0nle  34831  lhprelat3N  34836  4atexlemswapqr  34859  4atexlemcnd  34868  lautle  34880  lautcvr  34888  ltrnel  34935  ltrneq2  34944  trlnle  34982  cdlemc3  34989  cdlemd6  34999  cdleme3  35033  cdleme7aa  35038  cdleme7  35045  cdleme11c  35057  cdleme15c  35072  cdleme20y  35098  cdleme20m  35119  cdleme21b  35122  cdleme21c  35123  cdleme21at  35124  cdleme36a  35256  cdleme43bN  35286  cdleme43dN  35288  cdleme46f2g2  35289  cdleme46f2g1  35290  cdlemeg46c  35309  cdlemeg46nlpq  35313  cdlemb3  35402  cdlemg4d  35409  cdlemg6d  35417  cdlemg10c  35435  cdlemg12  35446  cdlemg27b  35492  djhcvat42  36212
  Copyright terms: Public domain W3C validator