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

Theorem breq12d 4698
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 4690 . 2 ((𝐴 = 𝐵𝐶 = 𝐷) → (𝐴𝑅𝐶𝐵𝑅𝐷))
41, 2, 3syl2anc 694 1 (𝜑 → (𝐴𝑅𝐶𝐵𝑅𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196   = wceq 1523   class class class wbr 4685
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-rab 2950  df-v 3233  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-br 4686
This theorem is referenced by:  breq123d  4699  3brtr3d  4716  3brtr4d  4717  sbcbr  4740  pocl  5071  csbcnvgALT  5339  cnvpo  5711  sbcfung  5950  isoeq1  6607  isocnv  6620  isotr  6626  caovordig  6881  caovordg  6883  caovord2d  6885  caovord  6887  ofrfval  6947  ofrval  6949  ofrfval2  6957  caofref  6965  fnwelem  7337  fundmeng  8072  xpsneng  8086  xpcomeng  8093  xpdom2g  8097  map2xp  8171  mapdom3  8173  limensuc  8178  infensuc  8179  unxpdom  8208  pssnn  8219  dif1en  8234  unfilem3  8267  unfi  8268  domunfican  8274  fodomfi  8280  marypha1lem  8380  wemaplem1  8492  wemaplem2  8493  wemapwe  8632  dif1card  8871  infxpenlem  8874  pwsdompw  9064  infmap2  9078  sornom  9137  isfin5  9159  isfin6  9160  domtriomlem  9302  axdc2lem  9308  axdclem2  9380  pwcfsdom  9443  cfpwsdom  9444  alephom  9445  fpwwe2lem7  9496  fpwwe2lem9  9498  pwxpndom2  9525  tskcard  9641  ordpipq  9802  adderpqlem  9814  mulerpqlem  9815  mulcanenq  9820  lterpq  9830  ltanq  9831  ltmnq  9832  ltaddnq  9834  ltrnq  9839  archnq  9840  reclem4pr  9910  ltasr  9959  sqgt0sr  9965  axpre-ltadd  10026  axpre-mulgt0  10027  ltadd1  10533  leadd2  10535  ltmul2  10912  lemul2  10914  lemul1a  10915  ltdiv1  10925  ltdiv2  10947  lediv2  10951  div4p1lem1div2  11325  nn0ledivnn  11979  xleadd1  12123  xltadd2  12125  xsubge0  12129  xlemul1a  12156  xlemul1  12158  xlemul2  12159  xltmul2  12161  ltdifltdiv  12675  fzennn  12807  monoord  12871  monoord2  12872  ltexp2r  12957  leexp1a  12959  sqlecan  13011  bernneq  13030  faclbnd  13117  faclbnd3  13119  faclbnd4lem1  13120  faclbnd4lem2  13121  faclbnd4lem3  13122  faclbnd4lem4  13123  faclbnd6  13126  facubnd  13127  rlimcld2  14353  isercoll2  14443  climsup  14444  iseraltlem2  14457  fsumabs  14577  fsumrlim  14587  climcndslem1  14625  climcndslem2  14626  supcvg  14632  geomulcvg  14651  cvgrat  14659  ntrivcvgtail  14676  fprodle  14771  ruclem2  15005  ruclem8  15010  addmodlteqALT  15094  fproddvdsd  15106  sadcaddlem  15226  sadcadd  15227  nn0seqcvgd  15330  algcvg  15336  algcvga  15339  eucalgcvga  15346  isprm5  15466  qnumgt0  15505  pcprendvds2  15593  pcpremul  15595  pcadd2  15641  prmreclem4  15670  prmreclem5  15671  prmreclem6  15672  2expltfac  15846  xpsle  16288  mreexexlemd  16351  issubc  16542  latjlej2  17113  latmlem2  17129  sylow1lem3  18061  isslw  18069  fislw  18086  efgi  18178  lt6abl  18342  ablfac1eu  18518  isabv  18867  abvtri  18878  cayleyhamilton1  20745  isucn  22129  ispsmet  22156  psmettri2  22161  ismet  22175  isxmet  22176  xmettri2  22192  imasdsf1olem  22225  imasf1oxmet  22227  blvalps  22237  blval  22238  comet  22365  stdbdxmet  22367  nrmmetd  22426  tngngp  22505  tngngp3  22507  nmofval  22565  nmolb2d  22569  nmoi  22579  nmoix  22580  icopnfhmeo  22789  xrhmeo  22792  evth2  22806  pi1grplem  22895  minveclem6  23251  ovolfiniun  23315  ovoliunlem3  23318  voliunlem3  23366  ioombl1  23376  mbfmax  23461  mbfpos  23463  itg1climres  23526  mbfi1fseqlem2  23528  mbfi1fseqlem6  23532  mbfi1fseq  23533  mbfmullem  23537  itg2split  23561  itg2monolem1  23562  itg2monolem3  23564  itg2mono  23565  itg2i1fseqle  23566  itg2i1fseq  23567  itg2i1fseq2  23568  itg2addlem  23570  rolle  23798  dvlip  23801  c1lip1  23805  dvcnvrelem1  23825  dvcvx  23828  ply1divex  23941  q1pval  23958  fta1glem2  23971  fta1g  23972  fta1b  23974  plydivlem3  24095  fta1lem  24107  fta1  24108  aalioulem3  24134  aalioulem4  24135  aaliou3lem2  24143  aaliou3lem8  24145  aaliou3lem9  24150  ulmdvlem1  24199  ulmdvlem3  24201  abelthlem2  24231  abelthlem7a  24236  argrege0  24402  cxplt  24485  cxplea  24487  cxple2  24488  cxplt3  24491  logbleb  24566  logblt  24567  rlimcxp  24745  scvxcvx  24757  jensenlem2  24759  ftalem3  24846  ftalem7  24850  vmalelog  24975  chtub  24982  chpchtsum  24989  bclbnd  25050  efexple  25051  bposlem5  25058  bposlem6  25059  bposlem7  25060  lgsdilem  25094  2lgslem1a2  25160  dchrisumlem3  25225  dchrmusumlema  25227  dchrmusum2  25228  dchrvmasumlem2  25232  dchrvmasumlema  25234  dchrvmasumiflem1  25235  dchrisum0flblem2  25243  dchrisum0flb  25244  dchrisum0lema  25248  dchrisum0lem1b  25249  dchrisum0lem2  25252  pntrlog2bndlem2  25312  pntibndlem2  25325  pntlemf  25339  ostth2lem1  25352  qabvle  25359  legso  25539  iscgra  25746  isleag  25778  iseqlg  25792  brbtwn2  25830  axlowdim  25886  ewlksfval  26553  isnvlem  27593  nvtri  27653  nmlnoubi  27779  nmblolbii  27782  nmblolbi  27783  blocnilem  27787  sii  27837  ubthlem2  27855  minvecolem3  27860  minvecolem5  27865  minvecolem6  27866  norm-ii  28123  norm3dif  28135  norm3adifi  28138  bcs  28166  pjnorm  28711  pjnel  28713  nmbdoplbi  29011  nmbdoplb  29012  nmcoplb  29017  lnconi  29020  nmbdfnlb  29037  nmcfnlb  29041  pjdifnormi  29154  mdslmd2i  29317  cvmd  29323  cvexch  29361  cdj1i  29420  cdj3lem1  29421  cdj3lem2b  29424  cdj3lem3b  29427  cdj3i  29428  isoun  29607  isomnd  29829  omndadd  29834  omndmul  29842  ogrpinvlt  29852  isinftm  29863  gsumle  29907  xrmulc1cn  30104  lmdvg  30127  nexple  30199  faeval  30437  brfae  30439  inelcarsg  30501  carsgsigalem  30505  carsgclctunlem2  30509  carsgclctun  30511  hgt750lemc  30853  hgt750lemd  30854  hgt749d  30855  sconnpht  31337  snmlval  31439  lediv2aALT  31697  faclim  31758  poseq  31878  sltval2  31934  sltres  31940  nolesgn2o  31949  nodense  31967  nolt02o  31970  noresle  31971  nosupbnd2lem1  31986  nosupbnd2  31987  fvtransport  32264  idinside  32316  btwnconn1lem7  32325  btwnconn1lem11  32329  btwnconn1lem12  32330  nn0prpwlem  32442  poimirlem29  33568  heicant  33574  itg2addnclem  33591  itg2addnclem3  33593  itg2gt0cn  33595  ftc1anclem6  33620  ftc1anc  33623  ftc2nc  33624  dvasin  33626  areacirclem1  33630  seqpo  33673  incsequz  33674  metf1o  33681  mettrifi  33683  cntotbnd  33725  heiborlem4  33743  heiborlem6  33745  heiborlem10  33749  bfplem1  33751  bfplem2  33752  isopos  34785  oplecon3b  34805  atlatle  34925  4at2  35218  pmaple  35365  islaut  35687  lautcnvle  35693  lautco  35701  ltrncnvel  35746  cdlemeg49lebilem  36144  cdlemg17h  36273  tendoset  36364  tendotp  36366  cdlemk39s  36544  irrapxlem2  37704  irrapxlem4  37706  irrapxlem5  37707  irrapxlem6  37708  pellexlem3  37712  monotuz  37823  monotoddzzfi  37824  monotoddzz  37825  expmordi  37829  jm2.17a  37844  jm2.17b  37845  rmygeid  37848  rmydioph  37898  expdiophlem1  37905  expdiophlem2  37906  ttac  37920  fnwe2lem2  37938  relexp01min  38322  cvgdvgrat  38829  monoords  39825  supxrgelem  39866  supxrge  39867  abslt2sqd  39889  ltmulneg  39928  ltdiv23neg  39930  monoordxrv  40025  monoordxr  40026  monoord2xrv  40027  monoord2xr  40028  evthiccabs  40036  sqrlearg  40098  climinf  40156  climinff  40161  limsupres  40255  climinf2  40257  climinf2mpt  40264  climinfmpt  40265  supcnvlimsup  40290  liminfval2  40318  liminflelimsuplem  40325  liminfltlem  40354  fprodsubrecnncnvlem  40439  fprodaddrecnncnvlem  40441  ioodvbdlimc1lem1  40464  ioodvbdlimc1lem2  40465  ioodvbdlimc2lem  40467  iblspltprt  40507  itgspltprt  40513  stoweidlem3  40538  fourierdlem2  40644  fourierdlem3  40645  fourierdlem11  40653  fourierdlem12  40654  fourierdlem15  40657  fourierdlem34  40676  fourierdlem41  40683  fourierdlem48  40689  fourierdlem49  40690  fourierdlem79  40720  fourierdlem83  40724  fourierdlem89  40730  fourierdlem91  40732  fourierdlem100  40741  fourierdlem107  40748  fourierdlem109  40750  fourierdlem112  40753  etransclem31  40800  etransclem32  40801  rrndistlt  40828  ioorrnopn  40843  ioorrnopnxrlem  40844  sge0less  40927  sge0le  40942  sge0split  40944  sge0lempt  40945  sge0iunmptlemre  40950  sge0isum  40962  sge0seq  40981  meaiuninclem  41015  meaiininclem  41021  meaiininc  41022  isome  41029  omeunile  41040  omeiunlempt  41055  carageniuncllem2  41057  0ome  41064  isomenndlem  41065  isomennd  41066  ovnsslelem  41095  ovnssle  41096  ovnsubadd  41107  hsphoidmvle2  41120  hsphoidmvle  41121  hoidmvval0  41122  hoidmv1lelem1  41126  hoidmv1lelem2  41127  hoidmv1lelem3  41128  hoidmv1le  41129  hoidmvlelem1  41130  hoidmvlelem2  41131  hoidmvlelem3  41132  hoidmvlelem4  41133  hoidmvlelem5  41134  hoidmvle  41135  hoidifhspdmvle  41155  hspmbllem2  41162  hspmbl  41164  ovnsubadd2lem  41180  ovolval4lem2  41185  ovolval4  41186  ovolval5lem2  41188  vonioolem2  41216  vonioo  41217  vonicclem2  41219  vonicc  41220  smfid  41282  smflimlem3  41302  2elfz2melfz  41653  smonoord  41666  iccpart  41677  iccpartimp  41678  iccpartres  41679  sqrtpwpw2p  41775  ismgmALT  42184  iscmgmALT  42185  issgrpALT  42186  iscsgrpALT  42187  lindslinindsimp2lem5  42576  aacllem  42875
  Copyright terms: Public domain W3C validator