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

Theorem breq2d 4227
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 4219 . 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 178    = wceq 1653   class class class wbr 4215
This theorem is referenced by:  breqtrd  4239  sbcbr1g  4266  pofun  4522  csbfv12g  5741  isorel  6049  soisores  6050  soisoi  6051  isocnv  6053  isotr  6059  f1owe  6076  f1oweALT  6077  caovordig  6255  caovordg  6257  caovord  6261  frxp  6459  xporderlem  6460  fnwelem  6464  th3qlem2  7014  difsnen  7193  domdifsn  7194  unfilem3  7376  domunfican  7382  marypha1lem  7441  marypha1  7442  r1sdom  7703  sdomsdomcardi  7863  alephordi  7960  pwcdadom  8101  sornom  8162  axdclem  8404  pwcfsdom  8463  elgch  8502  winalim2  8576  rankcf  8657  inatsk  8658  pinq  8809  nqereu  8811  ltaddnq  8856  ltrnq  8861  archnq  8862  addclprlem1  8898  mulclprlem  8901  1idpr  8911  ltaprlem  8926  ltapr  8927  prlem936  8929  ltasr  8980  mulgt0sr  8985  sqgt0sr  8986  map2psrpr  8990  axpre-ltadd  9047  axpre-mulgt0  9048  axpre-sup  9049  ltsubadd2  9504  lesubadd2  9506  ltaddpos2  9524  posdif  9526  lesub1  9527  ltnegcon1  9534  lenegcon1  9537  addge02  9544  mulge0  9550  msqge0  9554  ltordlem  9557  prodgt0  9860  prodgt02  9861  prodge02  9863  ltmulgt12  9876  lemulge12  9878  ltdivmul  9887  ledivmul  9888  ledivmulOLD  9889  ltdivmul2  9890  lt2mul2div  9891  ledivmul2  9892  ledivmul2OLD  9893  ltrec  9896  ltrec1  9902  ltdiv23  9906  lediv23  9907  nnge1  10031  halfpos  10203  lt2halves  10207  addltmul  10208  avglt2  10211  avgle2  10213  nnrecl  10224  zltlem1  10333  gtndiv  10352  rebtwnz  10578  xrmax1  10768  max1ALT  10779  qbtwnre  10790  xralrple  10796  xltnegi  10807  xmulval  10816  xsubge0  10845  xposdif  10846  xlesubadd  10847  fllelt  11211  flbi  11228  btwnzge0  11235  om2uzlti  11295  monoord  11358  sermono  11360  expval  11389  expnbnd  11513  discr1  11520  discr  11521  facwordi  11585  hashtpg  11696  seqcoll  11717  seqcoll2  11718  cnpart  12050  sqrlem6  12058  sqrmo  12062  resqreu  12063  resqrcl  12064  resqrthlem  12065  sqrneg  12078  sqreulem  12168  sqreu  12169  sqrthlem  12171  eqsqrd  12176  limsuple  12277  rlimcld2  12377  rlimrege0  12378  o1compt  12386  climserle  12461  caurcvgr  12472  fsum00  12582  fsumabs  12585  climcndslem2  12635  climcnds  12636  supcvg  12640  georeclim  12654  geoisumr  12660  cvgrat  12665  sin01bnd  12791  cos01bnd  12792  ruclem1  12835  ruclem9  12842  ruclem12  12845  dvdsaddr  12894  dvdssub  12895  dvdssubr  12896  dvdsfac  12909  dvdsmod  12911  oddp1even  12915  divalglem0  12918  divalglem2  12920  divalglem4  12921  divalglem5  12922  divalglem9  12926  divalg  12928  divalg2  12930  divalgmod  12931  ndvdssub  12932  ndvdsadd  12933  bitsfval  12940  bitsval  12941  bits0  12945  bitsp1  12948  bitsfzolem  12951  bitsfzo  12952  bitscmp  12955  bitsinv1lem  12958  bitsshft  12992  gcdcllem1  13016  dvdslegcd  13021  bezoutlem4  13046  dvdssqim  13058  dvdsmulgcd  13059  dvdssq  13065  nn0seqcvgd  13066  coprmdvds  13107  coprmdvds2  13108  isprm6  13114  prmdvdsexp  13119  prmdvdsexpr  13121  prmfac1  13123  divgcdodd  13124  rpmul  13128  hashdvds  13169  phiprmpw  13170  eulerthlem2  13176  prmdiv  13179  prmdiveq  13180  odzval  13182  odzcllem  13183  odzdvds  13186  opoe  13190  omoe  13191  pythagtriplem11  13204  pythagtriplem13  13206  pythagtrip  13213  pceulem  13224  pczndvds2  13245  pcdvdsb  13247  pc2dvds  13257  pcz  13259  pcprmpw2  13260  pcaddlem  13262  pcmpt  13266  prmpwdvds  13277  pockthlem  13278  prmreclem2  13290  prmreclem4  13292  4sqlem11  13328  vdwlem9  13362  rami  13388  ramlb  13392  0ram  13393  ramz2  13397  ramub1lem1  13399  imasleval  13771  subsubc  14055  pospo  14435  mulgval  14897  oddvdsnn0  15187  odmulg  15197  pgpfi1  15234  pgpfi  15244  slwispgp  15250  pgpssslw  15253  subgslw  15255  sylow2alem2  15257  sylow2blem3  15261  fislw  15264  efgi  15356  efgval2  15361  efgsrel  15371  efgredlemb  15383  lt6abl  15509  dprdval  15566  dprd2dlem2  15603  dprd2da  15605  dprd2d2  15607  ablfacrplem  15628  ablfac1a  15632  ablfac1b  15633  ablfac1eulem  15635  ablfac1eu  15636  pgpfac1lem3a  15639  ablfaclem3  15650  dvdsrtr  15762  dvdsrmul1  15763  unitpropd  15807  isabvd  15913  zndvds0  16836  znunit  16849  cygth  16857  hmphindis  17834  ordthmeolem  17838  psmettri2  18345  ismet2  18368  xmettri2  18375  imasdsf1olem  18408  imasf1oxmet  18410  comet  18548  stdbdxmet  18550  nmogelb  18755  nmolb  18756  metdsge  18884  metdseq0  18889  iihalf2  18963  bndth  18988  evth  18989  ipcau2  19196  tchcphlem1  19197  tchcphlem2  19198  iscau3  19236  iscmet3  19251  bcthlem1  19282  bcth  19287  minveclem3b  19334  minveclem3  19335  minveclem4  19338  minveclem5  19339  pjthlem1  19343  pjthlem2  19344  pmltpclem1  19350  pmltpc  19352  ivthlem2  19354  ivthlem3  19355  ovolgelb  19381  ovolunlem1  19398  ovoliunlem2  19404  ovolshftlem1  19410  ovolscalem1  19414  ovolicc1  19417  ovolicc2lem3  19420  ioombl1lem4  19460  mbfmulc2lem  19542  mbfposb  19548  mbfaddlem  19555  mbfsup  19559  mbfinf  19560  mbflimsup  19561  i1fposd  19602  itg1ge0a  19606  mbfi1fseqlem4  19613  mbfi1fseqlem6  19615  mbfi1flimlem  19617  mbfi1flim  19618  itg2const2  19636  itg2seq  19637  itg2monolem1  19645  itg2i1fseq  19650  itg2addlem  19653  ibllem  19659  isibl  19660  isibl2  19661  iblitg  19663  dfitg  19664  cbvitg  19670  itgeq2  19672  itgvallem  19679  iblneg  19697  itgneg  19698  itggt0  19736  dvlip  19882  c1lip1  19886  dvfsumle  19910  dvfsumlem2  19916  dvfsumlem4  19918  dvfsum2  19923  mdeglt  19993  degltp1le  20001  deg1suble  20035  ply1divex  20064  plypf1  20136  dgrlb  20160  coemulc  20178  dgrsub  20195  quotval  20214  plydivlem4  20218  quotcan  20231  vieta1lem2  20233  aalioulem2  20255  aaliou3lem9  20272  ulmcn  20320  dvradcnv  20342  sincosq1sgn  20411  sincosq2sgn  20412  sincosq4sgn  20414  logltb  20499  cxpge0  20579  cxple2  20593  logreclem  20665  jensen  20832  emcllem7  20845  wilthlem1  20856  ftalem2  20861  ftalem3  20862  ftalem7  20866  fta  20867  sgmval  20930  mumul  20969  dvdsppwf1o  20976  musum  20981  chtublem  21000  chtub  21001  perfect1  21017  bcmono  21066  bclbnd  21069  bposlem1  21073  bposlem5  21077  lgslem1  21085  lgsval  21089  lgsdilem  21111  lgsne0  21122  lgsqrlem2  21131  lgsqrlem4  21133  lgseisenlem1  21138  lgseisenlem2  21139  lgsquadlem1  21143  lgsquadlem2  21144  lgsquadlem3  21145  lgsquad2lem2  21148  m1lgs  21151  2sqlem4  21156  2sqlem8a  21160  2sqblem  21166  dchrisumlema  21187  dchrisumlem2  21189  dchrisumlem3  21190  chpdifbndlem2  21253  pntrsumbnd2  21266  pntpbnd1  21285  pntibndlem3  21291  pntlemi  21303  pntleme  21307  pntlem3  21308  pnt3  21311  ostth2lem2  21333  ostth3  21337  ostth  21338  eupath2lem3  21706  eupath2  21707  konigsberg  21714  nmounbseqi  22283  nmounbseqiOLD  22284  isblo3i  22307  blo3i  22308  blocnilem  22310  siilem2  22358  normlem6  22622  normgt0  22634  norm3dif  22657  norm3lemt  22659  pjhthlem1  22898  pjige0  23198  nmcexi  23534  lnconi  23541  lnopcnbd  23544  lnfncnbd  23565  riesz1  23573  cnlnadjlem2  23576  cnlnadjlem8  23582  leopg  23630  leop2  23632  leoppos  23634  leopadd  23640  leopmuli  23641  leopmul2i  23643  pjssge0i  23674  pjdifnormi  23675  pjssposi  23680  pjssdif1i  23683  chcv1  23863  cvexch  23882  atcvatlem  23893  atcvat3i  23904  atdmd  23906  cdj3i  23949  addltmulALT  23954  xrofsup  24131  xrge0addgt0  24219  isofld  24240  ofldadd  24243  ofldmul  24244  ofldchr  24249  elrhmunit  24263  unitdivcld  24304  esumlub  24457  esumfsup  24465  esumcvg  24481  dya2ub  24625  itgeq12dv  24646  prob01  24676  orvcval  24720  ballotlemfc0  24755  ballotlemfcc  24756  ballotleme  24759  ballotlem4  24761  ballotlem1c  24770  ballotlemsval  24771  ballotlemieq  24779  lgamgulmlem1  24818  lgamgulmlem2  24819  lgamgulmlem3  24820  lgamgulmlem5  24822  lgambdd  24826  lgamcvglem  24829  erdszelem8  24889  erdsze2lem2  24895  abs2sqle  25125  abs2sqlt  25126  divelunit  25190  mulge0b  25196  mulle0b  25197  possumd  25214  pdivsq  25373  dvdspw  25374  poseq  25533  soseq  25534  sltval  25607  brbtwn2  25849  axlowdim2  25904  axlowdim  25905  axcontlem2  25909  axcontlem3  25910  axcontlem4  25911  axcontlem9  25916  axcontlem10  25917  axcontlem11  25918  axcontlem12  25919  cgrdegen  25943  brofs  25944  segconeu  25950  btwntriv2  25951  transportprops  25973  brifs  25982  ifscgr  25983  brcgr3  25985  cgrxfr  25994  brcolinear2  25997  colineardim1  26000  brfs  26018  idinside  26023  btwnconn1lem11  26036  btwnconn1lem12  26037  btwnconn1lem14  26039  brsegle  26047  seglerflx  26051  seglemin  26052  segleantisym  26054  btwnsegle  26056  outsideofeu  26070  outsidele  26071  fvray  26080  ltflcei  26247  lxflflp1  26249  cos2h  26251  tan2h  26252  mblfinlem2  26255  mblfinlem3  26256  mblfinlem4  26257  dvtanlem  26267  itg2addnclem  26269  itg2addnclem2  26270  itg2gt0cn  26273  itggt0cn  26290  ftc1anclem5  26297  dvreasin  26303  areacirclem1  26305  areacirclem4  26308  areacirclem5  26309  areacirc  26310  nn0prpwlem  26338  nn0prpw  26339  seqpo  26464  incsequz2  26466  mettrifi  26476  heibor1lem  26531  rrncmslem  26554  elpell1qr2  26948  monotuz  27017  monotoddzzfi  27018  monotoddzz  27019  oddcomabszz  27020  rmxypos  27025  mzpcong  27050  congrep  27051  acongsym  27054  acongneg2  27055  acongtr  27056  acongeq12d  27057  dvdsabsmod0  27070  divalgmodcl  27071  jm2.18  27072  jm2.19lem2  27074  jm2.19lem3  27075  jm2.19lem4  27076  jm2.19  27077  jm2.25  27083  jm2.15nn0  27087  jm2.16nn0  27088  jm2.27  27092  rmydioph  27098  expdiophlem1  27105  expdiophlem2  27106  fnwe2lem2  27139  lmisfree  27302  evth2f  27675  evthf  27687  rfcnpre3  27693  fmul01  27699  fmul01lt1lem1  27703  climinf  27721  climinff  27726  stoweidlem3  27741  stoweidlem7  27745  stoweidlem15  27753  stoweidlem16  27754  stoweidlem18  27756  stoweidlem26  27764  stoweidlem27  27765  stoweidlem28  27766  stoweidlem31  27769  stoweidlem34  27772  stoweidlem36  27774  stoweidlem37  27775  stoweidlem41  27779  stoweidlem44  27782  stoweidlem45  27783  stoweidlem46  27784  stoweidlem48  27786  stoweidlem51  27789  stoweidlem55  27793  stoweidlem59  27797  stoweidlem60  27798  stoweidlem62  27800  leaddle0  28115  ubmelm1fzo  28149  subsubelfzo0  28157  2submod  28174  swrdccat3blem  28251  2cshw2lem2  28286  2cshwmod  28290  nbhashuvtx1  28430  lsatcv0eq  29918  oposlem  30054  oplecon1b  30072  opltcon1b  30076  atlatmstc  30190  cvlexch1  30199  cvlexch2  30200  cvlexchb2  30202  cvlatexchb2  30206  cvlatexch2  30208  cvlatcvr2  30213  cvlsupr2  30214  ishlat1  30223  hlsuprexch  30251  cvrexch  30290  cvrat  30292  atcvr0eq  30296  atcvrj0  30298  atltcvr  30305  cvrat3  30312  cvrat4  30313  cvrat42  30314  3noncolr2  30319  hlatcon2  30322  4noncolr3  30323  3dimlem1  30328  3dimlem2  30329  3dimlem3a  30330  3dimlem3  30331  3dimlem3OLDN  30332  3dimlem4a  30333  3dimlem4  30334  3dimlem4OLDN  30335  3dim1lem5  30336  3dim2  30338  3dim3  30339  ps-1  30347  ps-2  30348  3atlem5  30357  3atlem6  30358  lplni2  30407  lplnnle2at  30411  lplnnleat  30412  lplnnlelln  30413  lplnribN  30421  lplnexllnN  30434  lvoli2  30451  lvolnle3at  30452  lvolnleat  30453  lvolnlelln  30454  lvolnlelpln  30455  4atlem9  30473  4atlem10a  30474  4atlem11a  30477  4atlem11  30479  4atlem12a  30480  dalempnes  30521  dalemqnet  30522  dalem1  30529  dalemswapyzps  30560  dalemrotps  30561  dalem30  30572  dalem35  30577  lineset  30608  islinei  30610  psubspset  30614  psubspi2N  30618  snatpsubN  30620  2llnma1  30657  elpaddn0  30670  elpaddri  30672  elpaddat  30674  elpadd2at  30676  paddcom  30683  paddasslem12  30701  pmapjat1  30723  llnexchb2  30739  lhp2at0nle  30905  lhprelat3N  30910  4atexlemswapqr  30933  4atexlemcnd  30942  lautle  30954  lautcvr  30962  ltrnel  31009  ltrneq2  31018  trlnle  31056  cdlemc3  31063  cdlemd6  31073  cdleme3  31107  cdleme7aa  31112  cdleme7  31119  cdleme11c  31131  cdleme15c  31146  cdleme20y  31172  cdleme20m  31193  cdleme21b  31196  cdleme21c  31197  cdleme21at  31198  cdleme36a  31330  cdleme43bN  31360  cdleme43dN  31362  cdleme46f2g2  31363  cdleme46f2g1  31364  cdlemeg46c  31383  cdlemeg46nlpq  31387  cdlemb3  31476  cdlemg4d  31483  cdlemg6d  31491  cdlemg10c  31509  cdlemg12  31520  cdlemg27b  31566  djhcvat42  32286
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-rab 2716  df-v 2960  df-dif 3325  df-un 3327  df-in 3329  df-ss 3336  df-nul 3631  df-if 3742  df-sn 3822  df-pr 3823  df-op 3825  df-br 4216
  Copyright terms: Public domain W3C validator