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

Theorem breq12d 4596
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 4588 . 2 ((𝐴 = 𝐵𝐶 = 𝐷) → (𝐴𝑅𝐶𝐵𝑅𝐷))
41, 2, 3syl2anc 691 1 (𝜑 → (𝐴𝑅𝐶𝐵𝑅𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 195   = wceq 1475   class class class wbr 4583
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-br 4584
This theorem is referenced by:  breq123d  4597  3brtr3d  4614  3brtr4d  4615  sbcbr  4637  pocl  4966  csbcnvgALT  5229  cnvpo  5590  sbcfung  5827  isoeq1  6467  isocnv  6480  isotr  6486  caovordig  6737  caovordg  6739  caovord2d  6741  caovord  6743  ofrfval  6803  ofrval  6805  ofrfval2  6813  caofref  6821  fnwelem  7179  fundmeng  7917  xpsneng  7930  xpcomeng  7937  xpdom2g  7941  map2xp  8015  mapdom3  8017  limensuc  8022  infensuc  8023  unxpdom  8052  pssnn  8063  dif1en  8078  unfilem3  8111  unfi  8112  domunfican  8118  fodomfi  8124  marypha1lem  8222  wemaplem1  8334  wemaplem2  8335  wemapwe  8477  dif1card  8716  infxpenlem  8719  pwsdompw  8909  infmap2  8923  sornom  8982  isfin5  9004  isfin6  9005  domtriomlem  9147  axdc2lem  9153  axdclem2  9225  pwcfsdom  9284  cfpwsdom  9285  alephom  9286  fpwwe2lem7  9337  fpwwe2lem9  9339  pwxpndom2  9366  tskcard  9482  ordpipq  9643  adderpqlem  9655  mulerpqlem  9656  mulcanenq  9661  lterpq  9671  ltanq  9672  ltmnq  9673  ltaddnq  9675  ltrnq  9680  archnq  9681  reclem4pr  9751  ltasr  9800  sqgt0sr  9806  axpre-ltadd  9867  axpre-mulgt0  9868  ltadd1  10374  leadd2  10376  ltmul2  10753  lemul2  10755  lemul1a  10756  ltdiv1  10766  ltdiv2  10788  lediv2  10792  div4p1lem1div2  11164  nn0ledivnn  11817  xleadd1  11957  xltadd2  11959  xsubge0  11963  xlemul1a  11990  xlemul1  11992  xlemul2  11993  xltmul2  11995  ltdifltdiv  12497  fzennn  12629  monoord  12693  monoord2  12694  ltexp2r  12779  leexp1a  12781  sqlecan  12833  bernneq  12852  faclbnd  12939  faclbnd3  12941  faclbnd4lem1  12942  faclbnd4lem2  12943  faclbnd4lem3  12944  faclbnd4lem4  12945  faclbnd6  12948  facubnd  12949  rlimcld2  14157  isercoll2  14247  climsup  14248  iseraltlem2  14261  fsumabs  14374  fsumrlim  14384  climcndslem1  14420  climcndslem2  14421  supcvg  14427  geomulcvg  14446  cvgrat  14454  ntrivcvgtail  14471  fprodle  14566  ruclem2  14800  ruclem8  14805  addmodlteqALT  14885  fproddvdsd  14897  sadcaddlem  15017  sadcadd  15018  nn0seqcvgd  15121  algcvg  15127  algcvga  15130  eucalgcvga  15137  isprm5  15257  qnumgt0  15296  pcprendvds2  15384  pcpremul  15386  pcadd2  15432  prmreclem4  15461  prmreclem5  15462  prmreclem6  15463  2expltfac  15637  xpsle  16064  mreexexlemd  16127  issubc  16318  latjlej2  16889  latmlem2  16905  sylow1lem3  17838  isslw  17846  fislw  17863  efgi  17955  lt6abl  18119  ablfac1eu  18295  isabv  18642  abvtri  18653  cayleyhamilton1  20516  isucn  21892  ispsmet  21919  psmettri2  21924  ismet  21938  isxmet  21939  xmettri2  21955  imasdsf1olem  21988  imasf1oxmet  21990  blvalps  22000  blval  22001  comet  22128  stdbdxmet  22130  nrmmetd  22189  tngngp  22268  tngngp3  22270  nmofval  22328  nmolb2d  22332  nmoi  22342  nmoix  22343  icopnfhmeo  22550  xrhmeo  22553  evth2  22567  pi1grplem  22657  minveclem6  23013  ovolfiniun  23076  ovoliunlem3  23079  voliunlem3  23127  ioombl1  23137  mbfmax  23222  mbfpos  23224  itg1climres  23287  mbfi1fseqlem2  23289  mbfi1fseqlem6  23293  mbfi1fseq  23294  mbfmullem  23298  itg2split  23322  itg2monolem1  23323  itg2monolem3  23325  itg2mono  23326  itg2i1fseqle  23327  itg2i1fseq  23328  itg2i1fseq2  23329  itg2addlem  23331  rolle  23557  dvlip  23560  c1lip1  23564  dvcnvrelem1  23584  dvcvx  23587  ply1divex  23700  q1pval  23717  fta1glem2  23730  fta1g  23731  fta1b  23733  plydivlem3  23854  fta1lem  23866  fta1  23867  aalioulem3  23893  aalioulem4  23894  aaliou3lem2  23902  aaliou3lem8  23904  aaliou3lem9  23909  ulmdvlem1  23958  ulmdvlem3  23960  abelthlem2  23990  abelthlem7a  23995  argrege0  24161  cxplt  24240  cxplea  24242  cxple2  24243  cxplt3  24246  logbleb  24321  logblt  24322  rlimcxp  24500  scvxcvx  24512  jensenlem2  24514  ftalem3  24601  ftalem7  24605  vmalelog  24730  chtub  24737  chpchtsum  24744  bclbnd  24805  efexple  24806  bposlem5  24813  bposlem6  24814  bposlem7  24815  lgsdilem  24849  2lgslem1a2  24915  dchrisumlem3  24980  dchrmusumlema  24982  dchrmusum2  24983  dchrvmasumlem2  24987  dchrvmasumlema  24989  dchrvmasumiflem1  24990  dchrisum0flblem2  24998  dchrisum0flb  24999  dchrisum0lema  25003  dchrisum0lem1b  25004  dchrisum0lem2  25007  pntrlog2bndlem2  25067  pntibndlem2  25080  pntlemf  25094  ostth2lem1  25107  qabvle  25114  legso  25294  iscgra  25501  isleag  25533  iseqlg  25547  brbtwn2  25585  axlowdim  25641  sizeusglecusg  26014  isrusgra  26454  extwwlkfablem2  26605  isnvlem  26849  nvtri  26909  nmlnoubi  27035  nmblolbii  27038  nmblolbi  27039  blocnilem  27043  sii  27093  ubthlem2  27111  minvecolem3  27116  minvecolem5  27121  minvecolem6  27122  norm-ii  27379  norm3dif  27391  norm3adifi  27394  bcs  27422  pjnorm  27967  pjnel  27969  nmbdoplbi  28267  nmbdoplb  28268  nmcoplb  28273  lnconi  28276  nmbdfnlb  28293  nmcfnlb  28297  pjdifnormi  28410  mdslmd2i  28573  cvmd  28579  cvexch  28617  cdj1i  28676  cdj3lem1  28677  cdj3lem2b  28680  cdj3lem3b  28683  cdj3i  28684  isoun  28862  isomnd  29032  omndadd  29037  omndmul  29045  ogrpinvlt  29055  isinftm  29066  gsumle  29110  xrmulc1cn  29304  lmdvg  29327  nexple  29399  faeval  29636  brfae  29638  inelcarsg  29700  carsgsigalem  29704  carsgclctunlem2  29708  carsgclctun  29710  sconpht  30465  snmlval  30567  lediv2aALT  30825  faclim  30885  poseq  30994  sltval2  31053  sltres  31061  nodense  31088  nobndup  31099  nobnddown  31100  fvtransport  31309  idinside  31361  btwnconn1lem7  31370  btwnconn1lem11  31374  btwnconn1lem12  31375  nn0prpwlem  31487  poimirlem29  32608  heicant  32614  itg2addnclem  32631  itg2addnclem3  32633  itg2gt0cn  32635  ftc1anclem6  32660  ftc1anc  32663  ftc2nc  32664  dvasin  32666  areacirclem1  32670  seqpo  32713  incsequz  32714  metf1o  32721  mettrifi  32723  cntotbnd  32765  heiborlem4  32783  heiborlem6  32785  heiborlem10  32789  bfplem1  32791  bfplem2  32792  isopos  33485  oplecon3b  33505  atlatle  33625  4at2  33918  pmaple  34065  islaut  34387  lautcnvle  34393  lautco  34401  ltrncnvel  34446  cdlemeg49lebilem  34845  cdlemg17h  34974  tendoset  35065  tendotp  35067  cdlemk39s  35245  irrapxlem2  36405  irrapxlem4  36407  irrapxlem5  36408  irrapxlem6  36409  pellexlem3  36413  monotuz  36524  monotoddzzfi  36525  monotoddzz  36526  expmordi  36530  jm2.17a  36545  jm2.17b  36546  rmygeid  36549  rmydioph  36599  expdiophlem1  36606  expdiophlem2  36607  ttac  36621  fnwe2lem2  36639  relexp01min  37024  cvgdvgrat  37534  monoords  38452  supxrgelem  38494  supxrge  38495  abslt2sqd  38517  ltmulneg  38556  ltdiv23neg  38558  evthiccabs  38565  sqrlearg  38627  climinf  38673  climinff  38678  fprodsubrecnncnvlem  38794  fprodaddrecnncnvlem  38796  ioodvbdlimc1lem1  38821  ioodvbdlimc1lem2  38822  ioodvbdlimc2lem  38824  iblspltprt  38865  itgspltprt  38871  stoweidlem3  38896  fourierdlem2  39002  fourierdlem3  39003  fourierdlem11  39011  fourierdlem12  39012  fourierdlem15  39015  fourierdlem34  39034  fourierdlem41  39041  fourierdlem48  39047  fourierdlem49  39048  fourierdlem79  39078  fourierdlem83  39082  fourierdlem89  39088  fourierdlem91  39090  fourierdlem100  39099  fourierdlem107  39106  fourierdlem109  39108  fourierdlem112  39111  etransclem31  39158  etransclem32  39159  rrndistlt  39186  ioorrnopn  39201  ioorrnopnxrlem  39202  sge0less  39285  sge0le  39300  sge0split  39302  sge0lempt  39303  sge0iunmptlemre  39308  sge0isum  39320  sge0seq  39339  meaiuninclem  39373  meaiininclem  39376  meaiininc  39377  isome  39384  omeunile  39395  omeiunlempt  39410  carageniuncllem2  39412  0ome  39419  isomenndlem  39420  isomennd  39421  ovnsslelem  39450  ovnssle  39451  ovnsubadd  39462  hsphoidmvle2  39475  hsphoidmvle  39476  hoidmvval0  39477  hoidmv1lelem1  39481  hoidmv1lelem2  39482  hoidmv1lelem3  39483  hoidmv1le  39484  hoidmvlelem1  39485  hoidmvlelem2  39486  hoidmvlelem3  39487  hoidmvlelem4  39488  hoidmvlelem5  39489  hoidmvle  39490  hoidifhspdmvle  39510  hspmbllem2  39517  hspmbl  39519  ovnsubadd2lem  39535  ovolval4lem2  39540  ovolval4  39541  ovolval5lem2  39543  vonioolem2  39572  vonioo  39573  vonicclem2  39575  vonicc  39576  smfid  39639  smflimlem3  39659  smonoord  39944  iccpart  39954  iccpartimp  39955  iccpartres  39956  sqrtpwpw2p  39988  2elfz2melfz  40355  ewlksfval  40803  ismgmALT  41649  iscmgmALT  41650  issgrpALT  41651  iscsgrpALT  41652  lindslinindsimp2lem5  42045  aacllem  42356
  Copyright terms: Public domain W3C validator