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

Theorem breq2d 4184
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 4176 . 2  |-  ( A  =  B  ->  ( C R A  <->  C R B ) )
31, 2syl 16 1  |-  ( ph  ->  ( C R A  <-> 
C R B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    = wceq 1649   class class class wbr 4172
This theorem is referenced by:  breqtrd  4196  sbcbr1g  4223  pofun  4479  csbfv12g  5697  isorel  6005  soisores  6006  soisoi  6007  isocnv  6009  isotr  6015  f1owe  6032  f1oweALT  6033  caovordig  6211  caovordg  6213  caovord  6217  frxp  6415  xporderlem  6416  fnwelem  6420  th3qlem2  6970  difsnen  7149  domdifsn  7150  unfilem3  7332  domunfican  7338  marypha1lem  7396  marypha1  7397  r1sdom  7656  sdomsdomcardi  7814  alephordi  7911  pwcdadom  8052  sornom  8113  axdclem  8355  pwcfsdom  8414  elgch  8453  winalim2  8527  rankcf  8608  inatsk  8609  pinq  8760  nqereu  8762  ltaddnq  8807  ltrnq  8812  archnq  8813  addclprlem1  8849  mulclprlem  8852  1idpr  8862  ltaprlem  8877  ltapr  8878  prlem936  8880  ltasr  8931  mulgt0sr  8936  sqgt0sr  8937  map2psrpr  8941  axpre-ltadd  8998  axpre-mulgt0  8999  axpre-sup  9000  ltsubadd2  9455  lesubadd2  9457  ltaddpos2  9475  posdif  9477  lesub1  9478  ltnegcon1  9485  lenegcon1  9488  addge02  9495  mulge0  9501  msqge0  9505  ltordlem  9508  prodgt0  9811  prodgt02  9812  prodge02  9814  ltmulgt12  9827  lemulge12  9829  ltdivmul  9838  ledivmul  9839  ledivmulOLD  9840  ltdivmul2  9841  lt2mul2div  9842  ledivmul2  9843  ledivmul2OLD  9844  ltrec  9847  ltrec1  9853  ltdiv23  9857  lediv23  9858  nnge1  9982  halfpos  10154  lt2halves  10158  addltmul  10159  avglt2  10162  avgle2  10164  nnrecl  10175  zltlem1  10284  gtndiv  10303  rebtwnz  10529  xrmax1  10719  max1ALT  10730  qbtwnre  10741  xralrple  10747  xltnegi  10758  xmulval  10767  xsubge0  10796  xposdif  10797  xlesubadd  10798  fllelt  11161  flbi  11178  btwnzge0  11185  om2uzlti  11245  monoord  11308  sermono  11310  expval  11339  expnbnd  11463  discr1  11470  discr  11471  facwordi  11535  hashtpg  11646  seqcoll  11667  seqcoll2  11668  cnpart  12000  sqrlem6  12008  sqrmo  12012  resqreu  12013  resqrcl  12014  resqrthlem  12015  sqrneg  12028  sqreulem  12118  sqreu  12119  sqrthlem  12121  eqsqrd  12126  limsuple  12227  rlimcld2  12327  rlimrege0  12328  o1compt  12336  climserle  12411  caurcvgr  12422  fsum00  12532  fsumabs  12535  climcndslem2  12585  climcnds  12586  supcvg  12590  georeclim  12604  geoisumr  12610  cvgrat  12615  sin01bnd  12741  cos01bnd  12742  ruclem1  12785  ruclem9  12792  ruclem12  12795  dvdsaddr  12844  dvdssub  12845  dvdssubr  12846  dvdsfac  12859  dvdsmod  12861  oddp1even  12865  divalglem0  12868  divalglem2  12870  divalglem4  12871  divalglem5  12872  divalglem9  12876  divalg  12878  divalg2  12880  divalgmod  12881  ndvdssub  12882  ndvdsadd  12883  bitsfval  12890  bitsval  12891  bits0  12895  bitsp1  12898  bitsfzolem  12901  bitsfzo  12902  bitscmp  12905  bitsinv1lem  12908  bitsshft  12942  gcdcllem1  12966  dvdslegcd  12971  bezoutlem4  12996  dvdssqim  13008  dvdsmulgcd  13009  dvdssq  13015  nn0seqcvgd  13016  coprmdvds  13057  coprmdvds2  13058  isprm6  13064  prmdvdsexp  13069  prmdvdsexpr  13071  prmfac1  13073  divgcdodd  13074  rpmul  13078  hashdvds  13119  phiprmpw  13120  eulerthlem2  13126  prmdiv  13129  prmdiveq  13130  odzval  13132  odzcllem  13133  odzdvds  13136  opoe  13140  omoe  13141  pythagtriplem11  13154  pythagtriplem13  13156  pythagtrip  13163  pceulem  13174  pczndvds2  13195  pcdvdsb  13197  pc2dvds  13207  pcz  13209  pcprmpw2  13210  pcaddlem  13212  pcmpt  13216  prmpwdvds  13227  pockthlem  13228  prmreclem2  13240  prmreclem4  13242  4sqlem11  13278  vdwlem9  13312  rami  13338  ramlb  13342  0ram  13343  ramz2  13347  ramub1lem1  13349  imasleval  13721  subsubc  14005  pospo  14385  mulgval  14847  oddvdsnn0  15137  odmulg  15147  pgpfi1  15184  pgpfi  15194  slwispgp  15200  pgpssslw  15203  subgslw  15205  sylow2alem2  15207  sylow2blem3  15211  fislw  15214  efgi  15306  efgval2  15311  efgsrel  15321  efgredlemb  15333  lt6abl  15459  dprdval  15516  dprd2dlem2  15553  dprd2da  15555  dprd2d2  15557  ablfacrplem  15578  ablfac1a  15582  ablfac1b  15583  ablfac1eulem  15585  ablfac1eu  15586  pgpfac1lem3a  15589  ablfaclem3  15600  dvdsrtr  15712  dvdsrmul1  15713  unitpropd  15757  isabvd  15863  zndvds0  16786  znunit  16799  cygth  16807  hmphindis  17782  ordthmeolem  17786  psmettri2  18293  ismet2  18316  xmettri2  18323  imasdsf1olem  18356  imasf1oxmet  18358  comet  18496  stdbdxmet  18498  nmogelb  18703  nmolb  18704  metdsge  18832  metdseq0  18837  iihalf2  18911  bndth  18936  evth  18937  ipcau2  19144  tchcphlem1  19145  tchcphlem2  19146  iscau3  19184  iscmet3  19199  bcthlem1  19230  bcth  19235  minveclem3b  19282  minveclem3  19283  minveclem4  19286  minveclem5  19287  pjthlem1  19291  pjthlem2  19292  pmltpclem1  19298  pmltpc  19300  ivthlem2  19302  ivthlem3  19303  ovolgelb  19329  ovolunlem1  19346  ovoliunlem2  19352  ovolshftlem1  19358  ovolscalem1  19362  ovolicc1  19365  ovolicc2lem3  19368  ioombl1lem4  19408  mbfmulc2lem  19492  mbfposb  19498  mbfaddlem  19505  mbfsup  19509  mbfinf  19510  mbflimsup  19511  i1fposd  19552  itg1ge0a  19556  mbfi1fseqlem4  19563  mbfi1fseqlem6  19565  mbfi1flimlem  19567  mbfi1flim  19568  itg2const2  19586  itg2seq  19587  itg2monolem1  19595  itg2i1fseq  19600  itg2addlem  19603  ibllem  19609  isibl  19610  isibl2  19611  iblitg  19613  dfitg  19614  cbvitg  19620  itgeq2  19622  itgvallem  19629  iblneg  19647  itgneg  19648  itggt0  19686  dvlip  19830  c1lip1  19834  dvfsumle  19858  dvfsumlem2  19864  dvfsumlem4  19866  dvfsum2  19871  mdeglt  19941  degltp1le  19949  deg1suble  19983  ply1divex  20012  plypf1  20084  dgrlb  20108  coemulc  20126  dgrsub  20143  quotval  20162  plydivlem4  20166  quotcan  20179  vieta1lem2  20181  aalioulem2  20203  aaliou3lem9  20220  ulmcn  20268  dvradcnv  20290  sincosq1sgn  20359  sincosq2sgn  20360  sincosq4sgn  20362  logltb  20447  cxpge0  20527  cxple2  20541  logreclem  20613  jensen  20780  emcllem7  20793  wilthlem1  20804  ftalem2  20809  ftalem3  20810  ftalem7  20814  fta  20815  sgmval  20878  mumul  20917  dvdsppwf1o  20924  musum  20929  chtublem  20948  chtub  20949  perfect1  20965  bcmono  21014  bclbnd  21017  bposlem1  21021  bposlem5  21025  lgslem1  21033  lgsval  21037  lgsdilem  21059  lgsne0  21070  lgsqrlem2  21079  lgsqrlem4  21081  lgseisenlem1  21086  lgseisenlem2  21087  lgsquadlem1  21091  lgsquadlem2  21092  lgsquadlem3  21093  lgsquad2lem2  21096  m1lgs  21099  2sqlem4  21104  2sqlem8a  21108  2sqblem  21114  dchrisumlema  21135  dchrisumlem2  21137  dchrisumlem3  21138  chpdifbndlem2  21201  pntrsumbnd2  21214  pntpbnd1  21233  pntibndlem3  21239  pntlemi  21251  pntleme  21255  pntlem3  21256  pnt3  21259  ostth2lem2  21281  ostth3  21285  ostth  21286  eupath2lem3  21654  eupath2  21655  konigsberg  21662  nmounbseqi  22231  nmounbseqiOLD  22232  isblo3i  22255  blo3i  22256  blocnilem  22258  siilem2  22306  normlem6  22570  normgt0  22582  norm3dif  22605  norm3lemt  22607  pjhthlem1  22846  pjige0  23146  nmcexi  23482  lnconi  23489  lnopcnbd  23492  lnfncnbd  23513  riesz1  23521  cnlnadjlem2  23524  cnlnadjlem8  23530  leopg  23578  leop2  23580  leoppos  23582  leopadd  23588  leopmuli  23589  leopmul2i  23591  pjssge0i  23622  pjdifnormi  23623  pjssposi  23628  pjssdif1i  23631  chcv1  23811  cvexch  23830  atcvatlem  23841  atcvat3i  23852  atdmd  23854  cdj3i  23897  addltmulALT  23902  xrofsup  24079  xrge0addgt0  24167  isofld  24188  ofldadd  24191  ofldmul  24192  ofldchr  24197  elrhmunit  24211  unitdivcld  24252  esumlub  24405  esumfsup  24413  esumcvg  24429  dya2ub  24573  itgeq12dv  24594  prob01  24624  orvcval  24668  ballotlemfc0  24703  ballotlemfcc  24704  ballotleme  24707  ballotlem4  24709  ballotlem1c  24718  ballotlemsval  24719  ballotlemieq  24727  lgamgulmlem1  24766  lgamgulmlem2  24767  lgamgulmlem3  24768  lgamgulmlem5  24770  lgambdd  24774  lgamcvglem  24777  erdszelem8  24837  erdsze2lem2  24843  abs2sqle  25073  abs2sqlt  25074  divelunit  25138  mulge0b  25144  mulle0b  25145  possumd  25162  pdivsq  25316  dvdspw  25317  poseq  25467  soseq  25468  sltval  25515  brbtwn2  25748  axlowdim2  25803  axlowdim  25804  axcontlem2  25808  axcontlem3  25809  axcontlem4  25810  axcontlem9  25815  axcontlem10  25816  axcontlem11  25817  axcontlem12  25818  cgrdegen  25842  brofs  25843  segconeu  25849  btwntriv2  25850  transportprops  25872  brifs  25881  ifscgr  25882  brcgr3  25884  cgrxfr  25893  brcolinear2  25896  colineardim1  25899  brfs  25917  idinside  25922  btwnconn1lem11  25935  btwnconn1lem12  25936  btwnconn1lem14  25938  brsegle  25946  seglerflx  25950  seglemin  25951  segleantisym  25953  btwnsegle  25955  outsideofeu  25969  outsidele  25970  fvray  25979  ltflcei  26140  lxflflp1  26142  mblfinlem  26143  mblfinlem2  26144  mblfinlem3  26145  itg2addnclem  26155  itg2addnclem2  26156  itg2gt0cn  26159  itggt0cn  26176  dvreasin  26179  areacirclem2  26181  areacirclem5  26185  areacirclem6  26186  areacirc  26187  nn0prpwlem  26215  nn0prpw  26216  seqpo  26341  incsequz2  26343  mettrifi  26353  heibor1lem  26408  rrncmslem  26431  elpell1qr2  26825  monotuz  26894  monotoddzzfi  26895  monotoddzz  26896  oddcomabszz  26897  rmxypos  26902  mzpcong  26927  congrep  26928  acongsym  26931  acongneg2  26932  acongtr  26933  acongeq12d  26934  dvdsabsmod0  26947  divalgmodcl  26948  jm2.18  26949  jm2.19lem2  26951  jm2.19lem3  26952  jm2.19lem4  26953  jm2.19  26954  jm2.25  26960  jm2.15nn0  26964  jm2.16nn0  26965  jm2.27  26969  rmydioph  26975  expdiophlem1  26982  expdiophlem2  26983  fnwe2lem2  27016  lmisfree  27180  evth2f  27553  evthf  27565  rfcnpre3  27571  fmul01  27577  fmul01lt1lem1  27581  climinf  27599  climinff  27604  stoweidlem3  27619  stoweidlem7  27623  stoweidlem15  27631  stoweidlem16  27632  stoweidlem18  27634  stoweidlem26  27642  stoweidlem27  27643  stoweidlem28  27644  stoweidlem31  27647  stoweidlem34  27650  stoweidlem36  27652  stoweidlem37  27653  stoweidlem41  27657  stoweidlem44  27660  stoweidlem45  27661  stoweidlem46  27662  stoweidlem48  27664  stoweidlem51  27667  stoweidlem55  27671  stoweidlem59  27675  stoweidlem60  27676  stoweidlem62  27678  ubmelm1fzo  27987  swrdccat3  28029  swrdccat3b  28031  lsatcv0eq  29530  oposlem  29666  oplecon1b  29684  opltcon1b  29688  atlatmstc  29802  cvlexch1  29811  cvlexch2  29812  cvlexchb2  29814  cvlatexchb2  29818  cvlatexch2  29820  cvlatcvr2  29825  cvlsupr2  29826  ishlat1  29835  hlsuprexch  29863  cvrexch  29902  cvrat  29904  atcvr0eq  29908  atcvrj0  29910  atltcvr  29917  cvrat3  29924  cvrat4  29925  cvrat42  29926  3noncolr2  29931  hlatcon2  29934  4noncolr3  29935  3dimlem1  29940  3dimlem2  29941  3dimlem3a  29942  3dimlem3  29943  3dimlem3OLDN  29944  3dimlem4a  29945  3dimlem4  29946  3dimlem4OLDN  29947  3dim1lem5  29948  3dim2  29950  3dim3  29951  ps-1  29959  ps-2  29960  3atlem5  29969  3atlem6  29970  lplni2  30019  lplnnle2at  30023  lplnnleat  30024  lplnnlelln  30025  lplnribN  30033  lplnexllnN  30046  lvoli2  30063  lvolnle3at  30064  lvolnleat  30065  lvolnlelln  30066  lvolnlelpln  30067  4atlem9  30085  4atlem10a  30086  4atlem11a  30089  4atlem11  30091  4atlem12a  30092  dalempnes  30133  dalemqnet  30134  dalem1  30141  dalemswapyzps  30172  dalemrotps  30173  dalem30  30184  dalem35  30189  lineset  30220  islinei  30222  psubspset  30226  psubspi2N  30230  snatpsubN  30232  2llnma1  30269  elpaddn0  30282  elpaddri  30284  elpaddat  30286  elpadd2at  30288  paddcom  30295  paddasslem12  30313  pmapjat1  30335  llnexchb2  30351  lhp2at0nle  30517  lhprelat3N  30522  4atexlemswapqr  30545  4atexlemcnd  30554  lautle  30566  lautcvr  30574  ltrnel  30621  ltrneq2  30630  trlnle  30668  cdlemc3  30675  cdlemd6  30685  cdleme3  30719  cdleme7aa  30724  cdleme7  30731  cdleme11c  30743  cdleme15c  30758  cdleme20y  30784  cdleme20m  30805  cdleme21b  30808  cdleme21c  30809  cdleme21at  30810  cdleme36a  30942  cdleme43bN  30972  cdleme43dN  30974  cdleme46f2g2  30975  cdleme46f2g1  30976  cdlemeg46c  30995  cdlemeg46nlpq  30999  cdlemb3  31088  cdlemg4d  31095  cdlemg6d  31103  cdlemg10c  31121  cdlemg12  31132  cdlemg27b  31178  djhcvat42  31898
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-rab 2675  df-v 2918  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-sn 3780  df-pr 3781  df-op 3783  df-br 4173
  Copyright terms: Public domain W3C validator