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

Theorem breq12d 4590
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 4582 . 2 ((𝐴 = 𝐵𝐶 = 𝐷) → (𝐴𝑅𝐶𝐵𝑅𝐷))
41, 2, 3syl2anc 690 1 (𝜑 → (𝐴𝑅𝐶𝐵𝑅𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194   = wceq 1474   class class class wbr 4577
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-rab 2904  df-v 3174  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-nul 3874  df-if 4036  df-sn 4125  df-pr 4127  df-op 4131  df-br 4578
This theorem is referenced by:  breq123d  4591  3brtr3d  4608  3brtr4d  4609  sbcbr  4631  pocl  4955  csbcnvgALT  5216  cnvpo  5575  sbcfung  5812  isoeq1  6444  isocnv  6457  isotr  6463  caovordig  6714  caovordg  6716  caovord2d  6718  caovord  6720  ofrfval  6780  ofrval  6782  ofrfval2  6790  caofref  6798  fnwelem  7156  fundmeng  7894  xpsneng  7907  xpcomeng  7914  xpdom2g  7918  map2xp  7992  mapdom3  7994  limensuc  7999  infensuc  8000  unxpdom  8029  pssnn  8040  dif1en  8055  unfilem3  8088  unfi  8089  domunfican  8095  fodomfi  8101  marypha1lem  8199  wemaplem1  8311  wemaplem2  8312  wemapwe  8454  dif1card  8693  infxpenlem  8696  pwsdompw  8886  infmap2  8900  sornom  8959  isfin5  8981  isfin6  8982  domtriomlem  9124  axdc2lem  9130  axdclem2  9202  pwcfsdom  9261  cfpwsdom  9262  alephom  9263  fpwwe2lem7  9314  fpwwe2lem9  9316  pwxpndom2  9343  tskcard  9459  ordpipq  9620  adderpqlem  9632  mulerpqlem  9633  mulcanenq  9638  lterpq  9648  ltanq  9649  ltmnq  9650  ltaddnq  9652  ltrnq  9657  archnq  9658  reclem4pr  9728  ltasr  9777  sqgt0sr  9783  axpre-ltadd  9844  axpre-mulgt0  9845  ltadd1  10346  leadd2  10348  ltmul2  10725  lemul2  10727  lemul1a  10728  ltdiv1  10738  ltdiv2  10760  lediv2  10764  div4p1lem1div2  11136  nn0ledivnn  11775  xleadd1  11916  xltadd2  11918  xsubge0  11922  xlemul1a  11949  xlemul1  11951  xlemul2  11952  xltmul2  11954  ltdifltdiv  12454  fzennn  12586  monoord  12650  monoord2  12651  ltexp2r  12736  leexp1a  12738  sqlecan  12790  bernneq  12809  faclbnd  12896  faclbnd3  12898  faclbnd4lem1  12899  faclbnd4lem2  12900  faclbnd4lem3  12901  faclbnd4lem4  12902  faclbnd6  12905  facubnd  12906  rlimcld2  14105  isercoll2  14195  climsup  14196  iseraltlem2  14209  fsumabs  14322  fsumrlim  14332  climcndslem1  14368  climcndslem2  14369  supcvg  14375  geomulcvg  14394  cvgrat  14402  ntrivcvgtail  14419  fprodle  14514  ruclem2  14748  ruclem8  14753  addmodlteqALT  14833  fproddvdsd  14845  sadcaddlem  14965  sadcadd  14966  nn0seqcvgd  15069  algcvg  15075  algcvga  15078  eucalgcvga  15085  isprm5  15205  qnumgt0  15244  pcprendvds2  15332  pcpremul  15334  pcadd2  15380  prmreclem4  15409  prmreclem5  15410  prmreclem6  15411  2expltfac  15585  xpsle  16012  mreexexlemd  16075  issubc  16266  latjlej2  16837  latmlem2  16853  sylow1lem3  17786  isslw  17794  fislw  17811  efgi  17903  lt6abl  18067  ablfac1eu  18243  isabv  18590  abvtri  18601  cayleyhamilton1  20463  isucn  21839  ispsmet  21866  psmettri2  21871  ismet  21885  isxmet  21886  xmettri2  21902  imasdsf1olem  21935  imasf1oxmet  21937  blvalps  21947  blval  21948  comet  22075  stdbdxmet  22077  nrmmetd  22136  tngngp  22215  tngngp3  22217  nmofval  22275  nmolb2d  22279  nmoi  22289  nmoix  22290  icopnfhmeo  22497  xrhmeo  22500  evth2  22514  pi1grplem  22604  minveclem6  22957  ovolfiniun  23020  ovoliunlem3  23023  voliunlem3  23071  ioombl1  23081  mbfmax  23166  mbfpos  23168  itg1climres  23231  mbfi1fseqlem2  23233  mbfi1fseqlem6  23237  mbfi1fseq  23238  mbfmullem  23242  itg2split  23266  itg2monolem1  23267  itg2monolem3  23269  itg2mono  23270  itg2i1fseqle  23271  itg2i1fseq  23272  itg2i1fseq2  23273  itg2addlem  23275  rolle  23501  dvlip  23504  c1lip1  23508  dvcnvrelem1  23528  dvcvx  23531  ply1divex  23644  q1pval  23661  fta1glem2  23674  fta1g  23675  fta1b  23677  plydivlem3  23798  fta1lem  23810  fta1  23811  aalioulem3  23837  aalioulem4  23838  aaliou3lem2  23846  aaliou3lem8  23848  aaliou3lem9  23853  ulmdvlem1  23902  ulmdvlem3  23904  abelthlem2  23934  abelthlem7a  23939  argrege0  24105  cxplt  24184  cxplea  24186  cxple2  24187  cxplt3  24190  logbleb  24265  logblt  24266  rlimcxp  24444  scvxcvx  24456  jensenlem2  24458  ftalem3  24545  ftalem7  24549  vmalelog  24674  chtub  24681  chpchtsum  24688  bclbnd  24749  efexple  24750  bposlem5  24757  bposlem6  24758  bposlem7  24759  lgsdilem  24793  2lgslem1a2  24859  dchrisumlem3  24924  dchrmusumlema  24926  dchrmusum2  24927  dchrvmasumlem2  24931  dchrvmasumlema  24933  dchrvmasumiflem1  24934  dchrisum0flblem2  24942  dchrisum0flb  24943  dchrisum0lema  24947  dchrisum0lem1b  24948  dchrisum0lem2  24951  pntrlog2bndlem2  25011  pntibndlem2  25024  pntlemf  25038  ostth2lem1  25051  qabvle  25058  legso  25239  iscgra  25446  isleag  25478  iseqlg  25492  brbtwn2  25530  axlowdim  25586  sizeusglecusg  25807  isrusgra  26247  extwwlkfablem2  26398  isnvlem  26642  nvtri  26702  nmlnoubi  26828  nmblolbii  26831  nmblolbi  26832  blocnilem  26836  sii  26886  ubthlem2  26904  minvecolem3  26909  minvecolem5  26914  minvecolem6  26915  norm-ii  27172  norm3dif  27184  norm3adifi  27187  bcs  27215  pjnorm  27760  pjnel  27762  nmbdoplbi  28060  nmbdoplb  28061  nmcoplb  28066  lnconi  28069  nmbdfnlb  28086  nmcfnlb  28090  pjdifnormi  28203  mdslmd2i  28366  cvmd  28372  cvexch  28410  cdj1i  28469  cdj3lem1  28470  cdj3lem2b  28473  cdj3lem3b  28476  cdj3i  28477  isoun  28655  isomnd  28825  omndadd  28830  omndmul  28838  ogrpinvlt  28848  isinftm  28859  gsumle  28903  xrmulc1cn  29097  lmdvg  29120  nexple  29192  faeval  29429  brfae  29431  inelcarsg  29493  carsgsigalem  29497  carsgclctunlem2  29501  carsgclctun  29503  sconpht  30258  snmlval  30360  lediv2aALT  30618  faclim  30678  poseq  30787  sltval2  30846  sltres  30854  nodense  30881  nobndup  30892  nobnddown  30893  fvtransport  31102  idinside  31154  btwnconn1lem7  31163  btwnconn1lem11  31167  btwnconn1lem12  31168  nn0prpwlem  31280  poimirlem29  32391  heicant  32397  itg2addnclem  32414  itg2addnclem3  32416  itg2gt0cn  32418  ftc1anclem6  32443  ftc1anc  32446  ftc2nc  32447  dvasin  32449  areacirclem1  32453  seqpo  32496  incsequz  32497  metf1o  32504  mettrifi  32506  cntotbnd  32548  heiborlem4  32566  heiborlem6  32568  heiborlem10  32572  bfplem1  32574  bfplem2  32575  isopos  33268  oplecon3b  33288  atlatle  33408  4at2  33701  pmaple  33848  islaut  34170  lautcnvle  34176  lautco  34184  ltrncnvel  34229  cdlemeg49lebilem  34628  cdlemg17h  34757  tendoset  34848  tendotp  34850  cdlemk39s  35028  irrapxlem2  36188  irrapxlem4  36190  irrapxlem5  36191  irrapxlem6  36192  pellexlem3  36196  monotuz  36307  monotoddzzfi  36308  monotoddzz  36309  expmordi  36313  jm2.17a  36328  jm2.17b  36329  rmygeid  36332  rmydioph  36382  expdiophlem1  36389  expdiophlem2  36390  ttac  36404  fnwe2lem2  36422  relexp01min  36807  cvgdvgrat  37317  monoords  38235  supxrgelem  38277  supxrge  38278  abslt2sqd  38300  ltmulneg  38339  ltdiv23neg  38341  evthiccabs  38348  sqrlearg  38410  climinf  38456  climinff  38461  fprodsubrecnncnvlem  38577  fprodaddrecnncnvlem  38579  ioodvbdlimc1lem1  38604  ioodvbdlimc1lem2  38605  ioodvbdlimc2lem  38607  iblspltprt  38648  itgspltprt  38654  stoweidlem3  38679  fourierdlem2  38785  fourierdlem3  38786  fourierdlem11  38794  fourierdlem12  38795  fourierdlem15  38798  fourierdlem34  38817  fourierdlem41  38824  fourierdlem48  38830  fourierdlem49  38831  fourierdlem79  38861  fourierdlem83  38865  fourierdlem89  38871  fourierdlem91  38873  fourierdlem100  38882  fourierdlem107  38889  fourierdlem109  38891  fourierdlem112  38894  etransclem31  38941  etransclem32  38942  rrndistlt  38969  ioorrnopn  38984  ioorrnopnxrlem  38985  sge0less  39068  sge0le  39083  sge0split  39085  sge0lempt  39086  sge0iunmptlemre  39091  sge0isum  39103  sge0seq  39122  meaiuninclem  39156  meaiininclem  39159  meaiininc  39160  isome  39167  omeunile  39178  omeiunlempt  39193  carageniuncllem2  39195  0ome  39202  isomenndlem  39203  isomennd  39204  ovnsslelem  39233  ovnssle  39234  ovnsubadd  39245  hsphoidmvle2  39258  hsphoidmvle  39259  hoidmvval0  39260  hoidmv1lelem1  39264  hoidmv1lelem2  39265  hoidmv1lelem3  39266  hoidmv1le  39267  hoidmvlelem1  39268  hoidmvlelem2  39269  hoidmvlelem3  39270  hoidmvlelem4  39271  hoidmvlelem5  39272  hoidmvle  39273  hoidifhspdmvle  39293  hspmbllem2  39300  hspmbl  39302  ovnsubadd2lem  39318  ovolval4lem2  39323  ovolval4  39324  ovolval5lem2  39326  vonioolem2  39355  vonioo  39356  vonicclem2  39358  vonicc  39359  smfid  39422  smflimlem3  39442  smonoord  39728  iccpart  39738  iccpartimp  39739  iccpartres  39740  sqrtpwpw2p  39772  2elfz2melfz  40161  ewlksfval  40784  ismgmALT  41630  iscmgmALT  41631  issgrpALT  41632  iscsgrpALT  41633  lindslinindsimp2lem5  42026  aacllem  42298
  Copyright terms: Public domain W3C validator