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

Theorem breq2d 4216
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 4208 . 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 1652   class class class wbr 4204
This theorem is referenced by:  breqtrd  4228  sbcbr1g  4255  pofun  4511  csbfv12g  5729  isorel  6037  soisores  6038  soisoi  6039  isocnv  6041  isotr  6047  f1owe  6064  f1oweALT  6065  caovordig  6243  caovordg  6245  caovord  6249  frxp  6447  xporderlem  6448  fnwelem  6452  th3qlem2  7002  difsnen  7181  domdifsn  7182  unfilem3  7364  domunfican  7370  marypha1lem  7429  marypha1  7430  r1sdom  7689  sdomsdomcardi  7847  alephordi  7944  pwcdadom  8085  sornom  8146  axdclem  8388  pwcfsdom  8447  elgch  8486  winalim2  8560  rankcf  8641  inatsk  8642  pinq  8793  nqereu  8795  ltaddnq  8840  ltrnq  8845  archnq  8846  addclprlem1  8882  mulclprlem  8885  1idpr  8895  ltaprlem  8910  ltapr  8911  prlem936  8913  ltasr  8964  mulgt0sr  8969  sqgt0sr  8970  map2psrpr  8974  axpre-ltadd  9031  axpre-mulgt0  9032  axpre-sup  9033  ltsubadd2  9488  lesubadd2  9490  ltaddpos2  9508  posdif  9510  lesub1  9511  ltnegcon1  9518  lenegcon1  9521  addge02  9528  mulge0  9534  msqge0  9538  ltordlem  9541  prodgt0  9844  prodgt02  9845  prodge02  9847  ltmulgt12  9860  lemulge12  9862  ltdivmul  9871  ledivmul  9872  ledivmulOLD  9873  ltdivmul2  9874  lt2mul2div  9875  ledivmul2  9876  ledivmul2OLD  9877  ltrec  9880  ltrec1  9886  ltdiv23  9890  lediv23  9891  nnge1  10015  halfpos  10187  lt2halves  10191  addltmul  10192  avglt2  10195  avgle2  10197  nnrecl  10208  zltlem1  10317  gtndiv  10336  rebtwnz  10562  xrmax1  10752  max1ALT  10763  qbtwnre  10774  xralrple  10780  xltnegi  10791  xmulval  10800  xsubge0  10829  xposdif  10830  xlesubadd  10831  fllelt  11194  flbi  11211  btwnzge0  11218  om2uzlti  11278  monoord  11341  sermono  11343  expval  11372  expnbnd  11496  discr1  11503  discr  11504  facwordi  11568  hashtpg  11679  seqcoll  11700  seqcoll2  11701  cnpart  12033  sqrlem6  12041  sqrmo  12045  resqreu  12046  resqrcl  12047  resqrthlem  12048  sqrneg  12061  sqreulem  12151  sqreu  12152  sqrthlem  12154  eqsqrd  12159  limsuple  12260  rlimcld2  12360  rlimrege0  12361  o1compt  12369  climserle  12444  caurcvgr  12455  fsum00  12565  fsumabs  12568  climcndslem2  12618  climcnds  12619  supcvg  12623  georeclim  12637  geoisumr  12643  cvgrat  12648  sin01bnd  12774  cos01bnd  12775  ruclem1  12818  ruclem9  12825  ruclem12  12828  dvdsaddr  12877  dvdssub  12878  dvdssubr  12879  dvdsfac  12892  dvdsmod  12894  oddp1even  12898  divalglem0  12901  divalglem2  12903  divalglem4  12904  divalglem5  12905  divalglem9  12909  divalg  12911  divalg2  12913  divalgmod  12914  ndvdssub  12915  ndvdsadd  12916  bitsfval  12923  bitsval  12924  bits0  12928  bitsp1  12931  bitsfzolem  12934  bitsfzo  12935  bitscmp  12938  bitsinv1lem  12941  bitsshft  12975  gcdcllem1  12999  dvdslegcd  13004  bezoutlem4  13029  dvdssqim  13041  dvdsmulgcd  13042  dvdssq  13048  nn0seqcvgd  13049  coprmdvds  13090  coprmdvds2  13091  isprm6  13097  prmdvdsexp  13102  prmdvdsexpr  13104  prmfac1  13106  divgcdodd  13107  rpmul  13111  hashdvds  13152  phiprmpw  13153  eulerthlem2  13159  prmdiv  13162  prmdiveq  13163  odzval  13165  odzcllem  13166  odzdvds  13169  opoe  13173  omoe  13174  pythagtriplem11  13187  pythagtriplem13  13189  pythagtrip  13196  pceulem  13207  pczndvds2  13228  pcdvdsb  13230  pc2dvds  13240  pcz  13242  pcprmpw2  13243  pcaddlem  13245  pcmpt  13249  prmpwdvds  13260  pockthlem  13261  prmreclem2  13273  prmreclem4  13275  4sqlem11  13311  vdwlem9  13345  rami  13371  ramlb  13375  0ram  13376  ramz2  13380  ramub1lem1  13382  imasleval  13754  subsubc  14038  pospo  14418  mulgval  14880  oddvdsnn0  15170  odmulg  15180  pgpfi1  15217  pgpfi  15227  slwispgp  15233  pgpssslw  15236  subgslw  15238  sylow2alem2  15240  sylow2blem3  15244  fislw  15247  efgi  15339  efgval2  15344  efgsrel  15354  efgredlemb  15366  lt6abl  15492  dprdval  15549  dprd2dlem2  15586  dprd2da  15588  dprd2d2  15590  ablfacrplem  15611  ablfac1a  15615  ablfac1b  15616  ablfac1eulem  15618  ablfac1eu  15619  pgpfac1lem3a  15622  ablfaclem3  15633  dvdsrtr  15745  dvdsrmul1  15746  unitpropd  15790  isabvd  15896  zndvds0  16819  znunit  16832  cygth  16840  hmphindis  17817  ordthmeolem  17821  psmettri2  18328  ismet2  18351  xmettri2  18358  imasdsf1olem  18391  imasf1oxmet  18393  comet  18531  stdbdxmet  18533  nmogelb  18738  nmolb  18739  metdsge  18867  metdseq0  18872  iihalf2  18946  bndth  18971  evth  18972  ipcau2  19179  tchcphlem1  19180  tchcphlem2  19181  iscau3  19219  iscmet3  19234  bcthlem1  19265  bcth  19270  minveclem3b  19317  minveclem3  19318  minveclem4  19321  minveclem5  19322  pjthlem1  19326  pjthlem2  19327  pmltpclem1  19333  pmltpc  19335  ivthlem2  19337  ivthlem3  19338  ovolgelb  19364  ovolunlem1  19381  ovoliunlem2  19387  ovolshftlem1  19393  ovolscalem1  19397  ovolicc1  19400  ovolicc2lem3  19403  ioombl1lem4  19443  mbfmulc2lem  19527  mbfposb  19533  mbfaddlem  19540  mbfsup  19544  mbfinf  19545  mbflimsup  19546  i1fposd  19587  itg1ge0a  19591  mbfi1fseqlem4  19598  mbfi1fseqlem6  19600  mbfi1flimlem  19602  mbfi1flim  19603  itg2const2  19621  itg2seq  19622  itg2monolem1  19630  itg2i1fseq  19635  itg2addlem  19638  ibllem  19644  isibl  19645  isibl2  19646  iblitg  19648  dfitg  19649  cbvitg  19655  itgeq2  19657  itgvallem  19664  iblneg  19682  itgneg  19683  itggt0  19721  dvlip  19865  c1lip1  19869  dvfsumle  19893  dvfsumlem2  19899  dvfsumlem4  19901  dvfsum2  19906  mdeglt  19976  degltp1le  19984  deg1suble  20018  ply1divex  20047  plypf1  20119  dgrlb  20143  coemulc  20161  dgrsub  20178  quotval  20197  plydivlem4  20201  quotcan  20214  vieta1lem2  20216  aalioulem2  20238  aaliou3lem9  20255  ulmcn  20303  dvradcnv  20325  sincosq1sgn  20394  sincosq2sgn  20395  sincosq4sgn  20397  logltb  20482  cxpge0  20562  cxple2  20576  logreclem  20648  jensen  20815  emcllem7  20828  wilthlem1  20839  ftalem2  20844  ftalem3  20845  ftalem7  20849  fta  20850  sgmval  20913  mumul  20952  dvdsppwf1o  20959  musum  20964  chtublem  20983  chtub  20984  perfect1  21000  bcmono  21049  bclbnd  21052  bposlem1  21056  bposlem5  21060  lgslem1  21068  lgsval  21072  lgsdilem  21094  lgsne0  21105  lgsqrlem2  21114  lgsqrlem4  21116  lgseisenlem1  21121  lgseisenlem2  21122  lgsquadlem1  21126  lgsquadlem2  21127  lgsquadlem3  21128  lgsquad2lem2  21131  m1lgs  21134  2sqlem4  21139  2sqlem8a  21143  2sqblem  21149  dchrisumlema  21170  dchrisumlem2  21172  dchrisumlem3  21173  chpdifbndlem2  21236  pntrsumbnd2  21249  pntpbnd1  21268  pntibndlem3  21274  pntlemi  21286  pntleme  21290  pntlem3  21291  pnt3  21294  ostth2lem2  21316  ostth3  21320  ostth  21321  eupath2lem3  21689  eupath2  21690  konigsberg  21697  nmounbseqi  22266  nmounbseqiOLD  22267  isblo3i  22290  blo3i  22291  blocnilem  22293  siilem2  22341  normlem6  22605  normgt0  22617  norm3dif  22640  norm3lemt  22642  pjhthlem1  22881  pjige0  23181  nmcexi  23517  lnconi  23524  lnopcnbd  23527  lnfncnbd  23548  riesz1  23556  cnlnadjlem2  23559  cnlnadjlem8  23565  leopg  23613  leop2  23615  leoppos  23617  leopadd  23623  leopmuli  23624  leopmul2i  23626  pjssge0i  23657  pjdifnormi  23658  pjssposi  23663  pjssdif1i  23666  chcv1  23846  cvexch  23865  atcvatlem  23876  atcvat3i  23887  atdmd  23889  cdj3i  23932  addltmulALT  23937  xrofsup  24114  xrge0addgt0  24202  isofld  24223  ofldadd  24226  ofldmul  24227  ofldchr  24232  elrhmunit  24246  unitdivcld  24287  esumlub  24440  esumfsup  24448  esumcvg  24464  dya2ub  24608  itgeq12dv  24629  prob01  24659  orvcval  24703  ballotlemfc0  24738  ballotlemfcc  24739  ballotleme  24742  ballotlem4  24744  ballotlem1c  24753  ballotlemsval  24754  ballotlemieq  24762  lgamgulmlem1  24801  lgamgulmlem2  24802  lgamgulmlem3  24803  lgamgulmlem5  24805  lgambdd  24809  lgamcvglem  24812  erdszelem8  24872  erdsze2lem2  24878  abs2sqle  25108  abs2sqlt  25109  divelunit  25173  mulge0b  25179  mulle0b  25180  possumd  25197  pdivsq  25357  dvdspw  25358  poseq  25508  soseq  25509  sltval  25556  brbtwn2  25792  axlowdim2  25847  axlowdim  25848  axcontlem2  25852  axcontlem3  25853  axcontlem4  25854  axcontlem9  25859  axcontlem10  25860  axcontlem11  25861  axcontlem12  25862  cgrdegen  25886  brofs  25887  segconeu  25893  btwntriv2  25894  transportprops  25916  brifs  25925  ifscgr  25926  brcgr3  25928  cgrxfr  25937  brcolinear2  25940  colineardim1  25943  brfs  25961  idinside  25966  btwnconn1lem11  25979  btwnconn1lem12  25980  btwnconn1lem14  25982  brsegle  25990  seglerflx  25994  seglemin  25995  segleantisym  25997  btwnsegle  25999  outsideofeu  26013  outsidele  26014  fvray  26023  ltflcei  26187  lxflflp1  26189  mblfinlem  26190  mblfinlem2  26191  mblfinlem3  26192  itg2addnclem  26202  itg2addnclem2  26203  itg2gt0cn  26206  itggt0cn  26223  dvreasin  26226  areacirclem2  26228  areacirclem5  26232  areacirclem6  26233  areacirc  26234  nn0prpwlem  26262  nn0prpw  26263  seqpo  26388  incsequz2  26390  mettrifi  26400  heibor1lem  26455  rrncmslem  26478  elpell1qr2  26872  monotuz  26941  monotoddzzfi  26942  monotoddzz  26943  oddcomabszz  26944  rmxypos  26949  mzpcong  26974  congrep  26975  acongsym  26978  acongneg2  26979  acongtr  26980  acongeq12d  26981  dvdsabsmod0  26994  divalgmodcl  26995  jm2.18  26996  jm2.19lem2  26998  jm2.19lem3  26999  jm2.19lem4  27000  jm2.19  27001  jm2.25  27007  jm2.15nn0  27011  jm2.16nn0  27012  jm2.27  27016  rmydioph  27022  expdiophlem1  27029  expdiophlem2  27030  fnwe2lem2  27063  lmisfree  27227  evth2f  27600  evthf  27612  rfcnpre3  27618  fmul01  27624  fmul01lt1lem1  27628  climinf  27646  climinff  27651  stoweidlem3  27666  stoweidlem7  27670  stoweidlem15  27678  stoweidlem16  27679  stoweidlem18  27681  stoweidlem26  27689  stoweidlem27  27690  stoweidlem28  27691  stoweidlem31  27694  stoweidlem34  27697  stoweidlem36  27699  stoweidlem37  27700  stoweidlem41  27704  stoweidlem44  27707  stoweidlem45  27708  stoweidlem46  27709  stoweidlem48  27711  stoweidlem51  27714  stoweidlem55  27718  stoweidlem59  27722  stoweidlem60  27723  stoweidlem62  27725  ubmelm1fzo  28039  2submod  28058  swrdccat3  28104  swrdccat3b  28106  shwrdidx  28130  shwrdidxmod  28131  2shwrd2lem1a  28140  2shwrd2lem2  28143  lsatcv0eq  29684  oposlem  29820  oplecon1b  29838  opltcon1b  29842  atlatmstc  29956  cvlexch1  29965  cvlexch2  29966  cvlexchb2  29968  cvlatexchb2  29972  cvlatexch2  29974  cvlatcvr2  29979  cvlsupr2  29980  ishlat1  29989  hlsuprexch  30017  cvrexch  30056  cvrat  30058  atcvr0eq  30062  atcvrj0  30064  atltcvr  30071  cvrat3  30078  cvrat4  30079  cvrat42  30080  3noncolr2  30085  hlatcon2  30088  4noncolr3  30089  3dimlem1  30094  3dimlem2  30095  3dimlem3a  30096  3dimlem3  30097  3dimlem3OLDN  30098  3dimlem4a  30099  3dimlem4  30100  3dimlem4OLDN  30101  3dim1lem5  30102  3dim2  30104  3dim3  30105  ps-1  30113  ps-2  30114  3atlem5  30123  3atlem6  30124  lplni2  30173  lplnnle2at  30177  lplnnleat  30178  lplnnlelln  30179  lplnribN  30187  lplnexllnN  30200  lvoli2  30217  lvolnle3at  30218  lvolnleat  30219  lvolnlelln  30220  lvolnlelpln  30221  4atlem9  30239  4atlem10a  30240  4atlem11a  30243  4atlem11  30245  4atlem12a  30246  dalempnes  30287  dalemqnet  30288  dalem1  30295  dalemswapyzps  30326  dalemrotps  30327  dalem30  30338  dalem35  30343  lineset  30374  islinei  30376  psubspset  30380  psubspi2N  30384  snatpsubN  30386  2llnma1  30423  elpaddn0  30436  elpaddri  30438  elpaddat  30440  elpadd2at  30442  paddcom  30449  paddasslem12  30467  pmapjat1  30489  llnexchb2  30505  lhp2at0nle  30671  lhprelat3N  30676  4atexlemswapqr  30699  4atexlemcnd  30708  lautle  30720  lautcvr  30728  ltrnel  30775  ltrneq2  30784  trlnle  30822  cdlemc3  30829  cdlemd6  30839  cdleme3  30873  cdleme7aa  30878  cdleme7  30885  cdleme11c  30897  cdleme15c  30912  cdleme20y  30938  cdleme20m  30959  cdleme21b  30962  cdleme21c  30963  cdleme21at  30964  cdleme36a  31096  cdleme43bN  31126  cdleme43dN  31128  cdleme46f2g2  31129  cdleme46f2g1  31130  cdlemeg46c  31149  cdlemeg46nlpq  31153  cdlemb3  31242  cdlemg4d  31249  cdlemg6d  31257  cdlemg10c  31275  cdlemg12  31286  cdlemg27b  31332  djhcvat42  32052
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-rab 2706  df-v 2950  df-dif 3315  df-un 3317  df-in 3319  df-ss 3326  df-nul 3621  df-if 3732  df-sn 3812  df-pr 3813  df-op 3815  df-br 4205
  Copyright terms: Public domain W3C validator