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

Theorem breq2d 4137
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 4129 . 2  |-  ( A  =  B  ->  ( C R A  <->  C R B ) )
31, 2syl 15 1  |-  ( ph  ->  ( C R A  <-> 
C R B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    = wceq 1647   class class class wbr 4125
This theorem is referenced by:  breqtrd  4149  sbcbr1g  4176  pofun  4433  csbfv12g  5642  isorel  5946  soisores  5947  soisoi  5948  isocnv  5950  isotr  5956  f1owe  5973  f1oweALT  5974  caovordig  6152  caovordg  6154  caovord  6158  frxp  6353  xporderlem  6354  fnwelem  6358  th3qlem2  6908  difsnen  7087  domdifsn  7088  unfilem3  7270  domunfican  7276  marypha1lem  7333  marypha1  7334  r1sdom  7593  sdomsdomcardi  7751  alephordi  7848  pwcdadom  7989  sornom  8050  axdclem  8293  pwcfsdom  8352  elgch  8391  winalim2  8465  rankcf  8546  inatsk  8547  pinq  8698  nqereu  8700  ltaddnq  8745  ltrnq  8750  archnq  8751  addclprlem1  8787  mulclprlem  8790  1idpr  8800  ltaprlem  8815  ltapr  8816  prlem936  8818  ltasr  8869  mulgt0sr  8874  sqgt0sr  8875  map2psrpr  8879  axpre-ltadd  8936  axpre-mulgt0  8937  axpre-sup  8938  ltsubadd2  9392  lesubadd2  9394  ltaddpos2  9412  posdif  9414  lesub1  9415  ltnegcon1  9422  lenegcon1  9425  addge02  9432  mulge0  9438  msqge0  9442  ltordlem  9445  prodgt0  9748  prodgt02  9749  prodge02  9751  ltmulgt12  9764  lemulge12  9766  ltdivmul  9775  ledivmul  9776  ledivmulOLD  9777  ltdivmul2  9778  lt2mul2div  9779  ledivmul2  9780  ledivmul2OLD  9781  ltrec  9784  ltrec1  9790  ltdiv23  9794  lediv23  9795  nnge1  9919  halfpos  10091  lt2halves  10095  addltmul  10096  avglt2  10099  avgle2  10101  nnrecl  10112  zltlem1  10221  gtndiv  10240  rebtwnz  10466  xrmax1  10656  max1ALT  10667  qbtwnre  10678  xralrple  10684  xltnegi  10695  xmulval  10704  xsubge0  10733  xposdif  10734  xlesubadd  10735  fllelt  11093  flbi  11110  btwnzge0  11117  om2uzlti  11177  monoord  11240  sermono  11242  expval  11271  expnbnd  11395  discr1  11402  discr  11403  facwordi  11467  hashtpg  11578  seqcoll  11599  seqcoll2  11600  cnpart  11932  sqrlem6  11940  sqrmo  11944  resqreu  11945  resqrcl  11946  resqrthlem  11947  sqrneg  11960  sqreulem  12050  sqreu  12051  sqrthlem  12053  eqsqrd  12058  limsuple  12159  rlimcld2  12259  rlimrege0  12260  o1compt  12268  climserle  12343  caurcvgr  12354  fsum00  12464  fsumabs  12467  climcndslem2  12517  climcnds  12518  supcvg  12522  georeclim  12536  geoisumr  12542  cvgrat  12547  sin01bnd  12673  cos01bnd  12674  ruclem1  12717  ruclem9  12724  ruclem12  12727  dvdsaddr  12776  dvdssub  12777  dvdssubr  12778  dvdsfac  12791  dvdsmod  12793  oddp1even  12797  divalglem0  12800  divalglem2  12802  divalglem4  12803  divalglem5  12804  divalglem9  12808  divalg  12810  divalg2  12812  divalgmod  12813  ndvdssub  12814  ndvdsadd  12815  bitsfval  12822  bitsval  12823  bits0  12827  bitsp1  12830  bitsfzolem  12833  bitsfzo  12834  bitscmp  12837  bitsinv1lem  12840  bitsshft  12874  gcdcllem1  12898  dvdslegcd  12903  bezoutlem4  12928  dvdssqim  12940  dvdsmulgcd  12941  dvdssq  12947  nn0seqcvgd  12948  coprmdvds  12989  coprmdvds2  12990  isprm6  12996  prmdvdsexp  13001  prmdvdsexpr  13003  prmfac1  13005  divgcdodd  13006  rpmul  13010  hashdvds  13051  phiprmpw  13052  eulerthlem2  13058  prmdiv  13061  prmdiveq  13062  odzval  13064  odzcllem  13065  odzdvds  13068  opoe  13072  omoe  13073  pythagtriplem11  13086  pythagtriplem13  13088  pythagtrip  13095  pceulem  13106  pczndvds2  13127  pcdvdsb  13129  pc2dvds  13139  pcz  13141  pcprmpw2  13142  pcaddlem  13144  pcmpt  13148  prmpwdvds  13159  pockthlem  13160  prmreclem2  13172  prmreclem4  13174  4sqlem11  13210  vdwlem9  13244  rami  13270  ramlb  13274  0ram  13275  ramz2  13279  ramub1lem1  13281  imasleval  13653  subsubc  13937  pospo  14317  mulgval  14779  oddvdsnn0  15069  odmulg  15079  pgpfi1  15116  pgpfi  15126  slwispgp  15132  pgpssslw  15135  subgslw  15137  sylow2alem2  15139  sylow2blem3  15143  fislw  15146  efgi  15238  efgval2  15243  efgsrel  15253  efgredlemb  15265  lt6abl  15391  dprdval  15448  dprd2dlem2  15485  dprd2da  15487  dprd2d2  15489  ablfacrplem  15510  ablfac1a  15514  ablfac1b  15515  ablfac1eulem  15517  ablfac1eu  15518  pgpfac1lem3a  15521  ablfaclem3  15532  dvdsrtr  15644  dvdsrmul1  15645  unitpropd  15689  isabvd  15795  zndvds0  16721  znunit  16734  cygth  16742  hmphindis  17705  ordthmeolem  17709  ismet2  18111  xmettri2  18118  imasdsf1olem  18150  imasf1oxmet  18152  comet  18272  stdbdxmet  18274  nmogelb  18438  nmolb  18439  metdsge  18567  metdseq0  18572  iihalf2  18646  bndth  18671  evth  18672  ipcau2  18879  tchcphlem1  18880  tchcphlem2  18881  iscau3  18919  iscmet3  18934  bcthlem1  18961  bcth  18966  minveclem3b  19007  minveclem3  19008  minveclem4  19011  minveclem5  19012  pjthlem1  19016  pjthlem2  19017  pmltpclem1  19023  pmltpc  19025  ivthlem2  19027  ivthlem3  19028  ovolgelb  19054  ovolunlem1  19071  ovoliunlem2  19077  ovolshftlem1  19083  ovolscalem1  19087  ovolicc1  19090  ovolicc2lem3  19093  ioombl1lem4  19133  mbfmulc2lem  19217  mbfposb  19223  mbfaddlem  19230  mbfsup  19234  mbfinf  19235  mbflimsup  19236  i1fposd  19277  itg1ge0a  19281  mbfi1fseqlem4  19288  mbfi1fseqlem6  19290  mbfi1flimlem  19292  mbfi1flim  19293  itg2const2  19311  itg2seq  19312  itg2monolem1  19320  itg2i1fseq  19325  itg2addlem  19328  ibllem  19334  isibl  19335  isibl2  19336  iblitg  19338  dfitg  19339  cbvitg  19345  itgeq2  19347  itgvallem  19354  iblneg  19372  itgneg  19373  itggt0  19411  dvlip  19555  c1lip1  19559  dvfsumle  19583  dvfsumlem2  19589  dvfsumlem4  19591  dvfsum2  19596  mdeglt  19666  degltp1le  19674  deg1suble  19708  ply1divex  19737  plypf1  19809  dgrlb  19833  coemulc  19851  dgrsub  19868  quotval  19887  plydivlem4  19891  quotcan  19904  vieta1lem2  19906  aalioulem2  19928  aaliou3lem9  19945  ulmcn  19993  dvradcnv  20015  sincosq1sgn  20084  sincosq2sgn  20085  sincosq4sgn  20087  logltb  20172  cxpge0  20252  cxple2  20266  logreclem  20338  jensen  20505  emcllem7  20518  wilthlem1  20529  ftalem2  20534  ftalem3  20535  ftalem7  20539  fta  20540  sgmval  20603  mumul  20642  dvdsppwf1o  20649  musum  20654  chtublem  20673  chtub  20674  perfect1  20690  bcmono  20739  bclbnd  20742  bposlem1  20746  bposlem5  20750  lgslem1  20758  lgsval  20762  lgsdilem  20784  lgsne0  20795  lgsqrlem2  20804  lgsqrlem4  20806  lgseisenlem1  20811  lgseisenlem2  20812  lgsquadlem1  20816  lgsquadlem2  20817  lgsquadlem3  20818  lgsquad2lem2  20821  m1lgs  20824  2sqlem4  20829  2sqlem8a  20833  2sqblem  20839  dchrisumlema  20860  dchrisumlem2  20862  dchrisumlem3  20863  chpdifbndlem2  20926  pntrsumbnd2  20939  pntpbnd1  20958  pntibndlem3  20964  pntlemi  20976  pntleme  20980  pntlem3  20981  pnt3  20984  ostth2lem2  21006  ostth3  21010  ostth  21011  nmounbseqi  21668  nmounbseqiOLD  21669  isblo3i  21692  blo3i  21693  blocnilem  21695  siilem2  21743  normlem6  22007  normgt0  22019  norm3dif  22042  norm3lemt  22044  pjhthlem1  22283  pjige0  22583  nmcexi  22919  lnconi  22926  lnopcnbd  22929  lnfncnbd  22950  riesz1  22958  cnlnadjlem2  22961  cnlnadjlem8  22967  leopg  23015  leop2  23017  leoppos  23019  leopadd  23025  leopmuli  23026  leopmul2i  23028  pjssge0i  23059  pjdifnormi  23060  pjssposi  23065  pjssdif1i  23068  chcv1  23248  cvexch  23267  atcvatlem  23278  atcvat3i  23289  atdmd  23291  cdj3i  23334  addltmulALT  23339  xlt2addrd  23524  xrofsup  23526  bcm1n  23552  xrge0addgt0  23605  elrhmunit  23623  unitdivcld  23654  xrge0iifiso  23676  esumlub  23917  esumfsup  23925  esumcvg  23941  measssd  24032  dya2ub  24083  itgeq12dv  24104  prob01  24119  orvcval  24163  ballotlemfc0  24198  ballotlemfcc  24199  ballotleme  24202  ballotlem4  24204  ballotlemic  24212  ballotlem1c  24213  ballotlemsval  24214  ballotlemieq  24222  lgamgulmlem1  24261  lgamgulmlem2  24262  lgamgulmlem3  24263  lgamgulmlem5  24265  lgambdd  24269  lgamcvglem  24272  erdszelem8  24332  erdsze2lem2  24338  eupath2lem3  24490  eupath2  24491  konigsberg  24498  abs2sqle  24603  abs2sqlt  24604  divelunit  24669  mulge0b  24675  mulle0b  24676  possumd  24693  pdivsq  24843  dvdspw  24844  poseq  24994  soseq  24995  sltval  25042  brbtwn2  25275  axlowdim2  25330  axlowdim  25331  axcontlem2  25335  axcontlem3  25336  axcontlem4  25337  axcontlem9  25342  axcontlem10  25343  axcontlem11  25344  axcontlem12  25345  cgrdegen  25369  brofs  25370  segconeu  25376  btwntriv2  25377  transportprops  25399  brifs  25408  ifscgr  25409  brcgr3  25411  cgrxfr  25420  brcolinear2  25423  colineardim1  25426  brfs  25444  idinside  25449  btwnconn1lem11  25462  btwnconn1lem12  25463  btwnconn1lem14  25465  brsegle  25473  seglerflx  25477  seglemin  25478  segleantisym  25480  btwnsegle  25482  outsideofeu  25496  outsidele  25497  fvray  25506  ltflcei  25668  lxflflp1  25670  itg2addnclem  25675  itg2addnclem2  25676  itg2gt0cn  25678  itggt0cn  25695  dvreasin  25698  areacirclem2  25700  areacirclem5  25704  areacirclem6  25705  areacirc  25706  nn0prpwlem  25745  nn0prpw  25746  seqpo  25964  incsequz2  25966  mettrifi  25980  heibor1lem  26039  rrncmslem  26062  elpell1qr2  26463  monotuz  26532  monotoddzzfi  26533  monotoddzz  26534  oddcomabszz  26535  rmxypos  26540  mzpcong  26565  congrep  26566  acongsym  26569  acongneg2  26570  acongtr  26571  acongeq12d  26572  dvdsabsmod0  26585  divalgmodcl  26586  jm2.18  26587  jm2.19lem2  26589  jm2.19lem3  26590  jm2.19lem4  26591  jm2.19  26592  jm2.25  26598  jm2.15nn0  26602  jm2.16nn0  26603  jm2.27  26607  rmydioph  26613  expdiophlem1  26620  expdiophlem2  26621  fnwe2lem2  26654  lmisfree  26818  evth2f  27192  evthf  27204  rfcnpre3  27210  fmul01  27216  fmul01lt1lem1  27220  climinf  27238  climinff  27243  stoweidlem3  27258  stoweidlem7  27262  stoweidlem13  27268  stoweidlem15  27270  stoweidlem16  27271  stoweidlem18  27273  stoweidlem24  27279  stoweidlem26  27281  stoweidlem27  27282  stoweidlem28  27283  stoweidlem31  27286  stoweidlem34  27289  stoweidlem36  27291  stoweidlem37  27292  stoweidlem41  27296  stoweidlem44  27299  stoweidlem45  27300  stoweidlem46  27301  stoweidlem48  27303  stoweidlem51  27306  stoweidlem55  27310  stoweidlem59  27314  stoweidlem60  27315  stoweidlem62  27317  lsatcv0eq  29308  oposlem  29444  oplecon1b  29462  opltcon1b  29466  atlatmstc  29580  cvlexch1  29589  cvlexch2  29590  cvlexchb2  29592  cvlatexchb2  29596  cvlatexch2  29598  cvlatcvr2  29603  cvlsupr2  29604  ishlat1  29613  hlsuprexch  29641  cvrexch  29680  cvrat  29682  atcvr0eq  29686  atcvrj0  29688  atltcvr  29695  cvrat3  29702  cvrat4  29703  cvrat42  29704  3noncolr2  29709  hlatcon2  29712  4noncolr3  29713  3dimlem1  29718  3dimlem2  29719  3dimlem3a  29720  3dimlem3  29721  3dimlem3OLDN  29722  3dimlem4a  29723  3dimlem4  29724  3dimlem4OLDN  29725  3dim1lem5  29726  3dim2  29728  3dim3  29729  ps-1  29737  ps-2  29738  3atlem5  29747  3atlem6  29748  lplni2  29797  lplnnle2at  29801  lplnnleat  29802  lplnnlelln  29803  lplnribN  29811  lplnexllnN  29824  lvoli2  29841  lvolnle3at  29842  lvolnleat  29843  lvolnlelln  29844  lvolnlelpln  29845  4atlem9  29863  4atlem10a  29864  4atlem11a  29867  4atlem11  29869  4atlem12a  29870  dalempnes  29911  dalemqnet  29912  dalem1  29919  dalemswapyzps  29950  dalemrotps  29951  dalem30  29962  dalem35  29967  lineset  29998  islinei  30000  psubspset  30004  psubspi2N  30008  snatpsubN  30010  2llnma1  30047  elpaddn0  30060  elpaddri  30062  elpaddat  30064  elpadd2at  30066  paddcom  30073  paddasslem12  30091  pmapjat1  30113  llnexchb2  30129  lhp2at0nle  30295  lhprelat3N  30300  4atexlemswapqr  30323  4atexlemcnd  30332  lautle  30344  lautcvr  30352  ltrnel  30399  ltrneq2  30408  trlnle  30446  cdlemc3  30453  cdlemd6  30463  cdleme3  30497  cdleme7aa  30502  cdleme7  30509  cdleme11c  30521  cdleme15c  30536  cdleme20y  30562  cdleme20m  30583  cdleme21b  30586  cdleme21c  30587  cdleme21at  30588  cdleme36a  30720  cdleme43bN  30750  cdleme43dN  30752  cdleme46f2g2  30753  cdleme46f2g1  30754  cdlemeg46c  30773  cdlemeg46nlpq  30777  cdlemb3  30866  cdlemg4d  30873  cdlemg6d  30881  cdlemg10c  30899  cdlemg12  30910  cdlemg27b  30956  djhcvat42  31676
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1551  ax-5 1562  ax-17 1621  ax-9 1659  ax-8 1680  ax-6 1734  ax-7 1739  ax-11 1751  ax-12 1937  ax-ext 2347
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 937  df-tru 1324  df-ex 1547  df-nf 1550  df-sb 1654  df-clab 2353  df-cleq 2359  df-clel 2362  df-nfc 2491  df-rab 2637  df-v 2875  df-dif 3241  df-un 3243  df-in 3245  df-ss 3252  df-nul 3544  df-if 3655  df-sn 3735  df-pr 3736  df-op 3738  df-br 4126
  Copyright terms: Public domain W3C validator