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

Theorem breq2d 4371
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 4363 . 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 4359
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2058  ax-ext 2402
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2552  df-rab 2717  df-v 3018  df-dif 3375  df-un 3377  df-in 3379  df-ss 3386  df-nul 3698  df-if 3848  df-sn 3935  df-pr 3937  df-op 3941  df-br 4360
This theorem is referenced by:  breqtrd  4384  sbcbr1g  4414  pofun  4726  csbfv12  5853  isorel  6169  soisores  6170  soisoi  6171  isocnv  6173  isotr  6179  f1owe  6196  caovordig  6425  caovordg  6427  caovord  6431  f1oweALT  6728  frxp  6854  xporderlem  6855  fnwelem  6859  difsnen  7600  domdifsn  7601  unfilem3  7783  domunfican  7790  marypha1lem  7893  marypha1  7894  inflb  7951  wemapwe  8147  oef1o  8148  r1sdom  8190  sdomsdomcardi  8350  alephordi  8449  pwcdadom  8590  sornom  8651  axdclem  8893  pwcfsdom  8952  elgch  8991  winalim2  9065  rankcf  9146  inatsk  9147  pinq  9296  nqereu  9298  ltaddnq  9343  ltrnq  9348  archnq  9349  addclprlem1  9385  mulclprlem  9388  1idpr  9398  ltaprlem  9413  ltapr  9414  prlem936  9416  ltasr  9468  mulgt0sr  9473  sqgt0sr  9474  map2psrpr  9478  axpre-ltadd  9535  axpre-mulgt0  9536  axpre-sup  9537  ltsubadd2  10029  lesubadd2  10031  ltaddpos2  10049  posdif  10051  lesub1  10052  ltnegcon1  10059  lenegcon1  10062  addge02  10069  leaddle0  10073  mulge0  10076  msqge0  10079  ltordlem  10083  sublt0d  10182  prodgt0  10394  prodgt02  10395  prodge02  10397  ltmulgt12  10410  lemulge12  10412  mulge0b  10419  mulle0b  10420  ltdivmul  10424  ledivmul  10425  ltdivmul2  10426  lt2mul2div  10427  ledivmul2  10428  ledivmul2OLD  10429  ltrec  10432  ltrec1  10437  ltdiv23  10441  lediv23  10442  nnge1  10579  halfpos  10787  lt2halves  10791  addltmul  10792  avglt2  10795  avgle2  10797  nnrecl  10811  zltlem1  10933  gtndiv  10957  nn01to3  11201  rebtwnz  11207  xrmax1  11414  max1ALT  11425  qbtwnre  11436  xralrple  11442  xltnegi  11453  xmulval  11462  xsubge0  11491  xposdif  11492  xlesubadd  11493  divelunit  11718  eluzgtdifelfzo  11919  fllelt  11976  flflp1  11986  flbi  11994  btwnzge0  12004  dfceil2  12011  ceilval2  12012  2submod  12094  om2uzlti  12107  monoord  12186  sermono  12188  expval  12217  expnbnd  12344  discr1  12351  discr  12352  facwordi  12417  seqcoll  12568  seqcoll2  12569  hashtpg  12582  swrdccat3blem  12790  cnpart  13240  sqrlem6  13248  sqrmo  13252  resqreu  13253  resqrtcl  13254  resqrtthlem  13255  sqrtneg  13268  sqreulem  13359  sqreu  13360  sqrtthlem  13362  eqsqrtd  13367  limsuple  13472  limsupleOLD  13473  rlimcld2  13578  rlimrege0  13579  o1compt  13587  climserle  13662  caurcvgr  13674  caurcvgrOLD  13675  fsum00  13794  fsumabs  13797  climcndslem2  13844  climcnds  13845  supcvg  13850  georeclim  13864  geoisumr  13870  cvgrat  13875  sin01bnd  14175  cos01bnd  14176  ruclem1  14219  ruclem9  14226  ruclem12  14229  dvdsaddr  14280  dvdssub  14281  dvdssubr  14282  dvdsfac  14296  dvdsmod  14298  oddp1even  14303  fproddvdsd  14306  divalglem0  14307  divalglem2  14309  divalglem2OLD  14310  divalglem4  14311  divalglem5OLD  14312  divalglem5  14313  divalglem9  14317  divalglem9OLD  14318  divalg  14320  divalg2  14322  divalgmod  14323  ndvdssub  14324  ndvdsadd  14325  bitsfval  14332  bitsval  14333  bits0  14337  bitsp1  14340  bitsfzolem  14343  bitsfzolemOLD  14344  bitsfzo  14345  bitscmp  14348  bitsinv1lem  14351  bitsshft  14385  gcdcllem1  14409  dvdslegcd  14414  bezoutlem4OLD  14442  bezoutlem4  14445  dvdssqim  14457  dvdsmulgcd  14458  dvdssq  14464  nn0seqcvgd  14465  lcmfunsnlem2lem2  14548  divgcdodd  14589  coprmdvds  14595  coprmdvds2  14596  isprm6  14602  prmdvdsexp  14603  prmdvdsexpr  14605  prmfac1  14607  rpmul  14611  hashdvds  14659  phiprmpw  14660  eulerthlem2  14666  prmdiv  14669  prmdiveq  14670  odzval  14672  odzcllem  14673  odzdvds  14676  odzvalOLD  14678  odzcllemOLD  14679  odzdvdsOLD  14682  opoe  14697  omoe  14698  pythagtriplem11  14711  pythagtriplem13  14713  pythagtrip  14720  pceulem  14731  pczndvds2  14752  pcdvdsb  14754  pc2dvds  14764  pcz  14766  pcprmpw2  14767  pcaddlem  14769  pcmpt  14773  prmpwdvds  14784  pockthlem  14785  prmreclem2  14797  prmreclem4  14799  4sqlem11  14835  vdwlem9  14875  rami  14908  ramlb  14913  0ram  14914  ramz2  14918  ramub1lem1  14920  prmdvdsprmo  14936  prmgaplcmlem1OLD  14948  prmdvdsprmorOLD  14951  prmgaplem7  14963  prmgaplem8  14964  imasleval  15383  subsubc  15694  pospo  16155  mulgval  16696  oddvdsnn0  17129  odmulg  17143  pgpfi1  17183  pgpfi  17193  slwispgp  17199  pgpssslw  17202  subgslw  17204  sylow2alem2  17206  sylow2blem3  17210  fislw  17213  efgi  17305  efgval2  17310  efgsrel  17320  efgredlemb  17332  lt6abl  17465  telgsums  17559  dprdval  17571  dprd2dlem2  17609  dprd2da  17611  dprd2d2  17613  ablfacrplem  17634  ablfac1a  17638  ablfac1b  17639  ablfac1eulem  17641  ablfac1eu  17642  pgpfac1lem3a  17645  ablfaclem3  17656  dvdsrtr  17816  dvdsrmul1  17817  unitpropd  17861  isabvd  17984  mplval  18588  ressmplbas2  18615  mplbaspropd  18766  zndvds0  19056  znunit  19069  cygth  19077  frlmup1  19291  lmisfree  19335  pmatcoe1fsupp  19660  fvmptnn04if  19808  hmphindis  20747  ordthmeolem  20751  psmettri2  21260  ismet2  21283  xmettri2  21290  imasdsf1olem  21323  imasf1oxmet  21325  comet  21463  stdbdxmet  21465  nmogelb  21656  nmolb  21657  nmogelbOLD  21675  nmolbOLD  21676  metdsge  21801  metdseq0  21806  metdsgeOLD  21816  metdseq0OLD  21821  iihalf2  21896  bndth  21921  evth  21922  ipcau2  22143  tchcphlem1  22144  tchcphlem2  22145  iscau3  22183  iscmet3  22198  bcthlem1  22227  bcth  22232  minveclem3b  22305  minveclem3  22306  minveclem4  22309  minveclem5  22310  minveclem3bOLD  22317  minveclem3OLD  22318  minveclem4OLD  22321  minveclem5OLD  22322  pjthlem1  22326  pjthlem2  22327  pmltpclem1  22334  pmltpc  22336  ivthlem2  22338  ivthlem3  22339  ovolgelb  22368  ovolunlem1  22385  ovoliunlem2  22391  ovolshftlem1  22397  ovolscalem1  22401  ovolicc1  22404  ovolicc2lem3  22407  ioombl1lem4  22449  mbfmulc2lem  22538  mbfposb  22544  mbfaddlem  22551  mbfsup  22555  mbfinf  22556  mbfinfOLD  22557  mbflimsup  22558  mbflimsupOLD  22559  i1fposd  22600  itg1ge0a  22604  mbfi1fseqlem4  22611  mbfi1fseqlem6  22613  mbfi1flimlem  22615  mbfi1flim  22616  itg2const2  22634  itg2seq  22635  itg2monolem1  22643  itg2i1fseq  22648  itg2addlem  22651  ibllem  22657  isibl  22658  isibl2  22659  iblitg  22661  dfitg  22662  cbvitg  22668  itgeq2  22670  itgvallem  22677  iblneg  22695  itgneg  22696  itggt0  22734  dvlip  22880  c1lip1  22884  dvfsumle  22908  dvfsumlem2  22914  dvfsumlem4  22916  dvfsum2  22921  mdeglt  22949  degltp1le  22957  deg1suble  22991  ply1divex  23022  plypf1  23101  dgrlb  23125  coemulc  23144  dgrsub  23161  quotval  23180  plydivlem4  23184  quotcan  23197  vieta1lem2  23199  aalioulem2  23224  aaliou3lem9  23241  ulmcn  23289  dvradcnv  23311  sincosq1sgn  23388  sincosq2sgn  23389  sincosq4sgn  23391  logltb  23484  cxpge0  23563  cxple2  23577  logreclem  23634  jensen  23849  emcllem7  23862  lgamgulmlem1  23889  lgamgulmlem2  23890  lgamgulmlem3  23891  lgamgulmlem5  23893  lgambdd  23897  lgamcvglem  23900  wilthlem1  23928  ftalem2  23933  ftalem3  23934  ftalem7  23940  fta  23941  sgmval  24004  mumul  24043  dvdsppwf1o  24050  musum  24055  chtublem  24074  chtub  24075  perfect1  24091  bcmono  24140  bclbnd  24143  bposlem1  24147  bposlem5  24151  lgslem1  24159  lgsval  24163  lgsdilem  24185  lgsne0  24196  lgsqrlem2  24205  lgsqrlem4  24207  lgseisenlem1  24212  lgseisenlem2  24213  lgsquadlem1  24217  lgsquadlem2  24218  lgsquadlem3  24219  lgsquad2lem2  24222  m1lgs  24225  2sqlem4  24230  2sqlem8a  24234  2sqblem  24240  dchrisumlema  24261  dchrisumlem2  24263  dchrisumlem3  24264  chpdifbndlem2  24327  pntrsumbnd2  24340  pntpbnd1  24359  pntibndlem3  24365  pntlemi  24377  pntleme  24381  pntlem3  24382  pnt3  24385  ostth2lem2  24407  ostth3  24411  ostth  24412  tgcgrxfr  24498  hlpasch  24733  islmib  24764  lmicom  24765  trgcopyeu  24783  iscgra  24786  iscgra1  24787  iscgrad  24788  isleag  24818  iseqlg  24832  brbtwn2  24870  axlowdim2  24925  axlowdim  24926  axcontlem2  24930  axcontlem3  24931  axcontlem4  24932  axcontlem9  24937  axcontlem10  24938  axcontlem11  24939  axcontlem12  24940  ebtwntg  24947  ausisusgraedg  25018  clwlkisclwwlklem2a4  25447  clwlkisclwwlklem2a  25448  nbhashuvtx1  25578  eupath2lem3  25642  eupath2  25643  konigsberg  25650  frgrareggt1  25779  ex-ind-dvds  25834  nmounbseqi  26353  nmounbseqiALT  26354  isblo3i  26377  blo3i  26378  blocnilem  26380  siilem2  26428  normlem6  26703  normgt0  26715  norm3dif  26738  norm3lemt  26740  pjhthlem1  26979  pjige0  27279  nmcexi  27614  lnconi  27621  lnopcnbd  27624  lnfncnbd  27645  riesz1  27653  cnlnadjlem2  27656  cnlnadjlem8  27662  leopg  27710  leop2  27712  leoppos  27714  leopadd  27720  leopmuli  27721  leopmul2i  27723  pjssge0i  27754  pjdifnormi  27755  pjssposi  27760  pjssdif1i  27763  chcv1  27943  cvexch  27962  atcvatlem  27973  atcvat3i  27984  atdmd  27986  cdj3i  28029  addltmulALT  28034  xrofsup  28296  xrge0addgt0  28398  omndadd  28413  omndmul2  28419  ogrpinvlt  28431  isinftm  28442  isarchi3  28448  archirng  28449  archirngz  28450  archiexdiv  28451  isorng  28507  orngmul  28511  ofldchr  28522  isarchiofld  28525  elrhmunit  28528  rearchi  28550  fzto1st  28561  unitdivcld  28652  esumlub  28826  esumfsup  28836  esumcvg  28852  esum2d  28859  dya2ub  29037  omssubadd  29073  omssubaddOLD  29077  carsgmon  29091  itgeq12dv  29104  oddpwdc  29132  eulerpartlems  29138  prob01  29191  orvcval  29235  ballotlemfc0  29270  ballotlemfcc  29271  ballotleme  29274  ballotlem4  29276  ballotlemimin  29283  ballotlem1c  29285  ballotlemsval  29286  ballotlemieq  29294  ballotlemfrcn0  29307  ballotlem1cOLD  29323  ballotlemsvalOLD  29324  ballotlemieqOLD  29332  sgnmulsgp  29366  signsply0  29385  signslema  29396  signsvfpn  29419  erdszelem8  29866  erdsze2lem2  29872  abs2sqle  30269  abs2sqlt  30270  possumd  30310  pdivsq  30329  dvdspw  30330  poseq  30435  soseq  30436  sltval  30478  cgrdegen  30713  brofs  30714  segconeu  30720  btwntriv2  30721  transportprops  30743  brifs  30752  ifscgr  30753  brcgr3  30755  cgrxfr  30764  brcolinear2  30767  colineardim1  30770  brfs  30788  idinside  30793  btwnconn1lem11  30806  btwnconn1lem12  30807  btwnconn1lem14  30809  brsegle  30817  seglerflx  30821  seglemin  30822  segleantisym  30824  btwnsegle  30826  outsideofeu  30840  outsidele  30841  fvray  30850  nn0prpwlem  30920  nn0prpw  30921  ltflcei  31834  cos2h  31837  tan2h  31838  poimirlem5  31846  poimirlem6  31847  poimirlem7  31848  poimirlem8  31849  poimirlem10  31851  poimirlem11  31852  poimirlem12  31853  poimirlem15  31856  poimirlem16  31857  poimirlem17  31858  poimirlem18  31859  poimirlem19  31860  poimirlem20  31861  poimirlem21  31862  poimirlem22  31863  poimirlem25  31866  poimirlem27  31868  poimirlem28  31869  poimirlem29  31870  poimirlem30  31871  poimirlem31  31872  poimirlem32  31873  poimir  31874  heicant  31876  mblfinlem2  31879  mblfinlem3  31880  mblfinlem4  31881  dvtanlemOLD  31892  itg2addnclem  31894  itg2addnclem2  31895  itg2gt0cn  31898  itggt0cn  31915  ftc1anclem5  31922  dvasin  31929  areacirclem1  31933  areacirclem4  31936  areacirclem5  31937  areacirc  31938  seqpo  31977  incsequz2  31979  mettrifi  31987  heibor1lem  32042  rrncmslem  32065  lsatcv0eq  32519  oposlem  32654  oplecon1b  32673  opltcon1b  32677  atlatmstc  32791  cvlexch1  32800  cvlexch2  32801  cvlexchb2  32803  cvlatexchb2  32807  cvlatexch2  32809  cvlatcvr2  32814  cvlsupr2  32815  ishlat1  32824  hlsuprexch  32852  cvrexch  32891  cvrat  32893  atcvr0eq  32897  atcvrj0  32899  atltcvr  32906  cvrat3  32913  cvrat4  32914  cvrat42  32915  3noncolr2  32920  hlatcon2  32923  4noncolr3  32924  3dimlem1  32929  3dimlem2  32930  3dimlem3a  32931  3dimlem3  32932  3dimlem3OLDN  32933  3dimlem4a  32934  3dimlem4  32935  3dimlem4OLDN  32936  3dim1lem5  32937  3dim2  32939  3dim3  32940  ps-1  32948  ps-2  32949  3atlem5  32958  3atlem6  32959  lplni2  33008  lplnnle2at  33012  lplnnleat  33013  lplnnlelln  33014  lplnribN  33022  lplnexllnN  33035  lvoli2  33052  lvolnle3at  33053  lvolnleat  33054  lvolnlelln  33055  lvolnlelpln  33056  4atlem9  33074  4atlem10a  33075  4atlem11a  33078  4atlem11  33080  4atlem12a  33081  dalempnes  33122  dalemqnet  33123  dalem1  33130  dalemswapyzps  33161  dalemrotps  33162  dalem30  33173  dalem35  33178  lineset  33209  islinei  33211  psubspset  33215  psubspi2N  33219  snatpsubN  33221  2llnma1  33258  elpaddn0  33271  elpaddri  33273  elpaddat  33275  elpadd2at  33277  paddcom  33284  paddasslem12  33302  pmapjat1  33324  llnexchb2  33340  lhp2at0nle  33506  lhprelat3N  33511  4atexlemswapqr  33534  4atexlemcnd  33543  lautle  33555  lautcvr  33563  ltrnel  33610  ltrneq2  33619  trlnle  33658  cdlemc3  33665  cdlemd6  33675  cdleme3  33709  cdleme7aa  33714  cdleme7  33721  cdleme11c  33733  cdleme15c  33748  cdleme20yOLD  33775  cdleme20m  33796  cdleme21b  33799  cdleme21c  33800  cdleme21at  33801  cdleme36a  33933  cdleme43bN  33963  cdleme43dN  33965  cdleme46f2g2  33966  cdleme46f2g1  33967  cdlemeg46c  33986  cdlemeg46nlpq  33990  cdlemb3  34079  cdlemg4d  34086  cdlemg6d  34094  cdlemg10c  34112  cdlemg12  34123  cdlemg27b  34169  djhcvat42  34889  elpell1qr2  35625  monotuz  35696  monotoddzzfi  35697  monotoddzz  35698  oddcomabszz  35699  rmxypos  35704  mzpcong  35729  congrep  35730  acongsym  35733  acongneg2  35734  acongtr  35735  acongeq12d  35736  dvdsabsmod0OLD  35748  divalgmodcl  35749  jm2.18  35750  jm2.19lem2  35752  jm2.19lem3  35753  jm2.19lem4  35754  jm2.19  35755  jm2.25  35761  jm2.15nn0  35765  jm2.16nn0  35766  jm2.27  35770  rmydioph  35776  expdiophlem1  35783  expdiophlem2  35784  fnwe2lem2  35816  relexpmulg  36209  relexpxpmin  36216  frege124d  36260  frege72  36438  frege91  36457  inductionexd  36500  leeq2d  36503  imo72b2lem0  36515  imo72b2lem2  36517  imo72b2lem1  36521  imo72b2  36526  dvgrat  36568  hashnzfz  36576  evth2f  37246  evthf  37258  rfcnpre3  37264  ltaddneg  37399  upbdrech2  37417  supxrgelem  37451  supxrge  37452  xrlexaddrp  37466  xralrple2  37468  ltdivgt1  37470  fsumlessf  37534  fmul01  37535  fmul01lt1lem1  37539  climinf  37561  climinfOLD  37562  climinff  37567  climinffOLD  37568  limcrecl  37586  limsupre  37598  limsupreOLD  37599  limclner  37609  cncficcgt0  37643  stoweidlem3  37740  stoweidlem7  37744  stoweidlem15  37752  stoweidlem16  37753  stoweidlem18  37755  stoweidlem26  37763  stoweidlem27  37764  stoweidlem28  37765  stoweidlem31  37769  stoweidlem34  37772  stoweidlem36  37774  stoweidlem37  37775  stoweidlem41  37779  stoweidlem44  37782  stoweidlem45  37783  stoweidlem46  37784  stoweidlem48  37786  stoweidlem51  37789  stoweidlem55  37793  stoweidlem59  37797  stoweidlem60  37798  stoweidlem62  37800  stoweidlem62OLD  37801  fourierdlem42  37889  fourierdlem42OLD  37890  fourierdlem50  37897  fourierdlem54  37901  fourierdlem68  37915  fourierdlem79  37926  fourierdlem96  37943  fourierdlem97  37944  fourierdlem98  37945  fourierdlem99  37946  fourierdlem105  37952  fourierdlem108  37955  fourierdlem110  37957  fourierdlem111  37958  etransclem24  38000  etransclem25  38001  etransclem35  38011  etransclem37  38013  etransclem41  38017  etransclem44  38020  sge0gerp  38082  sge0pnffigt  38083  sge0gerpmpt  38089  omessle  38164  ovncvrrp  38227  ovnsubaddlem1  38233  ovnsubadd  38235  hoidmv1lelem2  38255  hoidmvlelem3  38260  hoidmvle  38263  smonoord  38525  iccpartiltu  38543  iccpartlt  38545  iccpartgtl  38547  iccpartgt  38548  iccpartgel  38550  iccpartrn  38551  iccpartiun  38555  icceuelpartlem  38556  iccpartdisj  38558  iccpartnel  38559  bits0ALTV  38615  sgoldbaltlem1  38687  bgoldbtbndlem2  38708  bgoldbtbndlem3  38709  bgoldbtbnd  38711  ltsubsubaddltsub  38839  subsubelfzo0  38853  nn0le2is012  39735  lcoop  39791  islininds  39826  ldepsnlinc  39888  ltsubaddb  39898  ltsubsubb  39899  ltsubadd2b  39900  logle1b  39931  loglt1b  39932  bigoval  39947  elbigo2r  39951  logbge0b  39961  logblt1b  39962  fldivexpfllog2  39963  nnlog2ge0lt1  39964  fllog2  39966  nnpw2pmod  39981  dignn0ldlem  40000  dig2nn1st  40003
  Copyright terms: Public domain W3C validator