MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  breq2d Structured version   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  5730  isorel  6038  soisores  6039  soisoi  6040  isocnv  6042  isotr  6048  f1owe  6065  f1oweALT  6066  caovordig  6244  caovordg  6246  caovord  6250  frxp  6448  xporderlem  6449  fnwelem  6453  th3qlem2  7003  difsnen  7182  domdifsn  7183  unfilem3  7365  domunfican  7371  marypha1lem  7430  marypha1  7431  r1sdom  7692  sdomsdomcardi  7850  alephordi  7947  pwcdadom  8088  sornom  8149  axdclem  8391  pwcfsdom  8450  elgch  8489  winalim2  8563  rankcf  8644  inatsk  8645  pinq  8796  nqereu  8798  ltaddnq  8843  ltrnq  8848  archnq  8849  addclprlem1  8885  mulclprlem  8888  1idpr  8898  ltaprlem  8913  ltapr  8914  prlem936  8916  ltasr  8967  mulgt0sr  8972  sqgt0sr  8973  map2psrpr  8977  axpre-ltadd  9034  axpre-mulgt0  9035  axpre-sup  9036  ltsubadd2  9491  lesubadd2  9493  ltaddpos2  9511  posdif  9513  lesub1  9514  ltnegcon1  9521  lenegcon1  9524  addge02  9531  mulge0  9537  msqge0  9541  ltordlem  9544  prodgt0  9847  prodgt02  9848  prodge02  9850  ltmulgt12  9863  lemulge12  9865  ltdivmul  9874  ledivmul  9875  ledivmulOLD  9876  ltdivmul2  9877  lt2mul2div  9878  ledivmul2  9879  ledivmul2OLD  9880  ltrec  9883  ltrec1  9889  ltdiv23  9893  lediv23  9894  nnge1  10018  halfpos  10190  lt2halves  10194  addltmul  10195  avglt2  10198  avgle2  10200  nnrecl  10211  zltlem1  10320  gtndiv  10339  rebtwnz  10565  xrmax1  10755  max1ALT  10766  qbtwnre  10777  xralrple  10783  xltnegi  10794  xmulval  10803  xsubge0  10832  xposdif  10833  xlesubadd  10834  fllelt  11198  flbi  11215  btwnzge0  11222  om2uzlti  11282  monoord  11345  sermono  11347  expval  11376  expnbnd  11500  discr1  11507  discr  11508  facwordi  11572  hashtpg  11683  seqcoll  11704  seqcoll2  11705  cnpart  12037  sqrlem6  12045  sqrmo  12049  resqreu  12050  resqrcl  12051  resqrthlem  12052  sqrneg  12065  sqreulem  12155  sqreu  12156  sqrthlem  12158  eqsqrd  12163  limsuple  12264  rlimcld2  12364  rlimrege0  12365  o1compt  12373  climserle  12448  caurcvgr  12459  fsum00  12569  fsumabs  12572  climcndslem2  12622  climcnds  12623  supcvg  12627  georeclim  12641  geoisumr  12647  cvgrat  12652  sin01bnd  12778  cos01bnd  12779  ruclem1  12822  ruclem9  12829  ruclem12  12832  dvdsaddr  12881  dvdssub  12882  dvdssubr  12883  dvdsfac  12896  dvdsmod  12898  oddp1even  12902  divalglem0  12905  divalglem2  12907  divalglem4  12908  divalglem5  12909  divalglem9  12913  divalg  12915  divalg2  12917  divalgmod  12918  ndvdssub  12919  ndvdsadd  12920  bitsfval  12927  bitsval  12928  bits0  12932  bitsp1  12935  bitsfzolem  12938  bitsfzo  12939  bitscmp  12942  bitsinv1lem  12945  bitsshft  12979  gcdcllem1  13003  dvdslegcd  13008  bezoutlem4  13033  dvdssqim  13045  dvdsmulgcd  13046  dvdssq  13052  nn0seqcvgd  13053  coprmdvds  13094  coprmdvds2  13095  isprm6  13101  prmdvdsexp  13106  prmdvdsexpr  13108  prmfac1  13110  divgcdodd  13111  rpmul  13115  hashdvds  13156  phiprmpw  13157  eulerthlem2  13163  prmdiv  13166  prmdiveq  13167  odzval  13169  odzcllem  13170  odzdvds  13173  opoe  13177  omoe  13178  pythagtriplem11  13191  pythagtriplem13  13193  pythagtrip  13200  pceulem  13211  pczndvds2  13232  pcdvdsb  13234  pc2dvds  13244  pcz  13246  pcprmpw2  13247  pcaddlem  13249  pcmpt  13253  prmpwdvds  13264  pockthlem  13265  prmreclem2  13277  prmreclem4  13279  4sqlem11  13315  vdwlem9  13349  rami  13375  ramlb  13379  0ram  13380  ramz2  13384  ramub1lem1  13386  imasleval  13758  subsubc  14042  pospo  14422  mulgval  14884  oddvdsnn0  15174  odmulg  15184  pgpfi1  15221  pgpfi  15231  slwispgp  15237  pgpssslw  15240  subgslw  15242  sylow2alem2  15244  sylow2blem3  15248  fislw  15251  efgi  15343  efgval2  15348  efgsrel  15358  efgredlemb  15370  lt6abl  15496  dprdval  15553  dprd2dlem2  15590  dprd2da  15592  dprd2d2  15594  ablfacrplem  15615  ablfac1a  15619  ablfac1b  15620  ablfac1eulem  15622  ablfac1eu  15623  pgpfac1lem3a  15626  ablfaclem3  15637  dvdsrtr  15749  dvdsrmul1  15750  unitpropd  15794  isabvd  15900  zndvds0  16823  znunit  16836  cygth  16844  hmphindis  17821  ordthmeolem  17825  psmettri2  18332  ismet2  18355  xmettri2  18362  imasdsf1olem  18395  imasf1oxmet  18397  comet  18535  stdbdxmet  18537  nmogelb  18742  nmolb  18743  metdsge  18871  metdseq0  18876  iihalf2  18950  bndth  18975  evth  18976  ipcau2  19183  tchcphlem1  19184  tchcphlem2  19185  iscau3  19223  iscmet3  19238  bcthlem1  19269  bcth  19274  minveclem3b  19321  minveclem3  19322  minveclem4  19325  minveclem5  19326  pjthlem1  19330  pjthlem2  19331  pmltpclem1  19337  pmltpc  19339  ivthlem2  19341  ivthlem3  19342  ovolgelb  19368  ovolunlem1  19385  ovoliunlem2  19391  ovolshftlem1  19397  ovolscalem1  19401  ovolicc1  19404  ovolicc2lem3  19407  ioombl1lem4  19447  mbfmulc2lem  19531  mbfposb  19537  mbfaddlem  19544  mbfsup  19548  mbfinf  19549  mbflimsup  19550  i1fposd  19591  itg1ge0a  19595  mbfi1fseqlem4  19602  mbfi1fseqlem6  19604  mbfi1flimlem  19606  mbfi1flim  19607  itg2const2  19625  itg2seq  19626  itg2monolem1  19634  itg2i1fseq  19639  itg2addlem  19642  ibllem  19648  isibl  19649  isibl2  19650  iblitg  19652  dfitg  19653  cbvitg  19659  itgeq2  19661  itgvallem  19668  iblneg  19686  itgneg  19687  itggt0  19725  dvlip  19869  c1lip1  19873  dvfsumle  19897  dvfsumlem2  19903  dvfsumlem4  19905  dvfsum2  19910  mdeglt  19980  degltp1le  19988  deg1suble  20022  ply1divex  20051  plypf1  20123  dgrlb  20147  coemulc  20165  dgrsub  20182  quotval  20201  plydivlem4  20205  quotcan  20218  vieta1lem2  20220  aalioulem2  20242  aaliou3lem9  20259  ulmcn  20307  dvradcnv  20329  sincosq1sgn  20398  sincosq2sgn  20399  sincosq4sgn  20401  logltb  20486  cxpge0  20566  cxple2  20580  logreclem  20652  jensen  20819  emcllem7  20832  wilthlem1  20843  ftalem2  20848  ftalem3  20849  ftalem7  20853  fta  20854  sgmval  20917  mumul  20956  dvdsppwf1o  20963  musum  20968  chtublem  20987  chtub  20988  perfect1  21004  bcmono  21053  bclbnd  21056  bposlem1  21060  bposlem5  21064  lgslem1  21072  lgsval  21076  lgsdilem  21098  lgsne0  21109  lgsqrlem2  21118  lgsqrlem4  21120  lgseisenlem1  21125  lgseisenlem2  21126  lgsquadlem1  21130  lgsquadlem2  21131  lgsquadlem3  21132  lgsquad2lem2  21135  m1lgs  21138  2sqlem4  21143  2sqlem8a  21147  2sqblem  21153  dchrisumlema  21174  dchrisumlem2  21176  dchrisumlem3  21177  chpdifbndlem2  21240  pntrsumbnd2  21253  pntpbnd1  21272  pntibndlem3  21278  pntlemi  21290  pntleme  21294  pntlem3  21295  pnt3  21298  ostth2lem2  21320  ostth3  21324  ostth  21325  eupath2lem3  21693  eupath2  21694  konigsberg  21701  nmounbseqi  22270  nmounbseqiOLD  22271  isblo3i  22294  blo3i  22295  blocnilem  22297  siilem2  22345  normlem6  22609  normgt0  22621  norm3dif  22644  norm3lemt  22646  pjhthlem1  22885  pjige0  23185  nmcexi  23521  lnconi  23528  lnopcnbd  23531  lnfncnbd  23552  riesz1  23560  cnlnadjlem2  23563  cnlnadjlem8  23569  leopg  23617  leop2  23619  leoppos  23621  leopadd  23627  leopmuli  23628  leopmul2i  23630  pjssge0i  23661  pjdifnormi  23662  pjssposi  23667  pjssdif1i  23670  chcv1  23850  cvexch  23869  atcvatlem  23880  atcvat3i  23891  atdmd  23893  cdj3i  23936  addltmulALT  23941  xrofsup  24118  xrge0addgt0  24206  isofld  24227  ofldadd  24230  ofldmul  24231  ofldchr  24236  elrhmunit  24250  unitdivcld  24291  esumlub  24444  esumfsup  24452  esumcvg  24468  dya2ub  24612  itgeq12dv  24633  prob01  24663  orvcval  24707  ballotlemfc0  24742  ballotlemfcc  24743  ballotleme  24746  ballotlem4  24748  ballotlem1c  24757  ballotlemsval  24758  ballotlemieq  24766  lgamgulmlem1  24805  lgamgulmlem2  24806  lgamgulmlem3  24807  lgamgulmlem5  24809  lgambdd  24813  lgamcvglem  24816  erdszelem8  24876  erdsze2lem2  24882  abs2sqle  25112  abs2sqlt  25113  divelunit  25177  mulge0b  25183  mulle0b  25184  possumd  25201  pdivsq  25360  dvdspw  25361  poseq  25520  soseq  25521  sltval  25594  brbtwn2  25836  axlowdim2  25891  axlowdim  25892  axcontlem2  25896  axcontlem3  25897  axcontlem4  25898  axcontlem9  25903  axcontlem10  25904  axcontlem11  25905  axcontlem12  25906  cgrdegen  25930  brofs  25931  segconeu  25937  btwntriv2  25938  transportprops  25960  brifs  25969  ifscgr  25970  brcgr3  25972  cgrxfr  25981  brcolinear2  25984  colineardim1  25987  brfs  26005  idinside  26010  btwnconn1lem11  26023  btwnconn1lem12  26024  btwnconn1lem14  26026  brsegle  26034  seglerflx  26038  seglemin  26039  segleantisym  26041  btwnsegle  26043  outsideofeu  26057  outsidele  26058  fvray  26067  ltflcei  26231  lxflflp1  26233  mblfinlem  26234  mblfinlem2  26235  mblfinlem3  26236  itg2addnclem  26246  itg2addnclem2  26247  itg2gt0cn  26250  itggt0cn  26267  dvreasin  26270  areacirclem2  26272  areacirclem5  26276  areacirclem6  26277  areacirc  26278  nn0prpwlem  26306  nn0prpw  26307  seqpo  26432  incsequz2  26434  mettrifi  26444  heibor1lem  26499  rrncmslem  26522  elpell1qr2  26916  monotuz  26985  monotoddzzfi  26986  monotoddzz  26987  oddcomabszz  26988  rmxypos  26993  mzpcong  27018  congrep  27019  acongsym  27022  acongneg2  27023  acongtr  27024  acongeq12d  27025  dvdsabsmod0  27038  divalgmodcl  27039  jm2.18  27040  jm2.19lem2  27042  jm2.19lem3  27043  jm2.19lem4  27044  jm2.19  27045  jm2.25  27051  jm2.15nn0  27055  jm2.16nn0  27056  jm2.27  27060  rmydioph  27066  expdiophlem1  27073  expdiophlem2  27074  fnwe2lem2  27107  lmisfree  27270  evth2f  27643  evthf  27655  rfcnpre3  27661  fmul01  27667  fmul01lt1lem1  27671  climinf  27689  climinff  27694  stoweidlem3  27709  stoweidlem7  27713  stoweidlem15  27721  stoweidlem16  27722  stoweidlem18  27724  stoweidlem26  27732  stoweidlem27  27733  stoweidlem28  27734  stoweidlem31  27737  stoweidlem34  27740  stoweidlem36  27742  stoweidlem37  27743  stoweidlem41  27747  stoweidlem44  27750  stoweidlem45  27751  stoweidlem46  27752  stoweidlem48  27754  stoweidlem51  27757  stoweidlem55  27761  stoweidlem59  27765  stoweidlem60  27766  stoweidlem62  27768  leaddle0  28068  ubmelm1fzo  28100  subsubelfzo0  28108  2submod  28120  swrdccat3blem  28174  2cshw2lem2  28209  2cshwmod  28213  lsatcv0eq  29772  oposlem  29908  oplecon1b  29926  opltcon1b  29930  atlatmstc  30044  cvlexch1  30053  cvlexch2  30054  cvlexchb2  30056  cvlatexchb2  30060  cvlatexch2  30062  cvlatcvr2  30067  cvlsupr2  30068  ishlat1  30077  hlsuprexch  30105  cvrexch  30144  cvrat  30146  atcvr0eq  30150  atcvrj0  30152  atltcvr  30159  cvrat3  30166  cvrat4  30167  cvrat42  30168  3noncolr2  30173  hlatcon2  30176  4noncolr3  30177  3dimlem1  30182  3dimlem2  30183  3dimlem3a  30184  3dimlem3  30185  3dimlem3OLDN  30186  3dimlem4a  30187  3dimlem4  30188  3dimlem4OLDN  30189  3dim1lem5  30190  3dim2  30192  3dim3  30193  ps-1  30201  ps-2  30202  3atlem5  30211  3atlem6  30212  lplni2  30261  lplnnle2at  30265  lplnnleat  30266  lplnnlelln  30267  lplnribN  30275  lplnexllnN  30288  lvoli2  30305  lvolnle3at  30306  lvolnleat  30307  lvolnlelln  30308  lvolnlelpln  30309  4atlem9  30327  4atlem10a  30328  4atlem11a  30331  4atlem11  30333  4atlem12a  30334  dalempnes  30375  dalemqnet  30376  dalem1  30383  dalemswapyzps  30414  dalemrotps  30415  dalem30  30426  dalem35  30431  lineset  30462  islinei  30464  psubspset  30468  psubspi2N  30472  snatpsubN  30474  2llnma1  30511  elpaddn0  30524  elpaddri  30526  elpaddat  30528  elpadd2at  30530  paddcom  30537  paddasslem12  30555  pmapjat1  30577  llnexchb2  30593  lhp2at0nle  30759  lhprelat3N  30764  4atexlemswapqr  30787  4atexlemcnd  30796  lautle  30808  lautcvr  30816  ltrnel  30863  ltrneq2  30872  trlnle  30910  cdlemc3  30917  cdlemd6  30927  cdleme3  30961  cdleme7aa  30966  cdleme7  30973  cdleme11c  30985  cdleme15c  31000  cdleme20y  31026  cdleme20m  31047  cdleme21b  31050  cdleme21c  31051  cdleme21at  31052  cdleme36a  31184  cdleme43bN  31214  cdleme43dN  31216  cdleme46f2g2  31217  cdleme46f2g1  31218  cdlemeg46c  31237  cdlemeg46nlpq  31241  cdlemb3  31330  cdlemg4d  31337  cdlemg6d  31345  cdlemg10c  31363  cdlemg12  31374  cdlemg27b  31420  djhcvat42  32140
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