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

Theorem breq2d 4299
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 4291 . 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 1369   class class class wbr 4287
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-rab 2719  df-v 2969  df-dif 3326  df-un 3328  df-in 3330  df-ss 3337  df-nul 3633  df-if 3787  df-sn 3873  df-pr 3875  df-op 3879  df-br 4288
This theorem is referenced by:  breqtrd  4311  sbcbr1g  4342  pofun  4652  csbfv12  5720  csbfv12gOLD  5721  isorel  6012  soisores  6013  soisoi  6014  isocnv  6016  isotr  6022  f1owe  6039  caovordig  6263  caovordg  6265  caovord  6269  f1oweALT  6556  frxp  6677  xporderlem  6678  fnwelem  6682  th3qlem2  7199  difsnen  7385  domdifsn  7386  unfilem3  7570  domunfican  7576  marypha1lem  7675  marypha1  7676  wemapwe  7920  oef1o  7922  r1sdom  7973  sdomsdomcardi  8133  alephordi  8236  pwcdadom  8377  sornom  8438  axdclem  8680  pwcfsdom  8739  elgch  8781  winalim2  8855  rankcf  8936  inatsk  8937  pinq  9088  nqereu  9090  ltaddnq  9135  ltrnq  9140  archnq  9141  addclprlem1  9177  mulclprlem  9180  1idpr  9190  ltaprlem  9205  ltapr  9206  prlem936  9208  ltasr  9259  mulgt0sr  9264  sqgt0sr  9265  map2psrpr  9269  axpre-ltadd  9326  axpre-mulgt0  9327  axpre-sup  9328  ltsubadd2  9802  lesubadd2  9804  ltaddpos2  9822  posdif  9824  lesub1  9825  ltnegcon1  9832  lenegcon1  9835  addge02  9842  leaddle0  9846  mulge0  9849  msqge0  9853  ltordlem  9857  prodgt0  10166  prodgt02  10167  prodge02  10169  ltmulgt12  10182  lemulge12  10184  mulge0b  10191  mulle0b  10192  ltdivmul  10196  ledivmul  10197  ledivmulOLD  10198  ltdivmul2  10199  lt2mul2div  10200  ledivmul2  10201  ledivmul2OLD  10202  ltrec  10205  ltrec1  10211  ltdiv23  10215  lediv23  10216  nnge1  10340  halfpos  10547  lt2halves  10551  addltmul  10552  avglt2  10555  avgle2  10557  nnrecl  10569  zltlem1  10689  gtndiv  10711  rebtwnz  10944  xrmax1  11139  max1ALT  11150  qbtwnre  11161  xralrple  11167  xltnegi  11178  xmulval  11187  xsubge0  11216  xposdif  11217  xlesubadd  11218  divelunit  11419  fllelt  11639  flbi  11656  btwnzge0  11665  dfceil2  11672  ceilval2  11673  2submod  11752  om2uzlti  11765  monoord  11828  sermono  11830  expval  11859  expnbnd  11985  discr1  11992  discr  11993  facwordi  12057  hashtpg  12178  seqcoll  12208  seqcoll2  12209  swrdccat3blem  12378  cnpart  12721  sqrlem6  12729  sqrmo  12733  resqreu  12734  resqrcl  12735  resqrthlem  12736  sqrneg  12749  sqreulem  12839  sqreu  12840  sqrthlem  12842  eqsqrd  12847  limsuple  12948  rlimcld2  13048  rlimrege0  13049  o1compt  13057  climserle  13132  caurcvgr  13143  fsum00  13253  fsumabs  13256  climcndslem2  13305  climcnds  13306  supcvg  13310  georeclim  13324  geoisumr  13330  cvgrat  13335  sin01bnd  13461  cos01bnd  13462  ruclem1  13505  ruclem9  13512  ruclem12  13515  dvdsaddr  13564  dvdssub  13565  dvdssubr  13566  dvdsfac  13580  dvdsmod  13582  oddp1even  13586  divalglem0  13589  divalglem2  13591  divalglem4  13592  divalglem5  13593  divalglem9  13597  divalg  13599  divalg2  13601  divalgmod  13602  ndvdssub  13603  ndvdsadd  13604  bitsfval  13611  bitsval  13612  bits0  13616  bitsp1  13619  bitsfzolem  13622  bitsfzo  13623  bitscmp  13626  bitsinv1lem  13629  bitsshft  13663  gcdcllem1  13687  dvdslegcd  13692  bezoutlem4  13717  dvdssqim  13729  dvdsmulgcd  13730  dvdssq  13736  nn0seqcvgd  13737  coprmdvds  13780  coprmdvds2  13781  isprm6  13787  prmdvdsexp  13792  prmdvdsexpr  13794  prmfac1  13796  divgcdodd  13797  rpmul  13801  hashdvds  13842  phiprmpw  13843  eulerthlem2  13849  prmdiv  13852  prmdiveq  13853  odzval  13855  odzcllem  13856  odzdvds  13859  opoe  13870  omoe  13871  pythagtriplem11  13884  pythagtriplem13  13886  pythagtrip  13893  pceulem  13904  pczndvds2  13925  pcdvdsb  13927  pc2dvds  13937  pcz  13939  pcprmpw2  13940  pcaddlem  13942  pcmpt  13946  prmpwdvds  13957  pockthlem  13958  prmreclem2  13970  prmreclem4  13972  4sqlem11  14008  vdwlem9  14042  rami  14068  ramlb  14072  0ram  14073  ramz2  14077  ramub1lem1  14079  imasleval  14471  subsubc  14755  pospo  15135  mulgval  15620  oddvdsnn0  16038  odmulg  16048  pgpfi1  16085  pgpfi  16095  slwispgp  16101  pgpssslw  16104  subgslw  16106  sylow2alem2  16108  sylow2blem3  16112  fislw  16115  efgi  16207  efgval2  16212  efgsrel  16222  efgredlemb  16234  lt6abl  16362  dprdval  16475  dprdvalOLD  16477  dprd2dlem2  16529  dprd2da  16531  dprd2d2  16533  ablfacrplem  16556  ablfac1a  16560  ablfac1b  16561  ablfac1eulem  16563  ablfac1eu  16564  pgpfac1lem3a  16567  ablfaclem3  16578  dvdsrtr  16734  dvdsrmul1  16735  unitpropd  16779  isabvd  16885  mplval  17481  ressmplbas2  17514  mplbaspropd  17671  zndvds0  17963  znunit  17976  cygth  17984  frlmup1  18206  lmisfree  18251  hmphindis  19350  ordthmeolem  19354  psmettri2  19865  ismet2  19888  xmettri2  19895  imasdsf1olem  19928  imasf1oxmet  19930  comet  20068  stdbdxmet  20070  nmogelb  20275  nmolb  20276  metdsge  20405  metdseq0  20410  iihalf2  20485  bndth  20510  evth  20511  ipcau2  20729  tchcphlem1  20730  tchcphlem2  20731  iscau3  20769  iscmet3  20784  bcthlem1  20815  bcth  20820  minveclem3b  20895  minveclem3  20896  minveclem4  20899  minveclem5  20900  pjthlem1  20904  pjthlem2  20905  pmltpclem1  20912  pmltpc  20914  ivthlem2  20916  ivthlem3  20917  ovolgelb  20943  ovolunlem1  20960  ovoliunlem2  20966  ovolshftlem1  20972  ovolscalem1  20976  ovolicc1  20979  ovolicc2lem3  20982  ioombl1lem4  21022  mbfmulc2lem  21105  mbfposb  21111  mbfaddlem  21118  mbfsup  21122  mbfinf  21123  mbflimsup  21124  i1fposd  21165  itg1ge0a  21169  mbfi1fseqlem4  21176  mbfi1fseqlem6  21178  mbfi1flimlem  21180  mbfi1flim  21181  itg2const2  21199  itg2seq  21200  itg2monolem1  21208  itg2i1fseq  21213  itg2addlem  21216  ibllem  21222  isibl  21223  isibl2  21224  iblitg  21226  dfitg  21227  cbvitg  21233  itgeq2  21235  itgvallem  21242  iblneg  21260  itgneg  21261  itggt0  21299  dvlip  21445  c1lip1  21449  dvfsumle  21473  dvfsumlem2  21479  dvfsumlem4  21481  dvfsum2  21486  mdeglt  21516  degltp1le  21524  deg1suble  21559  ply1divex  21588  plypf1  21660  dgrlb  21684  coemulc  21702  dgrsub  21719  quotval  21738  plydivlem4  21742  quotcan  21755  vieta1lem2  21757  aalioulem2  21779  aaliou3lem9  21796  ulmcn  21844  dvradcnv  21866  sincosq1sgn  21940  sincosq2sgn  21941  sincosq4sgn  21943  logltb  22028  cxpge0  22108  cxple2  22122  logreclem  22194  jensen  22362  emcllem7  22375  wilthlem1  22386  ftalem2  22391  ftalem3  22392  ftalem7  22396  fta  22397  sgmval  22460  mumul  22499  dvdsppwf1o  22506  musum  22511  chtublem  22530  chtub  22531  perfect1  22547  bcmono  22596  bclbnd  22599  bposlem1  22603  bposlem5  22607  lgslem1  22615  lgsval  22619  lgsdilem  22641  lgsne0  22652  lgsqrlem2  22661  lgsqrlem4  22663  lgseisenlem1  22668  lgseisenlem2  22669  lgsquadlem1  22673  lgsquadlem2  22674  lgsquadlem3  22675  lgsquad2lem2  22678  m1lgs  22681  2sqlem4  22686  2sqlem8a  22690  2sqblem  22696  dchrisumlema  22717  dchrisumlem2  22719  dchrisumlem3  22720  chpdifbndlem2  22783  pntrsumbnd2  22796  pntpbnd1  22815  pntibndlem3  22821  pntlemi  22833  pntleme  22837  pntlem3  22838  pnt3  22841  ostth2lem2  22863  ostth3  22867  ostth  22868  tgcgrxfr  22950  legtrid  23002  brbtwn2  23119  axlowdim2  23174  axlowdim  23175  axcontlem2  23179  axcontlem3  23180  axcontlem4  23181  axcontlem9  23186  axcontlem10  23187  axcontlem11  23188  axcontlem12  23189  ebtwntg  23196  eupath2lem3  23568  eupath2  23569  konigsberg  23576  nmounbseqi  24145  nmounbseqiOLD  24146  isblo3i  24169  blo3i  24170  blocnilem  24172  siilem2  24220  normlem6  24485  normgt0  24497  norm3dif  24520  norm3lemt  24522  pjhthlem1  24762  pjige0  25062  nmcexi  25398  lnconi  25405  lnopcnbd  25408  lnfncnbd  25429  riesz1  25437  cnlnadjlem2  25440  cnlnadjlem8  25446  leopg  25494  leop2  25496  leoppos  25498  leopadd  25504  leopmuli  25505  leopmul2i  25507  pjssge0i  25538  pjdifnormi  25539  pjssposi  25544  pjssdif1i  25547  chcv1  25727  cvexch  25746  atcvatlem  25757  atcvat3i  25768  atdmd  25770  cdj3i  25813  addltmulALT  25818  xrofsup  26023  xrge0addgt0  26122  omndadd  26137  omndmul2  26143  ogrpinvlt  26155  isarchi3  26172  archirng  26173  archirngz  26174  archiexdiv  26175  isorng  26235  orngmul  26239  ofldchr  26250  isarchiofld  26253  elrhmunit  26256  rearchi  26279  unitdivcld  26300  esumlub  26480  esumfsup  26488  esumcvg  26504  dya2ub  26654  itgeq12dv  26681  oddpwdc  26706  eulerpartlems  26712  prob01  26765  orvcval  26809  ballotlemfc0  26844  ballotlemfcc  26845  ballotleme  26848  ballotlem4  26850  ballotlem1c  26859  ballotlemsval  26860  ballotlemieq  26868  sgnmulsgp  26902  signsply0  26921  signslema  26932  signsvfpn  26955  lgamgulmlem1  26984  lgamgulmlem2  26985  lgamgulmlem3  26986  lgamgulmlem5  26988  lgambdd  26992  lgamcvglem  26995  erdszelem8  27055  erdsze2lem2  27061  abs2sqle  27294  abs2sqlt  27295  possumd  27365  pdivsq  27524  dvdspw  27525  poseq  27683  soseq  27684  sltval  27757  cgrdegen  28004  brofs  28005  segconeu  28011  btwntriv2  28012  transportprops  28034  brifs  28043  ifscgr  28044  brcgr3  28046  cgrxfr  28055  brcolinear2  28058  colineardim1  28061  brfs  28079  idinside  28084  btwnconn1lem11  28097  btwnconn1lem12  28098  btwnconn1lem14  28100  brsegle  28108  seglerflx  28112  seglemin  28113  segleantisym  28115  btwnsegle  28117  outsideofeu  28131  outsidele  28132  fvray  28141  ltflcei  28390  lxflflp1  28392  cos2h  28394  tan2h  28395  heicant  28397  mblfinlem2  28400  mblfinlem3  28401  mblfinlem4  28402  dvtanlem  28412  itg2addnclem  28414  itg2addnclem2  28415  itg2gt0cn  28418  itggt0cn  28435  ftc1anclem5  28442  dvasin  28451  areacirclem1  28455  areacirclem4  28458  areacirclem5  28459  areacirc  28460  nn0prpwlem  28488  nn0prpw  28489  seqpo  28614  incsequz2  28616  mettrifi  28624  heibor1lem  28679  rrncmslem  28702  elpell1qr2  29184  monotuz  29253  monotoddzzfi  29254  monotoddzz  29255  oddcomabszz  29256  rmxypos  29261  mzpcong  29286  congrep  29287  acongsym  29290  acongneg2  29291  acongtr  29292  acongeq12d  29293  dvdsabsmod0  29306  divalgmodcl  29307  jm2.18  29308  jm2.19lem2  29310  jm2.19lem3  29311  jm2.19lem4  29312  jm2.19  29313  jm2.25  29319  jm2.15nn0  29323  jm2.16nn0  29324  jm2.27  29328  rmydioph  29334  expdiophlem1  29341  expdiophlem2  29342  fnwe2lem2  29375  evth2f  29708  evthf  29720  rfcnpre3  29726  fmul01  29732  fmul01lt1lem1  29736  climinf  29750  climinff  29755  stoweidlem3  29769  stoweidlem7  29773  stoweidlem15  29781  stoweidlem16  29782  stoweidlem18  29784  stoweidlem26  29792  stoweidlem27  29793  stoweidlem28  29794  stoweidlem31  29797  stoweidlem34  29800  stoweidlem36  29802  stoweidlem37  29803  stoweidlem41  29807  stoweidlem44  29810  stoweidlem45  29811  stoweidlem46  29812  stoweidlem48  29814  stoweidlem51  29817  stoweidlem55  29821  stoweidlem59  29825  stoweidlem60  29826  stoweidlem62  29828  nn01to3  30158  subsubelfzo0  30181  eluzgtdifelfzo  30190  clwlkisclwwlklem2a4  30417  clwlkisclwwlklem2a  30418  ltsubsubaddltsub  30438  nbhashuvtx1  30504  frgrareggt1  30680  nn0le2is012  30735  pmatcoe1fsupp  30852  lcoop  30876  islininds  30911  ldepsnlinc  30981  lsatcv0eq  32585  oposlem  32720  oplecon1b  32739  opltcon1b  32743  atlatmstc  32857  cvlexch1  32866  cvlexch2  32867  cvlexchb2  32869  cvlatexchb2  32873  cvlatexch2  32875  cvlatcvr2  32880  cvlsupr2  32881  ishlat1  32890  hlsuprexch  32918  cvrexch  32957  cvrat  32959  atcvr0eq  32963  atcvrj0  32965  atltcvr  32972  cvrat3  32979  cvrat4  32980  cvrat42  32981  3noncolr2  32986  hlatcon2  32989  4noncolr3  32990  3dimlem1  32995  3dimlem2  32996  3dimlem3a  32997  3dimlem3  32998  3dimlem3OLDN  32999  3dimlem4a  33000  3dimlem4  33001  3dimlem4OLDN  33002  3dim1lem5  33003  3dim2  33005  3dim3  33006  ps-1  33014  ps-2  33015  3atlem5  33024  3atlem6  33025  lplni2  33074  lplnnle2at  33078  lplnnleat  33079  lplnnlelln  33080  lplnribN  33088  lplnexllnN  33101  lvoli2  33118  lvolnle3at  33119  lvolnleat  33120  lvolnlelln  33121  lvolnlelpln  33122  4atlem9  33140  4atlem10a  33141  4atlem11a  33144  4atlem11  33146  4atlem12a  33147  dalempnes  33188  dalemqnet  33189  dalem1  33196  dalemswapyzps  33227  dalemrotps  33228  dalem30  33239  dalem35  33244  lineset  33275  islinei  33277  psubspset  33281  psubspi2N  33285  snatpsubN  33287  2llnma1  33324  elpaddn0  33337  elpaddri  33339  elpaddat  33341  elpadd2at  33343  paddcom  33350  paddasslem12  33368  pmapjat1  33390  llnexchb2  33406  lhp2at0nle  33572  lhprelat3N  33577  4atexlemswapqr  33600  4atexlemcnd  33609  lautle  33621  lautcvr  33629  ltrnel  33676  ltrneq2  33685  trlnle  33723  cdlemc3  33730  cdlemd6  33740  cdleme3  33774  cdleme7aa  33779  cdleme7  33786  cdleme11c  33798  cdleme15c  33813  cdleme20y  33839  cdleme20m  33860  cdleme21b  33863  cdleme21c  33864  cdleme21at  33865  cdleme36a  33997  cdleme43bN  34027  cdleme43dN  34029  cdleme46f2g2  34030  cdleme46f2g1  34031  cdlemeg46c  34050  cdlemeg46nlpq  34054  cdlemb3  34143  cdlemg4d  34150  cdlemg6d  34158  cdlemg10c  34176  cdlemg12  34187  cdlemg27b  34233  djhcvat42  34953
  Copyright terms: Public domain W3C validator