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

Theorem breq2d 4402
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 4394 . 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 1370   class class class wbr 4390
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-rab 2804  df-v 3070  df-dif 3429  df-un 3431  df-in 3433  df-ss 3440  df-nul 3736  df-if 3890  df-sn 3976  df-pr 3978  df-op 3982  df-br 4391
This theorem is referenced by:  breqtrd  4414  sbcbr1g  4445  pofun  4755  csbfv12  5824  csbfv12gOLD  5825  isorel  6116  soisores  6117  soisoi  6118  isocnv  6120  isotr  6126  f1owe  6143  caovordig  6368  caovordg  6370  caovord  6374  f1oweALT  6661  frxp  6782  xporderlem  6783  fnwelem  6787  th3qlem2  7307  difsnen  7493  domdifsn  7494  unfilem3  7679  domunfican  7685  marypha1lem  7784  marypha1  7785  wemapwe  8029  oef1o  8031  r1sdom  8082  sdomsdomcardi  8242  alephordi  8345  pwcdadom  8486  sornom  8547  axdclem  8789  pwcfsdom  8848  elgch  8890  winalim2  8964  rankcf  9045  inatsk  9046  pinq  9197  nqereu  9199  ltaddnq  9244  ltrnq  9249  archnq  9250  addclprlem1  9286  mulclprlem  9289  1idpr  9299  ltaprlem  9314  ltapr  9315  prlem936  9317  ltasr  9368  mulgt0sr  9373  sqgt0sr  9374  map2psrpr  9378  axpre-ltadd  9435  axpre-mulgt0  9436  axpre-sup  9437  ltsubadd2  9911  lesubadd2  9913  ltaddpos2  9931  posdif  9933  lesub1  9934  ltnegcon1  9941  lenegcon1  9944  addge02  9951  leaddle0  9955  mulge0  9958  msqge0  9962  ltordlem  9966  prodgt0  10275  prodgt02  10276  prodge02  10278  ltmulgt12  10291  lemulge12  10293  mulge0b  10300  mulle0b  10301  ltdivmul  10305  ledivmul  10306  ledivmulOLD  10307  ltdivmul2  10308  lt2mul2div  10309  ledivmul2  10310  ledivmul2OLD  10311  ltrec  10314  ltrec1  10320  ltdiv23  10324  lediv23  10325  nnge1  10449  halfpos  10656  lt2halves  10660  addltmul  10661  avglt2  10664  avgle2  10666  nnrecl  10678  zltlem1  10798  gtndiv  10820  rebtwnz  11053  xrmax1  11248  max1ALT  11259  qbtwnre  11270  xralrple  11276  xltnegi  11287  xmulval  11296  xsubge0  11325  xposdif  11326  xlesubadd  11327  divelunit  11528  fllelt  11748  flbi  11765  btwnzge0  11774  dfceil2  11781  ceilval2  11782  2submod  11861  om2uzlti  11874  monoord  11937  sermono  11939  expval  11968  expnbnd  12094  discr1  12101  discr  12102  facwordi  12166  hashtpg  12288  seqcoll  12318  seqcoll2  12319  swrdccat3blem  12488  cnpart  12831  sqrlem6  12839  sqrmo  12843  resqreu  12844  resqrcl  12845  resqrthlem  12846  sqrneg  12859  sqreulem  12949  sqreu  12950  sqrthlem  12952  eqsqrd  12957  limsuple  13058  rlimcld2  13158  rlimrege0  13159  o1compt  13167  climserle  13242  caurcvgr  13253  fsum00  13363  fsumabs  13366  climcndslem2  13415  climcnds  13416  supcvg  13420  georeclim  13434  geoisumr  13440  cvgrat  13445  sin01bnd  13571  cos01bnd  13572  ruclem1  13615  ruclem9  13622  ruclem12  13625  dvdsaddr  13674  dvdssub  13675  dvdssubr  13676  dvdsfac  13690  dvdsmod  13692  oddp1even  13696  divalglem0  13699  divalglem2  13701  divalglem4  13702  divalglem5  13703  divalglem9  13707  divalg  13709  divalg2  13711  divalgmod  13712  ndvdssub  13713  ndvdsadd  13714  bitsfval  13721  bitsval  13722  bits0  13726  bitsp1  13729  bitsfzolem  13732  bitsfzo  13733  bitscmp  13736  bitsinv1lem  13739  bitsshft  13773  gcdcllem1  13797  dvdslegcd  13802  bezoutlem4  13827  dvdssqim  13839  dvdsmulgcd  13840  dvdssq  13846  nn0seqcvgd  13847  coprmdvds  13890  coprmdvds2  13891  isprm6  13897  prmdvdsexp  13902  prmdvdsexpr  13904  prmfac1  13906  divgcdodd  13907  rpmul  13911  hashdvds  13952  phiprmpw  13953  eulerthlem2  13959  prmdiv  13962  prmdiveq  13963  odzval  13965  odzcllem  13966  odzdvds  13969  opoe  13980  omoe  13981  pythagtriplem11  13994  pythagtriplem13  13996  pythagtrip  14003  pceulem  14014  pczndvds2  14035  pcdvdsb  14037  pc2dvds  14047  pcz  14049  pcprmpw2  14050  pcaddlem  14052  pcmpt  14056  prmpwdvds  14067  pockthlem  14068  prmreclem2  14080  prmreclem4  14082  4sqlem11  14118  vdwlem9  14152  rami  14178  ramlb  14182  0ram  14183  ramz2  14187  ramub1lem1  14189  imasleval  14581  subsubc  14865  pospo  15245  mulgval  15731  oddvdsnn0  16151  odmulg  16161  pgpfi1  16198  pgpfi  16208  slwispgp  16214  pgpssslw  16217  subgslw  16219  sylow2alem2  16221  sylow2blem3  16225  fislw  16228  efgi  16320  efgval2  16325  efgsrel  16335  efgredlemb  16347  lt6abl  16475  dprdval  16590  dprdvalOLD  16592  dprd2dlem2  16644  dprd2da  16646  dprd2d2  16648  ablfacrplem  16671  ablfac1a  16675  ablfac1b  16676  ablfac1eulem  16678  ablfac1eu  16679  pgpfac1lem3a  16682  ablfaclem3  16693  dvdsrtr  16850  dvdsrmul1  16851  unitpropd  16895  isabvd  17011  mplval  17608  ressmplbas2  17641  mplbaspropd  17798  zndvds0  18092  znunit  18105  cygth  18113  frlmup1  18335  lmisfree  18380  hmphindis  19486  ordthmeolem  19490  psmettri2  20001  ismet2  20024  xmettri2  20031  imasdsf1olem  20064  imasf1oxmet  20066  comet  20204  stdbdxmet  20206  nmogelb  20411  nmolb  20412  metdsge  20541  metdseq0  20546  iihalf2  20621  bndth  20646  evth  20647  ipcau2  20865  tchcphlem1  20866  tchcphlem2  20867  iscau3  20905  iscmet3  20920  bcthlem1  20951  bcth  20956  minveclem3b  21031  minveclem3  21032  minveclem4  21035  minveclem5  21036  pjthlem1  21040  pjthlem2  21041  pmltpclem1  21048  pmltpc  21050  ivthlem2  21052  ivthlem3  21053  ovolgelb  21079  ovolunlem1  21096  ovoliunlem2  21102  ovolshftlem1  21108  ovolscalem1  21112  ovolicc1  21115  ovolicc2lem3  21118  ioombl1lem4  21158  mbfmulc2lem  21241  mbfposb  21247  mbfaddlem  21254  mbfsup  21258  mbfinf  21259  mbflimsup  21260  i1fposd  21301  itg1ge0a  21305  mbfi1fseqlem4  21312  mbfi1fseqlem6  21314  mbfi1flimlem  21316  mbfi1flim  21317  itg2const2  21335  itg2seq  21336  itg2monolem1  21344  itg2i1fseq  21349  itg2addlem  21352  ibllem  21358  isibl  21359  isibl2  21360  iblitg  21362  dfitg  21363  cbvitg  21369  itgeq2  21371  itgvallem  21378  iblneg  21396  itgneg  21397  itggt0  21435  dvlip  21581  c1lip1  21585  dvfsumle  21609  dvfsumlem2  21615  dvfsumlem4  21617  dvfsum2  21622  mdeglt  21652  degltp1le  21660  deg1suble  21695  ply1divex  21724  plypf1  21796  dgrlb  21820  coemulc  21838  dgrsub  21855  quotval  21874  plydivlem4  21878  quotcan  21891  vieta1lem2  21893  aalioulem2  21915  aaliou3lem9  21932  ulmcn  21980  dvradcnv  22002  sincosq1sgn  22076  sincosq2sgn  22077  sincosq4sgn  22079  logltb  22164  cxpge0  22244  cxple2  22258  logreclem  22330  jensen  22498  emcllem7  22511  wilthlem1  22522  ftalem2  22527  ftalem3  22528  ftalem7  22532  fta  22533  sgmval  22596  mumul  22635  dvdsppwf1o  22642  musum  22647  chtublem  22666  chtub  22667  perfect1  22683  bcmono  22732  bclbnd  22735  bposlem1  22739  bposlem5  22743  lgslem1  22751  lgsval  22755  lgsdilem  22777  lgsne0  22788  lgsqrlem2  22797  lgsqrlem4  22799  lgseisenlem1  22804  lgseisenlem2  22805  lgsquadlem1  22809  lgsquadlem2  22810  lgsquadlem3  22811  lgsquad2lem2  22814  m1lgs  22817  2sqlem4  22822  2sqlem8a  22826  2sqblem  22832  dchrisumlema  22853  dchrisumlem2  22855  dchrisumlem3  22856  chpdifbndlem2  22919  pntrsumbnd2  22932  pntpbnd1  22951  pntibndlem3  22957  pntlemi  22969  pntleme  22973  pntlem3  22974  pnt3  22977  ostth2lem2  22999  ostth3  23003  ostth  23004  tgcgrxfr  23089  legtrid  23143  brbtwn2  23286  axlowdim2  23341  axlowdim  23342  axcontlem2  23346  axcontlem3  23347  axcontlem4  23348  axcontlem9  23353  axcontlem10  23354  axcontlem11  23355  axcontlem12  23356  ebtwntg  23363  eupath2lem3  23735  eupath2  23736  konigsberg  23743  nmounbseqi  24312  nmounbseqiOLD  24313  isblo3i  24336  blo3i  24337  blocnilem  24339  siilem2  24387  normlem6  24652  normgt0  24664  norm3dif  24687  norm3lemt  24689  pjhthlem1  24929  pjige0  25229  nmcexi  25565  lnconi  25572  lnopcnbd  25575  lnfncnbd  25596  riesz1  25604  cnlnadjlem2  25607  cnlnadjlem8  25613  leopg  25661  leop2  25663  leoppos  25665  leopadd  25671  leopmuli  25672  leopmul2i  25674  pjssge0i  25705  pjdifnormi  25706  pjssposi  25711  pjssdif1i  25714  chcv1  25894  cvexch  25913  atcvatlem  25924  atcvat3i  25935  atdmd  25937  cdj3i  25980  addltmulALT  25985  xrofsup  26189  xrge0addgt0  26288  omndadd  26303  omndmul2  26309  ogrpinvlt  26321  isarchi3  26338  archirng  26339  archirngz  26340  archiexdiv  26341  isorng  26401  orngmul  26405  ofldchr  26416  isarchiofld  26419  elrhmunit  26422  rearchi  26444  unitdivcld  26465  esumlub  26645  esumfsup  26653  esumcvg  26669  dya2ub  26819  itgeq12dv  26846  oddpwdc  26871  eulerpartlems  26877  prob01  26930  orvcval  26974  ballotlemfc0  27009  ballotlemfcc  27010  ballotleme  27013  ballotlem4  27015  ballotlem1c  27024  ballotlemsval  27025  ballotlemieq  27033  sgnmulsgp  27067  signsply0  27086  signslema  27097  signsvfpn  27120  lgamgulmlem1  27149  lgamgulmlem2  27150  lgamgulmlem3  27151  lgamgulmlem5  27153  lgambdd  27157  lgamcvglem  27160  erdszelem8  27220  erdsze2lem2  27226  abs2sqle  27459  abs2sqlt  27460  possumd  27530  pdivsq  27689  dvdspw  27690  poseq  27848  soseq  27849  sltval  27922  cgrdegen  28169  brofs  28170  segconeu  28176  btwntriv2  28177  transportprops  28199  brifs  28208  ifscgr  28209  brcgr3  28211  cgrxfr  28220  brcolinear2  28223  colineardim1  28226  brfs  28244  idinside  28249  btwnconn1lem11  28262  btwnconn1lem12  28263  btwnconn1lem14  28265  brsegle  28273  seglerflx  28277  seglemin  28278  segleantisym  28280  btwnsegle  28282  outsideofeu  28296  outsidele  28297  fvray  28306  ltflcei  28557  lxflflp1  28559  cos2h  28561  tan2h  28562  heicant  28564  mblfinlem2  28567  mblfinlem3  28568  mblfinlem4  28569  dvtanlem  28579  itg2addnclem  28581  itg2addnclem2  28582  itg2gt0cn  28585  itggt0cn  28602  ftc1anclem5  28609  dvasin  28618  areacirclem1  28622  areacirclem4  28625  areacirclem5  28626  areacirc  28627  nn0prpwlem  28655  nn0prpw  28656  seqpo  28781  incsequz2  28783  mettrifi  28791  heibor1lem  28846  rrncmslem  28869  elpell1qr2  29351  monotuz  29420  monotoddzzfi  29421  monotoddzz  29422  oddcomabszz  29423  rmxypos  29428  mzpcong  29453  congrep  29454  acongsym  29457  acongneg2  29458  acongtr  29459  acongeq12d  29460  dvdsabsmod0  29473  divalgmodcl  29474  jm2.18  29475  jm2.19lem2  29477  jm2.19lem3  29478  jm2.19lem4  29479  jm2.19  29480  jm2.25  29486  jm2.15nn0  29490  jm2.16nn0  29491  jm2.27  29495  rmydioph  29501  expdiophlem1  29508  expdiophlem2  29509  fnwe2lem2  29542  evth2f  29875  evthf  29887  rfcnpre3  29893  fmul01  29899  fmul01lt1lem1  29903  climinf  29917  climinff  29922  stoweidlem3  29936  stoweidlem7  29940  stoweidlem15  29948  stoweidlem16  29949  stoweidlem18  29951  stoweidlem26  29959  stoweidlem27  29960  stoweidlem28  29961  stoweidlem31  29964  stoweidlem34  29967  stoweidlem36  29969  stoweidlem37  29970  stoweidlem41  29974  stoweidlem44  29977  stoweidlem45  29978  stoweidlem46  29979  stoweidlem48  29981  stoweidlem51  29984  stoweidlem55  29988  stoweidlem59  29992  stoweidlem60  29993  stoweidlem62  29995  nn01to3  30325  subsubelfzo0  30348  eluzgtdifelfzo  30357  clwlkisclwwlklem2a4  30584  clwlkisclwwlklem2a  30585  ltsubsubaddltsub  30605  nbhashuvtx1  30671  frgrareggt1  30847  nn0le2is012  30906  telescgsum  30955  lcoop  31052  islininds  31087  ldepsnlinc  31157  pmatcoe1fsupp  31167  pmattomply1rn  31257  fvmptnn04if  31303  lsatcv0eq  32998  oposlem  33133  oplecon1b  33152  opltcon1b  33156  atlatmstc  33270  cvlexch1  33279  cvlexch2  33280  cvlexchb2  33282  cvlatexchb2  33286  cvlatexch2  33288  cvlatcvr2  33293  cvlsupr2  33294  ishlat1  33303  hlsuprexch  33331  cvrexch  33370  cvrat  33372  atcvr0eq  33376  atcvrj0  33378  atltcvr  33385  cvrat3  33392  cvrat4  33393  cvrat42  33394  3noncolr2  33399  hlatcon2  33402  4noncolr3  33403  3dimlem1  33408  3dimlem2  33409  3dimlem3a  33410  3dimlem3  33411  3dimlem3OLDN  33412  3dimlem4a  33413  3dimlem4  33414  3dimlem4OLDN  33415  3dim1lem5  33416  3dim2  33418  3dim3  33419  ps-1  33427  ps-2  33428  3atlem5  33437  3atlem6  33438  lplni2  33487  lplnnle2at  33491  lplnnleat  33492  lplnnlelln  33493  lplnribN  33501  lplnexllnN  33514  lvoli2  33531  lvolnle3at  33532  lvolnleat  33533  lvolnlelln  33534  lvolnlelpln  33535  4atlem9  33553  4atlem10a  33554  4atlem11a  33557  4atlem11  33559  4atlem12a  33560  dalempnes  33601  dalemqnet  33602  dalem1  33609  dalemswapyzps  33640  dalemrotps  33641  dalem30  33652  dalem35  33657  lineset  33688  islinei  33690  psubspset  33694  psubspi2N  33698  snatpsubN  33700  2llnma1  33737  elpaddn0  33750  elpaddri  33752  elpaddat  33754  elpadd2at  33756  paddcom  33763  paddasslem12  33781  pmapjat1  33803  llnexchb2  33819  lhp2at0nle  33985  lhprelat3N  33990  4atexlemswapqr  34013  4atexlemcnd  34022  lautle  34034  lautcvr  34042  ltrnel  34089  ltrneq2  34098  trlnle  34136  cdlemc3  34143  cdlemd6  34153  cdleme3  34187  cdleme7aa  34192  cdleme7  34199  cdleme11c  34211  cdleme15c  34226  cdleme20y  34252  cdleme20m  34273  cdleme21b  34276  cdleme21c  34277  cdleme21at  34278  cdleme36a  34410  cdleme43bN  34440  cdleme43dN  34442  cdleme46f2g2  34443  cdleme46f2g1  34444  cdlemeg46c  34463  cdlemeg46nlpq  34467  cdlemb3  34556  cdlemg4d  34563  cdlemg6d  34571  cdlemg10c  34589  cdlemg12  34600  cdlemg27b  34646  djhcvat42  35366
  Copyright terms: Public domain W3C validator