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

Theorem breq12d 5119
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 5111 . 2 ((𝐴 = 𝐵𝐶 = 𝐷) → (𝐴𝑅𝐶𝐵𝑅𝐷))
41, 2, 3syl2anc 585 1 (𝜑 → (𝐴𝑅𝐶𝐵𝑅𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205   = wceq 1542   class class class wbr 5106
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-rab 3409  df-v 3448  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-sn 4588  df-pr 4590  df-op 4594  df-br 5107
This theorem is referenced by:  breq123d  5120  3brtr3d  5137  3brtr4d  5138  sbcbr  5161  pocl  5553  poclOLD  5554  csbcnvgALT  5841  cnvpo  6240  sbcfung  6526  isoeq1  7263  isocnv  7276  isotr  7282  caovordig  7560  caovordg  7562  caovord2d  7564  caovord  7566  ofrfvalg  7626  ofrval  7630  ofrfval2  7639  caofref  7647  fnwelem  8064  poseq  8091  fundmeng  8977  enrefnn  8992  xpsneng  9001  xpcomeng  9009  xpdom2g  9013  limensuc  9099  infensuc  9100  pssnn  9113  unxpdom  9198  pssnnOLD  9210  dif1ennnALT  9222  unfilem3  9257  unfiOLD  9258  domunfican  9265  fodomfi  9270  marypha1lem  9370  infsupprpr  9441  wemaplem1  9483  wemaplem2  9484  wemapwe  9634  ssttrcl  9652  ttrcltr  9653  ttrclss  9657  dmttrcl  9658  rnttrcl  9659  ttrclselem2  9663  dif1card  9947  infxpenlem  9950  nnadju  10134  pwsdompw  10141  infmap2  10155  sornom  10214  isfin5  10236  isfin6  10237  domtriomlem  10379  axdc2lem  10385  axdclem2  10457  pwcfsdom  10520  cfpwsdom  10521  alephom  10522  fpwwe2lem6  10573  fpwwe2lem8  10575  tskcard  10718  ordpipq  10879  adderpqlem  10891  mulerpqlem  10892  mulcanenq  10897  lterpq  10907  ltanq  10908  ltmnq  10909  ltaddnq  10911  ltrnq  10916  archnq  10917  reclem4pr  10987  ltasr  11037  sqgt0sr  11043  axpre-ltadd  11104  axpre-mulgt0  11105  ltadd1  11623  leadd2  11625  ltmul2  12007  lemul2  12009  lemul1a  12010  ltdiv1  12020  ltdiv2  12042  lediv2  12046  div4p1lem1div2  12409  nn0ledivnn  13029  xleadd1  13175  xltadd2  13177  xsubge0  13181  xlemul1a  13208  xlemul1  13210  xlemul2  13211  xltmul2  13213  ltdifltdiv  13740  fzennn  13874  monoord  13939  monoord2  13940  expmordi  14073  ltexp2r  14079  leexp1a  14081  sqlecan  14114  bernneq  14133  faclbnd  14191  faclbnd3  14193  faclbnd4lem1  14194  faclbnd4lem2  14195  faclbnd4lem3  14196  faclbnd4lem4  14197  faclbnd6  14200  facubnd  14201  rlimcld2  15461  isercoll2  15554  climsup  15555  iseraltlem2  15568  fsumabs  15687  fsumrlim  15697  climcndslem1  15735  climcndslem2  15736  supcvg  15742  geomulcvg  15762  cvgrat  15769  ntrivcvgtail  15786  ruclem2  16115  ruclem8  16120  addmodlteqALT  16208  fproddvdsd  16218  sadcaddlem  16338  sadcadd  16339  nn0seqcvgd  16447  algcvg  16453  algcvga  16456  eucalgcvga  16463  isprm5  16584  qnumgt0  16626  pcprendvds2  16714  pcpremul  16716  pcadd2  16763  prmreclem4  16792  prmreclem5  16793  prmreclem6  16794  2expltfac  16966  xpsle  17462  mreexexlemd  17525  issubc  17722  latjlej2  18344  latmlem2  18360  sylow1lem3  19383  isslw  19391  fislw  19408  efgi  19502  lt6abl  19673  ablfac1eu  19853  isabv  20281  abvtri  20292  cayleyhamilton1  22244  isucn  23633  ispsmet  23660  psmettri2  23665  ismet  23679  isxmet  23680  xmettri2  23696  imasdsf1olem  23729  imasf1oxmet  23731  blvalps  23741  blval  23742  comet  23872  stdbdxmet  23874  nrmmetd  23933  tngngp  24021  tngngp3  24023  nmofval  24081  nmolb2d  24085  nmoi  24095  nmoix  24096  icopnfhmeo  24309  xrhmeo  24312  evth2  24326  pi1grplem  24415  minveclem6  24801  ovolfiniun  24868  ovoliunlem3  24871  voliunlem3  24919  ioombl1  24929  mbfmax  25016  mbfpos  25018  itg1climres  25082  mbfi1fseqlem2  25084  mbfi1fseqlem6  25088  mbfi1fseq  25089  mbfmullem  25093  itg2split  25117  itg2monolem1  25118  itg2monolem3  25120  itg2mono  25121  itg2i1fseqle  25122  itg2i1fseq  25123  itg2i1fseq2  25124  itg2addlem  25126  rolle  25357  dvlip  25360  c1lip1  25364  dvcnvrelem1  25384  dvcvx  25387  ply1divex  25504  q1pval  25521  fta1glem2  25534  fta1g  25535  fta1b  25537  plydivlem3  25658  fta1lem  25670  fta1  25671  aalioulem3  25697  aalioulem4  25698  aaliou3lem2  25706  aaliou3lem8  25708  aaliou3lem9  25713  ulmdvlem1  25762  ulmdvlem3  25764  abelthlem2  25794  abelthlem7a  25799  argrege0  25969  cxplt  26052  cxplea  26054  cxple2  26055  cxplt3  26058  logbleb  26136  logblt  26137  rlimcxp  26326  scvxcvx  26338  jensenlem2  26340  ftalem3  26427  ftalem7  26431  vmalelog  26556  chtub  26563  chpchtsum  26570  bclbnd  26631  efexple  26632  bposlem5  26639  bposlem6  26640  bposlem7  26641  lgsdilem  26675  2lgslem1a2  26741  2sqreuop  26813  2sqreuopnn  26814  2sqreuoplt  26815  2sqreuopltb  26816  2sqreuopnnlt  26817  2sqreuopnnltb  26818  dchrisumlem3  26842  dchrmusumlema  26844  dchrmusum2  26845  dchrvmasumlem2  26849  dchrvmasumlema  26851  dchrvmasumiflem1  26852  dchrisum0flblem2  26860  dchrisum0flb  26861  dchrisum0lema  26865  dchrisum0lem1b  26866  dchrisum0lem2  26869  pntrlog2bndlem2  26929  pntibndlem2  26942  pntlemf  26956  ostth2lem1  26969  qabvle  26976  sltval2  27007  sltres  27013  nolesgn2o  27022  nogesgn1o  27024  nodense  27043  nolt02o  27046  nogt01o  27047  noresle  27048  nosupbnd2lem1  27066  nosupbnd2  27067  noinfbnd2lem1  27081  noinfbnd2  27082  addsproplem1  27284  addsprop  27291  sltadd2im  27298  sleadd2im  27300  sleadd1  27301  sleadd2  27302  sltadd1  27304  sltsub1  27365  sltsub2  27366  sltsubsubbd  27371  legso  27544  iscgra  27754  isleag  27792  iseqlg  27812  brbtwn2  27857  axlowdim  27913  ewlksfval  28552  isnvlem  29555  nvtri  29615  nmlnoubi  29741  nmblolbii  29744  nmblolbi  29745  blocnilem  29749  sii  29799  ubthlem2  29816  minvecolem3  29821  minvecolem5  29826  minvecolem6  29827  norm-ii  30083  norm3dif  30095  norm3adifi  30098  bcs  30126  pjnorm  30669  pjnel  30671  nmbdoplbi  30969  nmbdoplb  30970  nmcoplb  30975  lnconi  30978  nmbdfnlb  30995  nmcfnlb  30999  pjdifnormi  31112  mdslmd2i  31275  cvmd  31281  cvexch  31319  cdj1i  31378  cdj3lem1  31379  cdj3lem2b  31382  cdj3lem3b  31385  cdj3i  31386  isoun  31618  ismnt  31846  mgcmntco  31857  dfmgc2lem  31858  dfmgc2  31859  mgcf1o  31866  isomnd  31912  omndadd  31917  omndmul  31925  ogrpinvlt  31934  gsumle  31935  isinftm  32020  xrmulc1cn  32514  lmdvg  32537  nexple  32611  faeval  32848  brfae  32850  inelcarsg  32914  carsgsigalem  32918  carsgclctunlem2  32922  carsgclctun  32924  hgt750lemc  33263  hgt750lemd  33264  hgt749d  33265  sconnpht  33826  snmlval  33928  satfv1lem  33959  satfv1  33960  satfv0fun  33968  satfv0fvfmla0  34010  lediv2aALT  34268  faclim  34322  mulsproplem1  34416  fvtransport  34620  idinside  34672  btwnconn1lem7  34681  btwnconn1lem11  34685  btwnconn1lem12  34686  nn0prpwlem  34797  bj-opabco  35662  poimirlem29  36110  heicant  36116  itg2addnclem  36132  itg2addnclem3  36134  itg2gt0cn  36136  ftc1anclem6  36159  ftc1anc  36162  ftc2nc  36163  dvasin  36165  areacirclem1  36169  seqpo  36209  incsequz  36210  metf1o  36217  mettrifi  36219  cntotbnd  36258  heiborlem4  36276  heiborlem6  36278  heiborlem10  36282  bfplem1  36284  bfplem2  36285  isopos  37645  oplecon3b  37665  atlatle  37785  4at2  38080  pmaple  38227  islaut  38549  lautcnvle  38555  lautco  38563  ltrncnvel  38608  cdlemeg49lebilem  39005  cdlemg17h  39134  tendoset  39225  tendotp  39227  cdlemk39s  39405  lcmineqlem23  40511  lcmineqlem  40512  intlewftc  40521  aks4d1p1p4  40531  dvle2  40532  aks4d1p8d2  40545  aks4d1p9  40548  aks4d1  40549  2ap1caineq  40556  sticksstones1  40557  sticksstones2  40558  sticksstones3  40559  sticksstones8  40564  sticksstones10  40566  sticksstones11  40567  sticksstones12a  40568  sticksstones15  40572  factwoffsmonot  40618  brif12  40651  dvdsexpnn0  40830  dvdsexpb  40831  reltsub1  40858  irrapxlem2  41149  irrapxlem4  41151  irrapxlem5  41152  irrapxlem6  41153  pellexlem3  41157  monotuz  41268  monotoddzzfi  41269  monotoddzz  41270  jm2.17a  41287  jm2.17b  41288  rmygeid  41291  rmydioph  41341  expdiophlem1  41348  expdiophlem2  41349  ttac  41363  fnwe2lem2  41381  relexp01min  41992  cvgdvgrat  42600  monoords  43538  supxrgelem  43578  supxrge  43579  abslt2sqd  43601  ltmulneg  43634  ltdiv23neg  43636  monoordxrv  43724  monoordxr  43725  monoord2xrv  43726  monoord2xr  43727  evthiccabs  43741  sqrlearg  43798  climinf  43854  climinff  43859  limsupres  43953  climinf2  43955  climinf2mpt  43962  climinfmpt  43963  supcnvlimsup  43988  liminfval2  44016  liminflelimsuplem  44023  liminfltlem  44052  fprodsubrecnncnvlem  44155  fprodaddrecnncnvlem  44157  ioodvbdlimc1lem1  44179  ioodvbdlimc1lem2  44180  ioodvbdlimc2lem  44182  iblspltprt  44221  itgspltprt  44227  stoweidlem3  44251  fourierdlem2  44357  fourierdlem3  44358  fourierdlem11  44366  fourierdlem12  44367  fourierdlem15  44370  fourierdlem34  44389  fourierdlem41  44396  fourierdlem48  44402  fourierdlem49  44403  fourierdlem79  44433  fourierdlem83  44437  fourierdlem89  44443  fourierdlem91  44445  fourierdlem100  44454  fourierdlem107  44461  fourierdlem109  44463  fourierdlem112  44466  etransclem31  44513  etransclem32  44514  rrndistlt  44538  ioorrnopn  44553  ioorrnopnxrlem  44554  sge0less  44640  sge0le  44655  sge0split  44657  sge0lempt  44658  sge0iunmptlemre  44663  sge0isum  44675  sge0seq  44694  meaiuninclem  44728  meaiininclem  44734  meaiininc  44735  isome  44742  omeunile  44753  omeiunlempt  44768  carageniuncllem2  44770  0ome  44777  isomenndlem  44778  isomennd  44779  ovnssle  44809  ovnsubadd  44820  hsphoidmvle2  44833  hsphoidmvle  44834  hoidmvval0  44835  hoidmv1lelem1  44839  hoidmv1lelem2  44840  hoidmv1lelem3  44841  hoidmv1le  44842  hoidmvlelem1  44843  hoidmvlelem2  44844  hoidmvlelem3  44845  hoidmvlelem4  44846  hoidmvlelem5  44847  hoidmvle  44848  hoidifhspdmvle  44868  hspmbllem2  44875  hspmbl  44877  ovnsubadd2lem  44893  ovolval4lem2  44898  ovolval4  44899  ovolval5lem2  44901  vonioolem2  44929  vonioo  44930  vonicclem2  44932  vonicc  44933  smfid  45000  smflimlem3  45021  natglobalincr  45123  tworepnotupword  45132  2elfz2melfz  45557  smonoord  45570  iccpart  45615  iccpartimp  45616  iccpartres  45617  sqrtpwpw2p  45737  ismgmALT  46164  iscmgmALT  46165  issgrpALT  46166  iscsgrpALT  46167  lindslinindsimp2lem5  46550  rrx2plordisom  46816  aacllem  47255
  Copyright terms: Public domain W3C validator