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

Theorem breq12d 4636
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 4628 . 2 ((𝐴 = 𝐵𝐶 = 𝐷) → (𝐴𝑅𝐶𝐵𝑅𝐷))
41, 2, 3syl2anc 692 1 (𝜑 → (𝐴𝑅𝐶𝐵𝑅𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196   = wceq 1480   class class class wbr 4623
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-rab 2917  df-v 3192  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-nul 3898  df-if 4065  df-sn 4156  df-pr 4158  df-op 4162  df-br 4624
This theorem is referenced by:  breq123d  4637  3brtr3d  4654  3brtr4d  4655  sbcbr  4677  pocl  5012  csbcnvgALT  5277  cnvpo  5642  sbcfung  5881  isoeq1  6532  isocnv  6545  isotr  6551  caovordig  6804  caovordg  6806  caovord2d  6808  caovord  6810  ofrfval  6870  ofrval  6872  ofrfval2  6880  caofref  6888  fnwelem  7252  fundmeng  7991  xpsneng  8005  xpcomeng  8012  xpdom2g  8016  map2xp  8090  mapdom3  8092  limensuc  8097  infensuc  8098  unxpdom  8127  pssnn  8138  dif1en  8153  unfilem3  8186  unfi  8187  domunfican  8193  fodomfi  8199  marypha1lem  8299  wemaplem1  8411  wemaplem2  8412  wemapwe  8554  dif1card  8793  infxpenlem  8796  pwsdompw  8986  infmap2  9000  sornom  9059  isfin5  9081  isfin6  9082  domtriomlem  9224  axdc2lem  9230  axdclem2  9302  pwcfsdom  9365  cfpwsdom  9366  alephom  9367  fpwwe2lem7  9418  fpwwe2lem9  9420  pwxpndom2  9447  tskcard  9563  ordpipq  9724  adderpqlem  9736  mulerpqlem  9737  mulcanenq  9742  lterpq  9752  ltanq  9753  ltmnq  9754  ltaddnq  9756  ltrnq  9761  archnq  9762  reclem4pr  9832  ltasr  9881  sqgt0sr  9887  axpre-ltadd  9948  axpre-mulgt0  9949  ltadd1  10455  leadd2  10457  ltmul2  10834  lemul2  10836  lemul1a  10837  ltdiv1  10847  ltdiv2  10869  lediv2  10873  div4p1lem1div2  11247  nn0ledivnn  11901  xleadd1  12044  xltadd2  12046  xsubge0  12050  xlemul1a  12077  xlemul1  12079  xlemul2  12080  xltmul2  12082  ltdifltdiv  12591  fzennn  12723  monoord  12787  monoord2  12788  ltexp2r  12873  leexp1a  12875  sqlecan  12927  bernneq  12946  faclbnd  13033  faclbnd3  13035  faclbnd4lem1  13036  faclbnd4lem2  13037  faclbnd4lem3  13038  faclbnd4lem4  13039  faclbnd6  13042  facubnd  13043  rlimcld2  14259  isercoll2  14349  climsup  14350  iseraltlem2  14363  fsumabs  14479  fsumrlim  14489  climcndslem1  14525  climcndslem2  14526  supcvg  14532  geomulcvg  14551  cvgrat  14559  ntrivcvgtail  14576  fprodle  14671  ruclem2  14905  ruclem8  14910  addmodlteqALT  14990  fproddvdsd  15002  sadcaddlem  15122  sadcadd  15123  nn0seqcvgd  15226  algcvg  15232  algcvga  15235  eucalgcvga  15242  isprm5  15362  qnumgt0  15401  pcprendvds2  15489  pcpremul  15491  pcadd2  15537  prmreclem4  15566  prmreclem5  15567  prmreclem6  15568  2expltfac  15742  xpsle  16181  mreexexlemd  16244  issubc  16435  latjlej2  17006  latmlem2  17022  sylow1lem3  17955  isslw  17963  fislw  17980  efgi  18072  lt6abl  18236  ablfac1eu  18412  isabv  18759  abvtri  18770  cayleyhamilton1  20637  isucn  22022  ispsmet  22049  psmettri2  22054  ismet  22068  isxmet  22069  xmettri2  22085  imasdsf1olem  22118  imasf1oxmet  22120  blvalps  22130  blval  22131  comet  22258  stdbdxmet  22260  nrmmetd  22319  tngngp  22398  tngngp3  22400  nmofval  22458  nmolb2d  22462  nmoi  22472  nmoix  22473  icopnfhmeo  22682  xrhmeo  22685  evth2  22699  pi1grplem  22789  minveclem6  23145  ovolfiniun  23209  ovoliunlem3  23212  voliunlem3  23260  ioombl1  23270  mbfmax  23356  mbfpos  23358  itg1climres  23421  mbfi1fseqlem2  23423  mbfi1fseqlem6  23427  mbfi1fseq  23428  mbfmullem  23432  itg2split  23456  itg2monolem1  23457  itg2monolem3  23459  itg2mono  23460  itg2i1fseqle  23461  itg2i1fseq  23462  itg2i1fseq2  23463  itg2addlem  23465  rolle  23691  dvlip  23694  c1lip1  23698  dvcnvrelem1  23718  dvcvx  23721  ply1divex  23834  q1pval  23851  fta1glem2  23864  fta1g  23865  fta1b  23867  plydivlem3  23988  fta1lem  24000  fta1  24001  aalioulem3  24027  aalioulem4  24028  aaliou3lem2  24036  aaliou3lem8  24038  aaliou3lem9  24043  ulmdvlem1  24092  ulmdvlem3  24094  abelthlem2  24124  abelthlem7a  24129  argrege0  24295  cxplt  24374  cxplea  24376  cxple2  24377  cxplt3  24380  logbleb  24455  logblt  24456  rlimcxp  24634  scvxcvx  24646  jensenlem2  24648  ftalem3  24735  ftalem7  24739  vmalelog  24864  chtub  24871  chpchtsum  24878  bclbnd  24939  efexple  24940  bposlem5  24947  bposlem6  24948  bposlem7  24949  lgsdilem  24983  2lgslem1a2  25049  dchrisumlem3  25114  dchrmusumlema  25116  dchrmusum2  25117  dchrvmasumlem2  25121  dchrvmasumlema  25123  dchrvmasumiflem1  25124  dchrisum0flblem2  25132  dchrisum0flb  25133  dchrisum0lema  25137  dchrisum0lem1b  25138  dchrisum0lem2  25141  pntrlog2bndlem2  25201  pntibndlem2  25214  pntlemf  25228  ostth2lem1  25241  qabvle  25248  legso  25428  iscgra  25635  isleag  25667  iseqlg  25681  brbtwn2  25719  axlowdim  25775  ewlksfval  26401  isnvlem  27353  nvtri  27413  nmlnoubi  27539  nmblolbii  27542  nmblolbi  27543  blocnilem  27547  sii  27597  ubthlem2  27615  minvecolem3  27620  minvecolem5  27625  minvecolem6  27626  norm-ii  27883  norm3dif  27895  norm3adifi  27898  bcs  27926  pjnorm  28471  pjnel  28473  nmbdoplbi  28771  nmbdoplb  28772  nmcoplb  28777  lnconi  28780  nmbdfnlb  28797  nmcfnlb  28801  pjdifnormi  28914  mdslmd2i  29077  cvmd  29083  cvexch  29121  cdj1i  29180  cdj3lem1  29181  cdj3lem2b  29184  cdj3lem3b  29187  cdj3i  29188  isoun  29363  isomnd  29528  omndadd  29533  omndmul  29541  ogrpinvlt  29551  isinftm  29562  gsumle  29606  xrmulc1cn  29800  lmdvg  29823  nexple  29895  faeval  30132  brfae  30134  inelcarsg  30196  carsgsigalem  30200  carsgclctunlem2  30204  carsgclctun  30206  sconnpht  30972  snmlval  31074  lediv2aALT  31332  faclim  31393  poseq  31504  sltval2  31563  sltres  31571  nodense  31605  nobndup  31616  nobnddown  31617  noreslege  31624  fvtransport  31834  idinside  31886  btwnconn1lem7  31895  btwnconn1lem11  31899  btwnconn1lem12  31900  nn0prpwlem  32012  poimirlem29  33109  heicant  33115  itg2addnclem  33132  itg2addnclem3  33134  itg2gt0cn  33136  ftc1anclem6  33161  ftc1anc  33164  ftc2nc  33165  dvasin  33167  areacirclem1  33171  seqpo  33214  incsequz  33215  metf1o  33222  mettrifi  33224  cntotbnd  33266  heiborlem4  33284  heiborlem6  33286  heiborlem10  33290  bfplem1  33292  bfplem2  33293  isopos  33986  oplecon3b  34006  atlatle  34126  4at2  34419  pmaple  34566  islaut  34888  lautcnvle  34894  lautco  34902  ltrncnvel  34947  cdlemeg49lebilem  35346  cdlemg17h  35475  tendoset  35566  tendotp  35568  cdlemk39s  35746  irrapxlem2  36906  irrapxlem4  36908  irrapxlem5  36909  irrapxlem6  36910  pellexlem3  36914  monotuz  37025  monotoddzzfi  37026  monotoddzz  37027  expmordi  37031  jm2.17a  37046  jm2.17b  37047  rmygeid  37050  rmydioph  37100  expdiophlem1  37107  expdiophlem2  37108  ttac  37122  fnwe2lem2  37140  relexp01min  37525  cvgdvgrat  38033  monoords  39010  supxrgelem  39052  supxrge  39053  abslt2sqd  39075  ltmulneg  39114  ltdiv23neg  39116  evthiccabs  39164  sqrlearg  39226  climinf  39274  climinff  39279  limsupres  39373  climinf2  39375  climinf2mpt  39382  climinfmpt  39383  supcnvlimsup  39408  fprodsubrecnncnvlem  39456  fprodaddrecnncnvlem  39458  ioodvbdlimc1lem1  39483  ioodvbdlimc1lem2  39484  ioodvbdlimc2lem  39486  iblspltprt  39526  itgspltprt  39532  stoweidlem3  39557  fourierdlem2  39663  fourierdlem3  39664  fourierdlem11  39672  fourierdlem12  39673  fourierdlem15  39676  fourierdlem34  39695  fourierdlem41  39702  fourierdlem48  39708  fourierdlem49  39709  fourierdlem79  39739  fourierdlem83  39743  fourierdlem89  39749  fourierdlem91  39751  fourierdlem100  39760  fourierdlem107  39767  fourierdlem109  39769  fourierdlem112  39772  etransclem31  39819  etransclem32  39820  rrndistlt  39847  ioorrnopn  39862  ioorrnopnxrlem  39863  sge0less  39946  sge0le  39961  sge0split  39963  sge0lempt  39964  sge0iunmptlemre  39969  sge0isum  39981  sge0seq  40000  meaiuninclem  40034  meaiininclem  40037  meaiininc  40038  isome  40045  omeunile  40056  omeiunlempt  40071  carageniuncllem2  40073  0ome  40080  isomenndlem  40081  isomennd  40082  ovnsslelem  40111  ovnssle  40112  ovnsubadd  40123  hsphoidmvle2  40136  hsphoidmvle  40137  hoidmvval0  40138  hoidmv1lelem1  40142  hoidmv1lelem2  40143  hoidmv1lelem3  40144  hoidmv1le  40145  hoidmvlelem1  40146  hoidmvlelem2  40147  hoidmvlelem3  40148  hoidmvlelem4  40149  hoidmvlelem5  40150  hoidmvle  40151  hoidifhspdmvle  40171  hspmbllem2  40178  hspmbl  40180  ovnsubadd2lem  40196  ovolval4lem2  40201  ovolval4  40202  ovolval5lem2  40204  vonioolem2  40232  vonioo  40233  vonicclem2  40235  vonicc  40236  smfid  40298  smflimlem3  40318  2elfz2melfz  40655  smonoord  40669  iccpart  40680  iccpartimp  40681  iccpartres  40682  sqrtpwpw2p  40779  ismgmALT  41177  iscmgmALT  41178  issgrpALT  41179  iscsgrpALT  41180  lindslinindsimp2lem5  41569  aacllem  41880
  Copyright terms: Public domain W3C validator