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

Theorem breq12d 5046
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
StepHypRef Expression
1 breq1d.1 . 2 (𝜑𝐴 = 𝐵)
2 breq12d.2 . 2 (𝜑𝐶 = 𝐷)
3 breq12 5038 . 2 ((𝐴 = 𝐵𝐶 = 𝐷) → (𝐴𝑅𝐶𝐵𝑅𝐷))
41, 2, 3syl2anc 587 1 (𝜑 → (𝐴𝑅𝐶𝐵𝑅𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209   = wceq 1538   class class class wbr 5033
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-ext 2773
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-ex 1782  df-sb 2070  df-clab 2780  df-cleq 2794  df-clel 2873  df-v 3446  df-un 3889  df-sn 4529  df-pr 4531  df-op 4535  df-br 5034
This theorem is referenced by:  breq123d  5047  3brtr3d  5064  3brtr4d  5065  sbcbr  5088  pocl  5449  csbcnvgALT  5723  cnvpo  6110  sbcfung  6352  isoeq1  7053  isocnv  7066  isotr  7072  caovordig  7337  caovordg  7339  caovord2d  7341  caovord  7343  ofrfval  7401  ofrval  7403  ofrfval2  7411  caofref  7419  fnwelem  7812  fundmeng  8571  xpsneng  8589  xpcomeng  8596  xpdom2g  8600  limensuc  8682  infensuc  8683  unxpdom  8713  pssnn  8724  dif1en  8739  unfilem3  8772  unfi  8773  domunfican  8779  fodomfi  8785  marypha1lem  8885  infsupprpr  8956  wemaplem1  8998  wemaplem2  8999  wemapwe  9148  dif1card  9425  infxpenlem  9428  nnadju  9612  pwsdompw  9619  infmap2  9633  sornom  9692  isfin5  9714  isfin6  9715  domtriomlem  9857  axdc2lem  9863  axdclem2  9935  pwcfsdom  9998  cfpwsdom  9999  alephom  10000  fpwwe2lem7  10051  fpwwe2lem9  10053  tskcard  10196  ordpipq  10357  adderpqlem  10369  mulerpqlem  10370  mulcanenq  10375  lterpq  10385  ltanq  10386  ltmnq  10387  ltaddnq  10389  ltrnq  10394  archnq  10395  reclem4pr  10465  ltasr  10515  sqgt0sr  10521  axpre-ltadd  10582  axpre-mulgt0  10583  ltadd1  11100  leadd2  11102  ltmul2  11484  lemul2  11486  lemul1a  11487  ltdiv1  11497  ltdiv2  11519  lediv2  11523  div4p1lem1div2  11884  nn0ledivnn  12494  xleadd1  12640  xltadd2  12642  xsubge0  12646  xlemul1a  12673  xlemul1  12675  xlemul2  12676  xltmul2  12678  ltdifltdiv  13203  fzennn  13335  monoord  13400  monoord2  13401  expmordi  13531  ltexp2r  13537  leexp1a  13539  sqlecan  13571  bernneq  13590  faclbnd  13650  faclbnd3  13652  faclbnd4lem1  13653  faclbnd4lem2  13654  faclbnd4lem3  13655  faclbnd4lem4  13656  faclbnd6  13659  facubnd  13660  rlimcld2  14931  isercoll2  15021  climsup  15022  iseraltlem2  15035  fsumabs  15152  fsumrlim  15162  climcndslem1  15200  climcndslem2  15201  supcvg  15207  geomulcvg  15228  cvgrat  15235  ntrivcvgtail  15252  ruclem2  15581  ruclem8  15586  addmodlteqALT  15671  fproddvdsd  15680  sadcaddlem  15800  sadcadd  15801  nn0seqcvgd  15908  algcvg  15914  algcvga  15917  eucalgcvga  15924  isprm5  16045  qnumgt0  16084  pcprendvds2  16172  pcpremul  16174  pcadd2  16220  prmreclem4  16249  prmreclem5  16250  prmreclem6  16251  2expltfac  16422  xpsle  16848  mreexexlemd  16911  issubc  17101  latjlej2  17672  latmlem2  17688  sylow1lem3  18721  isslw  18729  fislw  18746  efgi  18841  lt6abl  19012  ablfac1eu  19192  isabv  19587  abvtri  19598  cayleyhamilton1  21501  isucn  22888  ispsmet  22915  psmettri2  22920  ismet  22934  isxmet  22935  xmettri2  22951  imasdsf1olem  22984  imasf1oxmet  22986  blvalps  22996  blval  22997  comet  23124  stdbdxmet  23126  nrmmetd  23185  tngngp  23264  tngngp3  23266  nmofval  23324  nmolb2d  23328  nmoi  23338  nmoix  23339  icopnfhmeo  23552  xrhmeo  23555  evth2  23569  pi1grplem  23658  minveclem6  24042  ovolfiniun  24109  ovoliunlem3  24112  voliunlem3  24160  ioombl1  24170  mbfmax  24257  mbfpos  24259  itg1climres  24322  mbfi1fseqlem2  24324  mbfi1fseqlem6  24328  mbfi1fseq  24329  mbfmullem  24333  itg2split  24357  itg2monolem1  24358  itg2monolem3  24360  itg2mono  24361  itg2i1fseqle  24362  itg2i1fseq  24363  itg2i1fseq2  24364  itg2addlem  24366  rolle  24597  dvlip  24600  c1lip1  24604  dvcnvrelem1  24624  dvcvx  24627  ply1divex  24741  q1pval  24758  fta1glem2  24771  fta1g  24772  fta1b  24774  plydivlem3  24895  fta1lem  24907  fta1  24908  aalioulem3  24934  aalioulem4  24935  aaliou3lem2  24943  aaliou3lem8  24945  aaliou3lem9  24950  ulmdvlem1  24999  ulmdvlem3  25001  abelthlem2  25031  abelthlem7a  25036  argrege0  25206  cxplt  25289  cxplea  25291  cxple2  25292  cxplt3  25295  logbleb  25373  logblt  25374  rlimcxp  25563  scvxcvx  25575  jensenlem2  25577  ftalem3  25664  ftalem7  25668  vmalelog  25793  chtub  25800  chpchtsum  25807  bclbnd  25868  efexple  25869  bposlem5  25876  bposlem6  25877  bposlem7  25878  lgsdilem  25912  2lgslem1a2  25978  2sqreuop  26050  2sqreuopnn  26051  2sqreuoplt  26052  2sqreuopltb  26053  2sqreuopnnlt  26054  2sqreuopnnltb  26055  dchrisumlem3  26079  dchrmusumlema  26081  dchrmusum2  26082  dchrvmasumlem2  26086  dchrvmasumlema  26088  dchrvmasumiflem1  26089  dchrisum0flblem2  26097  dchrisum0flb  26098  dchrisum0lema  26102  dchrisum0lem1b  26103  dchrisum0lem2  26106  pntrlog2bndlem2  26166  pntibndlem2  26179  pntlemf  26193  ostth2lem1  26206  qabvle  26213  legso  26397  iscgra  26607  isleag  26645  iseqlg  26665  brbtwn2  26703  axlowdim  26759  ewlksfval  27395  isnvlem  28397  nvtri  28457  nmlnoubi  28583  nmblolbii  28586  nmblolbi  28587  blocnilem  28591  sii  28641  ubthlem2  28658  minvecolem3  28663  minvecolem5  28668  minvecolem6  28669  norm-ii  28925  norm3dif  28937  norm3adifi  28940  bcs  28968  pjnorm  29511  pjnel  29513  nmbdoplbi  29811  nmbdoplb  29812  nmcoplb  29817  lnconi  29820  nmbdfnlb  29837  nmcfnlb  29841  pjdifnormi  29954  mdslmd2i  30117  cvmd  30123  cvexch  30161  cdj1i  30220  cdj3lem1  30221  cdj3lem2b  30224  cdj3lem3b  30227  cdj3i  30228  isoun  30465  ismnt  30695  mgcmntco  30706  dfmgc2lem  30707  dfmgc2  30708  isomnd  30756  omndadd  30761  omndmul  30769  ogrpinvlt  30778  gsumle  30779  isinftm  30864  xrmulc1cn  31287  lmdvg  31310  nexple  31382  faeval  31619  brfae  31621  inelcarsg  31683  carsgsigalem  31687  carsgclctunlem2  31691  carsgclctun  31693  hgt750lemc  32032  hgt750lemd  32033  hgt749d  32034  sconnpht  32590  snmlval  32692  satfv1lem  32723  satfv1  32724  satfv0fun  32732  satfv0fvfmla0  32774  lediv2aALT  33034  faclim  33092  poseq  33209  sltval2  33277  sltres  33283  nolesgn2o  33292  nodense  33310  nolt02o  33313  noresle  33314  nosupbnd2lem1  33329  nosupbnd2  33330  fvtransport  33607  idinside  33659  btwnconn1lem7  33668  btwnconn1lem11  33672  btwnconn1lem12  33673  nn0prpwlem  33784  bj-opabco  34604  poimirlem29  35085  heicant  35091  itg2addnclem  35107  itg2addnclem3  35109  itg2gt0cn  35111  ftc1anclem6  35134  ftc1anc  35137  ftc2nc  35138  dvasin  35140  areacirclem1  35144  seqpo  35184  incsequz  35185  metf1o  35192  mettrifi  35194  cntotbnd  35233  heiborlem4  35251  heiborlem6  35253  heiborlem10  35257  bfplem1  35259  bfplem2  35260  isopos  36475  oplecon3b  36495  atlatle  36615  4at2  36909  pmaple  37056  islaut  37378  lautcnvle  37384  lautco  37392  ltrncnvel  37437  cdlemeg49lebilem  37834  cdlemg17h  37963  tendoset  38054  tendotp  38056  cdlemk39s  38234  lcmineqlem23  39338  lcmineqlem  39339  2ap1caineq  39346  factwoffsmonot  39385  reltsub1  39521  irrapxlem2  39761  irrapxlem4  39763  irrapxlem5  39764  irrapxlem6  39765  pellexlem3  39769  monotuz  39879  monotoddzzfi  39880  monotoddzz  39881  jm2.17a  39898  jm2.17b  39899  rmygeid  39902  rmydioph  39952  expdiophlem1  39959  expdiophlem2  39960  ttac  39974  fnwe2lem2  39992  relexp01min  40411  cvgdvgrat  41014  monoords  41926  supxrgelem  41966  supxrge  41967  abslt2sqd  41989  ltmulneg  42025  ltdiv23neg  42027  monoordxrv  42118  monoordxr  42119  monoord2xrv  42120  monoord2xr  42121  evthiccabs  42130  sqrlearg  42187  climinf  42245  climinff  42250  limsupres  42344  climinf2  42346  climinf2mpt  42353  climinfmpt  42354  supcnvlimsup  42379  liminfval2  42407  liminflelimsuplem  42414  liminfltlem  42443  fprodsubrecnncnvlem  42546  fprodaddrecnncnvlem  42548  ioodvbdlimc1lem1  42570  ioodvbdlimc1lem2  42571  ioodvbdlimc2lem  42573  iblspltprt  42612  itgspltprt  42618  stoweidlem3  42642  fourierdlem2  42748  fourierdlem3  42749  fourierdlem11  42757  fourierdlem12  42758  fourierdlem15  42761  fourierdlem34  42780  fourierdlem41  42787  fourierdlem48  42793  fourierdlem49  42794  fourierdlem79  42824  fourierdlem83  42828  fourierdlem89  42834  fourierdlem91  42836  fourierdlem100  42845  fourierdlem107  42852  fourierdlem109  42854  fourierdlem112  42857  etransclem31  42904  etransclem32  42905  rrndistlt  42929  ioorrnopn  42944  ioorrnopnxrlem  42945  sge0less  43028  sge0le  43043  sge0split  43045  sge0lempt  43046  sge0iunmptlemre  43051  sge0isum  43063  sge0seq  43082  meaiuninclem  43116  meaiininclem  43122  meaiininc  43123  isome  43130  omeunile  43141  omeiunlempt  43156  carageniuncllem2  43158  0ome  43165  isomenndlem  43166  isomennd  43167  ovnsslelem  43196  ovnssle  43197  ovnsubadd  43208  hsphoidmvle2  43221  hsphoidmvle  43222  hoidmvval0  43223  hoidmv1lelem1  43227  hoidmv1lelem2  43228  hoidmv1lelem3  43229  hoidmv1le  43230  hoidmvlelem1  43231  hoidmvlelem2  43232  hoidmvlelem3  43233  hoidmvlelem4  43234  hoidmvlelem5  43235  hoidmvle  43236  hoidifhspdmvle  43256  hspmbllem2  43263  hspmbl  43265  ovnsubadd2lem  43281  ovolval4lem2  43286  ovolval4  43287  ovolval5lem2  43289  vonioolem2  43317  vonioo  43318  vonicclem2  43320  vonicc  43321  smfid  43383  smflimlem3  43403  2elfz2melfz  43872  smonoord  43885  iccpart  43930  iccpartimp  43931  iccpartres  43932  sqrtpwpw2p  44052  ismgmALT  44480  iscmgmALT  44481  issgrpALT  44482  iscsgrpALT  44483  lindslinindsimp2lem5  44868  rrx2plordisom  45134  aacllem  45326
  Copyright terms: Public domain W3C validator