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

Theorem breq2d 4430
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 4422 . 2  |-  ( A  =  B  ->  ( C R A  <->  C R B ) )
31, 2syl 17 1  |-  ( ph  ->  ( C R A  <-> 
C R B ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189    = wceq 1455   class class class wbr 4418
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-rab 2758  df-v 3059  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-nul 3744  df-if 3894  df-sn 3981  df-pr 3983  df-op 3987  df-br 4419
This theorem is referenced by:  breqtrd  4443  sbcbr1g  4473  pofun  4793  csbfv12  5927  isorel  6247  soisores  6248  soisoi  6249  isocnv  6251  isotr  6257  f1owe  6274  caovordig  6506  caovordg  6508  caovord  6512  f1oweALT  6809  frxp  6938  xporderlem  6939  fnwelem  6943  difsnen  7685  domdifsn  7686  unfilem3  7868  domunfican  7875  marypha1lem  7978  marypha1  7979  inflb  8036  wemapwe  8233  oef1o  8234  r1sdom  8276  sdomsdomcardi  8436  alephordi  8536  pwcdadom  8677  sornom  8738  axdclem  8980  pwcfsdom  9039  elgch  9078  winalim2  9152  rankcf  9233  inatsk  9234  pinq  9383  nqereu  9385  ltaddnq  9430  ltrnq  9435  archnq  9436  addclprlem1  9472  mulclprlem  9475  1idpr  9485  ltaprlem  9500  ltapr  9501  prlem936  9503  ltasr  9555  mulgt0sr  9560  sqgt0sr  9561  map2psrpr  9565  axpre-ltadd  9622  axpre-mulgt0  9623  axpre-sup  9624  ltsubadd2  10118  lesubadd2  10120  ltaddpos2  10138  posdif  10140  lesub1  10141  ltnegcon1  10148  lenegcon1  10151  addge02  10158  leaddle0  10162  mulge0  10165  msqge0  10168  ltordlem  10172  sublt0d  10271  prodgt0  10483  prodgt02  10484  prodge02  10486  ltmulgt12  10499  lemulge12  10501  mulge0b  10508  mulle0b  10509  ltdivmul  10513  ledivmul  10514  ltdivmul2  10515  lt2mul2div  10516  ledivmul2  10517  ledivmul2OLD  10518  ltrec  10521  ltrec1  10526  ltdiv23  10530  lediv23  10531  nnge1  10668  halfpos  10877  lt2halves  10881  addltmul  10882  avglt2  10885  avgle2  10887  nnrecl  10901  zltlem1  11023  gtndiv  11047  nn01to3  11291  rebtwnz  11297  xrmax1  11504  max1ALT  11515  qbtwnre  11526  xralrple  11532  xltnegi  11543  xmulval  11552  xsubge0  11581  xposdif  11582  xlesubadd  11583  divelunit  11809  eluzgtdifelfzo  12013  fllelt  12071  flflp1  12081  flbi  12089  btwnzge0  12099  dfceil2  12106  ceilval2  12107  2submod  12189  om2uzlti  12202  monoord  12281  sermono  12283  expval  12312  expnbnd  12439  discr1  12446  discr  12447  facwordi  12512  seqcoll  12666  seqcoll2  12667  hashtpg  12680  swrdccat3blem  12894  cnpart  13358  sqrlem6  13366  sqrmo  13370  resqreu  13371  resqrtcl  13372  resqrtthlem  13373  sqrtneg  13386  sqreulem  13477  sqreu  13478  sqrtthlem  13480  eqsqrtd  13485  limsuple  13591  limsupleOLD  13592  rlimcld2  13697  rlimrege0  13698  o1compt  13706  climserle  13781  caurcvgr  13793  caurcvgrOLD  13794  fsum00  13913  fsumabs  13916  climcndslem2  13963  climcnds  13964  supcvg  13969  georeclim  13983  geoisumr  13989  cvgrat  13994  sin01bnd  14294  cos01bnd  14295  ruclem1  14338  ruclem9  14345  ruclem12  14348  dvdsaddr  14399  dvdssub  14400  dvdssubr  14401  dvdsfac  14415  dvdsmod  14417  oddp1even  14422  fproddvdsd  14425  divalglem0  14426  divalglem2  14428  divalglem2OLD  14429  divalglem4  14430  divalglem5OLD  14431  divalglem5  14432  divalglem9  14436  divalglem9OLD  14437  divalg  14439  divalg2  14441  divalgmod  14442  ndvdssub  14443  ndvdsadd  14444  bitsfval  14451  bitsval  14452  bits0  14456  bitsp1  14459  bitsfzolem  14462  bitsfzolemOLD  14463  bitsfzo  14464  bitscmp  14467  bitsinv1lem  14470  bitsshft  14504  gcdcllem1  14528  dvdslegcd  14533  bezoutlem4OLD  14561  bezoutlem4  14564  dvdssqim  14576  dvdsmulgcd  14577  dvdssq  14583  nn0seqcvgd  14584  lcmfunsnlem2lem2  14667  divgcdodd  14708  coprmdvds  14714  coprmdvds2  14715  isprm6  14721  prmdvdsexp  14722  prmdvdsexpr  14724  prmfac1  14726  rpmul  14730  hashdvds  14778  phiprmpw  14779  eulerthlem2  14785  prmdiv  14788  prmdiveq  14789  odzval  14791  odzcllem  14792  odzdvds  14795  odzvalOLD  14797  odzcllemOLD  14798  odzdvdsOLD  14801  opoe  14816  omoe  14817  pythagtriplem11  14830  pythagtriplem13  14832  pythagtrip  14839  pceulem  14850  pczndvds2  14871  pcdvdsb  14873  pc2dvds  14883  pcz  14885  pcprmpw2  14886  pcaddlem  14888  pcmpt  14892  prmpwdvds  14903  pockthlem  14904  prmreclem2  14916  prmreclem4  14918  4sqlem11  14954  vdwlem9  14994  rami  15027  ramlb  15032  0ram  15033  ramz2  15037  ramub1lem1  15039  prmdvdsprmo  15055  prmgaplcmlem1OLD  15067  prmdvdsprmorOLD  15070  prmgaplem7  15082  prmgaplem8  15083  imasleval  15502  subsubc  15813  pospo  16274  mulgval  16815  oddvdsnn0  17248  odmulg  17262  pgpfi1  17302  pgpfi  17312  slwispgp  17318  pgpssslw  17321  subgslw  17323  sylow2alem2  17325  sylow2blem3  17329  fislw  17332  efgi  17424  efgval2  17429  efgsrel  17439  efgredlemb  17451  lt6abl  17584  telgsums  17678  dprdval  17690  dprd2dlem2  17728  dprd2da  17730  dprd2d2  17732  ablfacrplem  17753  ablfac1a  17757  ablfac1b  17758  ablfac1eulem  17760  ablfac1eu  17761  pgpfac1lem3a  17764  ablfaclem3  17775  dvdsrtr  17935  dvdsrmul1  17936  unitpropd  17980  isabvd  18103  mplval  18707  ressmplbas2  18734  mplbaspropd  18885  zndvds0  19176  znunit  19189  cygth  19197  frlmup1  19411  lmisfree  19455  pmatcoe1fsupp  19780  fvmptnn04if  19928  hmphindis  20867  ordthmeolem  20871  psmettri2  21380  ismet2  21403  xmettri2  21410  imasdsf1olem  21443  imasf1oxmet  21445  comet  21583  stdbdxmet  21585  nmogelb  21776  nmolb  21777  nmogelbOLD  21795  nmolbOLD  21796  metdsge  21921  metdseq0  21926  metdsgeOLD  21936  metdseq0OLD  21941  iihalf2  22016  bndth  22041  evth  22042  ipcau2  22263  tchcphlem1  22264  tchcphlem2  22265  iscau3  22303  iscmet3  22318  bcthlem1  22347  bcth  22352  minveclem3b  22425  minveclem3  22426  minveclem4  22429  minveclem5  22430  minveclem3bOLD  22437  minveclem3OLD  22438  minveclem4OLD  22441  minveclem5OLD  22442  pjthlem1  22446  pjthlem2  22447  pmltpclem1  22454  pmltpc  22456  ivthlem2  22458  ivthlem3  22459  ovolgelb  22488  ovolunlem1  22505  ovoliunlem2  22511  ovolshftlem1  22517  ovolscalem1  22521  ovolicc1  22524  ovolicc2lem3  22527  ioombl1lem4  22570  mbfmulc2lem  22659  mbfposb  22665  mbfaddlem  22672  mbfsup  22676  mbfinf  22677  mbfinfOLD  22678  mbflimsup  22679  mbflimsupOLD  22680  i1fposd  22721  itg1ge0a  22725  mbfi1fseqlem4  22732  mbfi1fseqlem6  22734  mbfi1flimlem  22736  mbfi1flim  22737  itg2const2  22755  itg2seq  22756  itg2monolem1  22764  itg2i1fseq  22769  itg2addlem  22772  ibllem  22778  isibl  22779  isibl2  22780  iblitg  22782  dfitg  22783  cbvitg  22789  itgeq2  22791  itgvallem  22798  iblneg  22816  itgneg  22817  itggt0  22855  dvlip  23001  c1lip1  23005  dvfsumle  23029  dvfsumlem2  23035  dvfsumlem4  23037  dvfsum2  23042  mdeglt  23070  degltp1le  23078  deg1suble  23112  ply1divex  23143  plypf1  23222  dgrlb  23246  coemulc  23265  dgrsub  23282  quotval  23301  plydivlem4  23305  quotcan  23318  vieta1lem2  23320  aalioulem2  23345  aaliou3lem9  23362  ulmcn  23410  dvradcnv  23432  sincosq1sgn  23509  sincosq2sgn  23510  sincosq4sgn  23512  logltb  23605  cxpge0  23684  cxple2  23698  logreclem  23755  jensen  23970  emcllem7  23983  lgamgulmlem1  24010  lgamgulmlem2  24011  lgamgulmlem3  24012  lgamgulmlem5  24014  lgambdd  24018  lgamcvglem  24021  wilthlem1  24049  ftalem2  24054  ftalem3  24055  ftalem7  24061  fta  24062  sgmval  24125  mumul  24164  dvdsppwf1o  24171  musum  24176  chtublem  24195  chtub  24196  perfect1  24212  bcmono  24261  bclbnd  24264  bposlem1  24268  bposlem5  24272  lgslem1  24280  lgsval  24284  lgsdilem  24306  lgsne0  24317  lgsqrlem2  24326  lgsqrlem4  24328  lgseisenlem1  24333  lgseisenlem2  24334  lgsquadlem1  24338  lgsquadlem2  24339  lgsquadlem3  24340  lgsquad2lem2  24343  m1lgs  24346  2sqlem4  24351  2sqlem8a  24355  2sqblem  24361  dchrisumlema  24382  dchrisumlem2  24384  dchrisumlem3  24385  chpdifbndlem2  24448  pntrsumbnd2  24461  pntpbnd1  24480  pntibndlem3  24486  pntlemi  24498  pntleme  24502  pntlem3  24503  pnt3  24506  ostth2lem2  24528  ostth3  24532  ostth  24533  tgcgrxfr  24619  hlpasch  24854  islmib  24885  lmicom  24886  trgcopyeu  24904  iscgra  24907  iscgra1  24908  iscgrad  24909  isleag  24939  iseqlg  24953  brbtwn2  24991  axlowdim2  25046  axlowdim  25047  axcontlem2  25051  axcontlem3  25052  axcontlem4  25053  axcontlem9  25058  axcontlem10  25059  axcontlem11  25060  axcontlem12  25061  ebtwntg  25068  ausisusgraedg  25139  clwlkisclwwlklem2a4  25568  clwlkisclwwlklem2a  25569  nbhashuvtx1  25699  eupath2lem3  25763  eupath2  25764  konigsberg  25771  frgrareggt1  25900  ex-ind-dvds  25955  nmounbseqi  26474  nmounbseqiALT  26475  isblo3i  26498  blo3i  26499  blocnilem  26501  siilem2  26549  normlem6  26824  normgt0  26836  norm3dif  26859  norm3lemt  26861  pjhthlem1  27100  pjige0  27400  nmcexi  27735  lnconi  27742  lnopcnbd  27745  lnfncnbd  27766  riesz1  27774  cnlnadjlem2  27777  cnlnadjlem8  27783  leopg  27831  leop2  27833  leoppos  27835  leopadd  27841  leopmuli  27842  leopmul2i  27844  pjssge0i  27875  pjdifnormi  27876  pjssposi  27881  pjssdif1i  27884  chcv1  28064  cvexch  28083  atcvatlem  28094  atcvat3i  28105  atdmd  28107  cdj3i  28150  addltmulALT  28155  xrofsup  28405  xrge0addgt0  28505  omndadd  28520  omndmul2  28526  ogrpinvlt  28538  isinftm  28549  isarchi3  28555  archirng  28556  archirngz  28557  archiexdiv  28558  isorng  28613  orngmul  28617  ofldchr  28628  isarchiofld  28631  elrhmunit  28634  rearchi  28656  fzto1st  28667  unitdivcld  28758  esumlub  28932  esumfsup  28942  esumcvg  28958  esum2d  28965  dya2ub  29142  omssubadd  29178  omssubaddOLD  29182  carsgmon  29196  itgeq12dv  29209  oddpwdc  29237  eulerpartlems  29243  prob01  29296  orvcval  29340  ballotlemfc0  29375  ballotlemfcc  29376  ballotleme  29379  ballotlem4  29381  ballotlemimin  29388  ballotlem1c  29390  ballotlemsval  29391  ballotlemieq  29399  ballotlemfrcn0  29412  ballotlem1cOLD  29428  ballotlemsvalOLD  29429  ballotlemieqOLD  29437  sgnmulsgp  29471  signsply0  29490  signslema  29501  signsvfpn  29524  erdszelem8  29971  erdsze2lem2  29977  abs2sqle  30374  abs2sqlt  30375  possumd  30416  pdivsq  30435  dvdspw  30436  poseq  30541  soseq  30542  sltval  30584  cgrdegen  30821  brofs  30822  segconeu  30828  btwntriv2  30829  transportprops  30851  brifs  30860  ifscgr  30861  brcgr3  30863  cgrxfr  30872  brcolinear2  30875  colineardim1  30878  brfs  30896  idinside  30901  btwnconn1lem11  30914  btwnconn1lem12  30915  btwnconn1lem14  30917  brsegle  30925  seglerflx  30929  seglemin  30930  segleantisym  30932  btwnsegle  30934  outsideofeu  30948  outsidele  30949  fvray  30958  nn0prpwlem  31028  nn0prpw  31029  ltflcei  31979  cos2h  31982  tan2h  31983  poimirlem5  31991  poimirlem6  31992  poimirlem7  31993  poimirlem8  31994  poimirlem10  31996  poimirlem11  31997  poimirlem12  31998  poimirlem15  32001  poimirlem16  32002  poimirlem17  32003  poimirlem18  32004  poimirlem19  32005  poimirlem20  32006  poimirlem21  32007  poimirlem22  32008  poimirlem25  32011  poimirlem27  32013  poimirlem28  32014  poimirlem29  32015  poimirlem30  32016  poimirlem31  32017  poimirlem32  32018  poimir  32019  heicant  32021  mblfinlem2  32024  mblfinlem3  32025  mblfinlem4  32026  dvtanlemOLD  32037  itg2addnclem  32039  itg2addnclem2  32040  itg2gt0cn  32043  itggt0cn  32060  ftc1anclem5  32067  dvasin  32074  areacirclem1  32078  areacirclem4  32081  areacirclem5  32082  areacirc  32083  seqpo  32122  incsequz2  32124  mettrifi  32132  heibor1lem  32187  rrncmslem  32210  lsatcv0eq  32659  oposlem  32794  oplecon1b  32813  opltcon1b  32817  atlatmstc  32931  cvlexch1  32940  cvlexch2  32941  cvlexchb2  32943  cvlatexchb2  32947  cvlatexch2  32949  cvlatcvr2  32954  cvlsupr2  32955  ishlat1  32964  hlsuprexch  32992  cvrexch  33031  cvrat  33033  atcvr0eq  33037  atcvrj0  33039  atltcvr  33046  cvrat3  33053  cvrat4  33054  cvrat42  33055  3noncolr2  33060  hlatcon2  33063  4noncolr3  33064  3dimlem1  33069  3dimlem2  33070  3dimlem3a  33071  3dimlem3  33072  3dimlem3OLDN  33073  3dimlem4a  33074  3dimlem4  33075  3dimlem4OLDN  33076  3dim1lem5  33077  3dim2  33079  3dim3  33080  ps-1  33088  ps-2  33089  3atlem5  33098  3atlem6  33099  lplni2  33148  lplnnle2at  33152  lplnnleat  33153  lplnnlelln  33154  lplnribN  33162  lplnexllnN  33175  lvoli2  33192  lvolnle3at  33193  lvolnleat  33194  lvolnlelln  33195  lvolnlelpln  33196  4atlem9  33214  4atlem10a  33215  4atlem11a  33218  4atlem11  33220  4atlem12a  33221  dalempnes  33262  dalemqnet  33263  dalem1  33270  dalemswapyzps  33301  dalemrotps  33302  dalem30  33313  dalem35  33318  lineset  33349  islinei  33351  psubspset  33355  psubspi2N  33359  snatpsubN  33361  2llnma1  33398  elpaddn0  33411  elpaddri  33413  elpaddat  33415  elpadd2at  33417  paddcom  33424  paddasslem12  33442  pmapjat1  33464  llnexchb2  33480  lhp2at0nle  33646  lhprelat3N  33651  4atexlemswapqr  33674  4atexlemcnd  33683  lautle  33695  lautcvr  33703  ltrnel  33750  ltrneq2  33759  trlnle  33798  cdlemc3  33805  cdlemd6  33815  cdleme3  33849  cdleme7aa  33854  cdleme7  33861  cdleme11c  33873  cdleme15c  33888  cdleme20yOLD  33915  cdleme20m  33936  cdleme21b  33939  cdleme21c  33940  cdleme21at  33941  cdleme36a  34073  cdleme43bN  34103  cdleme43dN  34105  cdleme46f2g2  34106  cdleme46f2g1  34107  cdlemeg46c  34126  cdlemeg46nlpq  34130  cdlemb3  34219  cdlemg4d  34226  cdlemg6d  34234  cdlemg10c  34252  cdlemg12  34263  cdlemg27b  34309  djhcvat42  35029  elpell1qr2  35764  monotuz  35835  monotoddzzfi  35836  monotoddzz  35837  oddcomabszz  35838  rmxypos  35843  mzpcong  35868  congrep  35869  acongsym  35872  acongneg2  35873  acongtr  35874  acongeq12d  35875  dvdsabsmod0OLD  35887  divalgmodcl  35888  jm2.18  35889  jm2.19lem2  35891  jm2.19lem3  35892  jm2.19lem4  35893  jm2.19  35894  jm2.25  35900  jm2.15nn0  35904  jm2.16nn0  35905  jm2.27  35909  rmydioph  35915  expdiophlem1  35922  expdiophlem2  35923  fnwe2lem2  35955  relexpmulg  36348  relexpxpmin  36355  frege124d  36399  frege72  36577  frege91  36596  inductionexd  36639  leeq2d  36642  imo72b2lem0  36654  imo72b2lem2  36656  imo72b2lem1  36660  imo72b2  36664  dvgrat  36706  hashnzfz  36714  evth2f  37377  evthf  37389  rfcnpre3  37395  brneqtrd  37463  ltaddneg  37583  upbdrech2  37601  supxrgelem  37635  supxrge  37636  xrlexaddrp  37650  xralrple2  37652  ltdivgt1  37654  infleinf  37671  fsumlessf  37741  fmul01  37744  fmul01lt1lem1  37748  climinf  37770  climinfOLD  37771  climinff  37776  climinffOLD  37777  limcrecl  37795  limsupre  37807  limsupreOLD  37808  limclner  37818  cncficcgt0  37852  stoweidlem3  37964  stoweidlem7  37968  stoweidlem15  37976  stoweidlem16  37977  stoweidlem18  37979  stoweidlem26  37987  stoweidlem27  37988  stoweidlem28  37989  stoweidlem31  37993  stoweidlem34  37996  stoweidlem36  37998  stoweidlem37  37999  stoweidlem41  38003  stoweidlem44  38006  stoweidlem45  38007  stoweidlem46  38008  stoweidlem48  38010  stoweidlem51  38013  stoweidlem55  38017  stoweidlem59  38021  stoweidlem60  38022  stoweidlem62  38024  stoweidlem62OLD  38025  fourierdlem42  38113  fourierdlem42OLD  38114  fourierdlem50  38121  fourierdlem54  38125  fourierdlem68  38139  fourierdlem79  38150  fourierdlem96  38167  fourierdlem97  38168  fourierdlem98  38169  fourierdlem99  38170  fourierdlem105  38176  fourierdlem108  38179  fourierdlem110  38181  fourierdlem111  38182  etransclem24  38224  etransclem25  38225  etransclem35  38235  etransclem37  38237  etransclem41  38241  etransclem44  38244  sge0gerp  38340  sge0pnffigt  38341  sge0gerpmpt  38347  omessle  38427  ovncvrrp  38493  ovnsubaddlem1  38499  ovnsubadd  38501  hoidmv1lelem2  38521  hoidmvlelem3  38526  hoidmvle  38529  ovncvr2  38540  hoidifhspval2  38544  hoidifhspval3  38548  hspmbllem2  38556  hspmbl  38558  smonoord  38853  iccpartiltu  38871  iccpartlt  38873  iccpartgtl  38875  iccpartgt  38876  iccpartgel  38878  iccpartrn  38879  iccpartiun  38883  icceuelpartlem  38884  iccpartdisj  38886  iccpartnel  38887  bits0ALTV  38943  sgoldbaltlem1  39015  bgoldbtbndlem2  39036  bgoldbtbndlem3  39037  bgoldbtbnd  39039  ltsubsubaddltsub  39186  subsubelfzo0  39200  ewlksfval  39764  isewlk  39765  ewlkinedg  39767  umgrislfupgrlem  39814  lfgrwlkprop  39818  nn0le2is012  40517  lcoop  40573  islininds  40608  ldepsnlinc  40670  ltsubaddb  40680  ltsubsubb  40681  ltsubadd2b  40682  logle1b  40713  loglt1b  40714  bigoval  40729  elbigo2r  40733  logbge0b  40743  logblt1b  40744  fldivexpfllog2  40745  nnlog2ge0lt1  40746  fllog2  40748  nnpw2pmod  40763  dignn0ldlem  40782  dig2nn1st  40785
  Copyright terms: Public domain W3C validator