Theorem breq12d 4465

Description: Equality deduction for a binary relation. (Contributed by NM, 8-Feb-1996.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)

Hypotheses

Ref	Expression
breq1d.1
breq12d.2

Assertion

Ref	Expression
breq12d

Proof of Theorem breq12d

Step	Hyp	Ref	Expression
1		breq1d.1	. 2
2		breq12d.2	. 2
3		breq12 4457	. 2
4	1, 2, 3	syl2anc 661	1

Syntax hints:  ->wi 4  <->wb 184  =wceq 1395   class class class wbr 4452

This theorem is referenced by:  breq123d  4466  3brtr3d  4481  3brtr4d  4482  sbcbr  4505  pocl  4812  csbcnvgALT  5192  cnvpo  5550  sbcfung  5616  isoeq1  6215  isocnv  6226  isotr  6232  caovordig  6480  caovordg  6482  caovord2d  6484  caovord  6486  ofrfval  6548  ofrval  6550  ofrfval2  6557  caofref  6566  fnwelem  6915  fundmeng  7610  xpsneng  7622  xpcomeng  7629  xpdom2g  7633  map2xp  7707  mapdom3  7709  limensuc  7714  infensuc  7715  unxpdom  7747  pssnn  7758  dif1enOLD  7772  dif1en  7773  unfilem3  7806  unfi  7807  domunfican  7813  fodomfi  7819  marypha1lem  7913  wemaplem1  7992  wemaplem2  7993  wemapwe  8160  wemapweOLD  8161  dif1card  8409  infxpenlem  8412  pwsdompw  8605  infmap2  8619  sornom  8678  isfin5  8700  isfin6  8701  domtriomlem  8843  axdc2lem  8849  axdclem2  8921  pwcfsdom  8979  cfpwsdom  8980  alephom  8981  fpwwe2lem7  9035  fpwwe2lem9  9037  pwxpndom2  9064  tskcard  9180  ordpipq  9341  adderpqlem  9353  mulerpqlem  9354  mulcanenq  9359  lterpq  9369  ltanq  9370  ltmnq  9371  ltaddnq  9373  ltrnq  9378  archnq  9379  reclem4pr  9449  ltasr  9498  sqgt0sr  9504  axpre-ltadd  9565  axpre-mulgt0  9566  ltadd1  10044  leadd2  10046  ltmul2  10418  lemul2  10420  lemul1a  10421  ltdiv1  10431  ltdiv2  10455  lediv2  10460  uzindOLD  10982  xleadd1  11476  xltadd2  11478  xsubge0  11482  xlemul1a  11509  xlemul1  11511  xlemul2  11512  xltmul2  11514  ltdifltdiv  11966  fzennn  12078  monoord  12137  monoord2  12138  ltexp2r  12222  leexp1a  12224  sqlecan  12274  bernneq  12292  faclbnd  12368  faclbnd3  12370  faclbnd4lem1  12371  faclbnd4lem2  12372  faclbnd4lem3  12373  faclbnd4lem4  12374  faclbnd6  12377  facubnd  12378  rlimcld2  13401  isercoll2  13491  climsup  13492  iseraltlem2  13505  fsumabs  13615  fsumrlim  13625  climcndslem1  13661  climcndslem2  13662  supcvg  13667  geomulcvg  13685  cvgrat  13692  ntrivcvgtail  13709  ruclem2  13965  ruclem8  13970  sadcaddlem  14107  sadcadd  14108  nn0seqcvgd  14199  algcvg  14205  algcvga  14208  eucalgcvga  14215  isprm5  14253  qnumgt0  14283  pcprendvds2  14365  pcpremul  14367  pcadd2  14409  prmreclem4  14437  prmreclem5  14438  prmreclem6  14439  2expltfac  14577  xpsle  14978  mreexexlemd  15041  issubc  15204  latjlej2  15696  latmlem2  15712  sylow1lem3  16620  isslw  16628  fislw  16645  efgi  16737  lt6abl  16897  ablfac1eu  17124  isabv  17468  abvtri  17479  cayleyhamilton1  19393  isucn  20781  ispsmet  20808  psmettri2  20813  ismet  20826  isxmet  20827  xmettri2  20843  imasdsf1olem  20876  imasf1oxmet  20878  blvalps  20888  blval  20889  comet  21016  stdbdxmet  21018  nrmmetd  21095  tngngp  21168  nmofval  21221  nmolb2d  21225  nmoi  21235  nmoix  21236  icopnfhmeo  21443  xrhmeo  21446  evth2  21460  pi1grplem  21549  minveclem6  21849  ovolfiniun  21912  ovoliunlem3  21915  voliunlem3  21962  ioombl1  21972  mbfmax  22056  mbfpos  22058  itg1climres  22121  mbfi1fseqlem2  22123  mbfi1fseqlem6  22127  mbfi1fseq  22128  mbfmullem  22132  itg2split  22156  itg2monolem1  22157  itg2monolem3  22159  itg2mono  22160  itg2i1fseqle  22161  itg2i1fseq  22162  itg2i1fseq2  22163  itg2addlem  22165  rolle  22391  dvlip  22394  c1lip1  22398  dvcnvrelem1  22418  dvcvx  22421  ply1divex  22537  q1pval  22554  fta1glem2  22567  fta1g  22568  fta1b  22570  plydivlem3  22691  fta1lem  22703  fta1  22704  aalioulem3  22730  aalioulem4  22731  aaliou3lem2  22739  aaliou3lem8  22741  aaliou3lem9  22746  ulmdvlem1  22795  ulmdvlem3  22797  abelthlem2  22827  abelthlem7a  22832  argrege0  22996  cxplt  23075  cxplea  23077  cxple2  23078  cxplt3  23081  rlimcxp  23303  scvxcvx  23315  jensenlem2  23317  ftalem3  23348  ftalem7  23352  vmalelog  23480  chtub  23487  chpchtsum  23494  bclbnd  23555  efexple  23556  bposlem5  23563  bposlem6  23564  bposlem7  23565  lgsdilem  23597  dchrisumlem3  23676  dchrmusumlema  23678  dchrmusum2  23679  dchrvmasumlem2  23683  dchrvmasumlema  23685  dchrvmasumiflem1  23686  dchrisum0flblem2  23694  dchrisum0flb  23695  dchrisum0lema  23699  dchrisum0lem1b  23700  dchrisum0lem2  23703  pntrlog2bndlem2  23763  pntibndlem2  23776  pntlemf  23790  ostth2lem1  23803  qabvle  23810  legso  23985  iscgra  24169  brbtwn2  24208  axlowdim  24264  sizeusglecusg  24486  isrusgra  24927  extwwlkfablem2  25078  isnvlem  25503  nvtri  25573  nmlnoubi  25711  nmblolbii  25714  nmblolbi  25715  blocnilem  25719  sii  25769  ubthlem2  25787  minvecolem3  25792  minvecolem5  25797  minvecolem6  25798  norm-ii  26055  norm3dif  26067  norm3adifi  26070  bcs  26098  pjnorm  26642  pjnel  26644  nmbdoplbi  26943  nmbdoplb  26944  nmcoplb  26949  lnconi  26952  nmbdfnlb  26969  nmcfnlb  26973  pjdifnormi  27086  mdslmd2i  27249  cvmd  27255  cvexch  27293  cdj1i  27352  cdj3lem1  27353  cdj3lem2b  27356  cdj3lem3b  27359  cdj3i  27360  isoun  27520  isomnd  27691  omndadd  27696  omndmul  27704  ogrpinvlt  27714  isinftm  27725  gsumle  27770  xrmulc1cn  27912  lmdvg  27935  nexple  28005  logblt  28022  faeval  28218  brfae  28220  sconpht  28674  snmlval  28776  lediv2aALT  29043  faclim  29171  poseq  29333  sltval2  29416  sltres  29424  nodense  29449  nobndup  29460  nobnddown  29461  fvtransport  29682  idinside  29734  btwnconn1lem7  29743  btwnconn1lem11  29747  btwnconn1lem12  29748  heicant  30049  itg2addnclem  30066  itg2addnclem3  30068  itg2gt0cn  30070  ftc1anclem6  30095  ftc1anc  30098  ftc2nc  30099  dvasin  30103  areacirclem1  30107  nn0prpwlem  30140  seqpo  30240  incsequz  30241  metf1o  30248  mettrifi  30250  cntotbnd  30292  heiborlem4  30310  heiborlem6  30312  heiborlem10  30316  bfplem1  30318  bfplem2  30319  irrapxlem2  30759  irrapxlem4  30761  irrapxlem5  30762  irrapxlem6  30763  pellexlem3  30767  monotuz  30877  monotoddzzfi  30878  monotoddzz  30879  expmordi  30883  jm2.17a  30898  jm2.17b  30899  rmygeid  30902  rmydioph  30956  expdiophlem1  30963  expdiophlem2  30964  ttac  30978  fnwe2lem2  30997  cvgdvgrat  31194  monoords  31496  evthiccabs  31529  fprodle  31604  climinf  31612  climinff  31617  ioodvbdlimc1lem1  31728  ioodvbdlimc1lem2  31729  ioodvbdlimc2lem  31731  iblspltprt  31772  itgspltprt  31778  stoweidlem3  31785  fourierdlem2  31891  fourierdlem3  31892  fourierdlem11  31900  fourierdlem12  31901  fourierdlem15  31904  fourierdlem34  31923  fourierdlem41  31930  fourierdlem48  31937  fourierdlem49  31938  fourierdlem79  31968  fourierdlem83  31972  fourierdlem89  31978  fourierdlem91  31980  fourierdlem100  31989  fourierdlem107  31996  fourierdlem109  31998  fourierdlem112  32001  etransclem31  32048  etransclem32  32049  2elfz2melfz  32334  ismgmALT  32547  iscmgmALT  32548  issgrpALT  32549  iscsgrpALT  32550  lindslinindsimp2lem5  33063  aacllem  33216  isopos  34905  oplecon3b  34925  atlatle  35045  4at2  35338  pmaple  35485  islaut  35807  lautcnvle  35813  lautco  35821  ltrncnvel  35866  cdlemeg49lebilem  36265  cdlemg17h  36394  tendoset  36485  tendotp  36487  cdlemk39s  36665

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-rab 2816  df-v 3111  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-br 4453