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

Theorem breq12d 4460
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  |-  ( ph  ->  A  =  B )
breq12d.2  |-  ( ph  ->  C  =  D )
Assertion
Ref Expression
breq12d  |-  ( ph  ->  ( A R C  <-> 
B R D ) )

Proof of Theorem breq12d
StepHypRef Expression
1 breq1d.1 . 2  |-  ( ph  ->  A  =  B )
2 breq12d.2 . 2  |-  ( ph  ->  C  =  D )
3 breq12 4452 . 2  |-  ( ( A  =  B  /\  C  =  D )  ->  ( A R C  <-> 
B R D ) )
41, 2, 3syl2anc 661 1  |-  ( ph  ->  ( A R C  <-> 
B R D ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    = wceq 1379   class class class wbr 4447
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-rab 2823  df-v 3115  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-sn 4028  df-pr 4030  df-op 4034  df-br 4448
This theorem is referenced by:  breq123d  4461  3brtr3d  4476  3brtr4d  4477  sbcbr  4500  pocl  4807  csbcnvgALT  5185  cnvpo  5543  sbcfung  5609  isoeq1  6201  isocnv  6212  isotr  6218  caovordig  6462  caovordg  6464  caovord2d  6466  caovord  6468  ofrfval  6530  ofrval  6532  ofrfval2  6539  caofref  6548  fnwelem  6895  fundmeng  7587  xpsneng  7599  xpcomeng  7606  xpdom2g  7610  map2xp  7684  mapdom3  7686  limensuc  7691  infensuc  7692  unxpdom  7724  pssnn  7735  dif1enOLD  7748  dif1en  7749  unfilem3  7782  unfi  7783  domunfican  7789  fodomfi  7795  marypha1lem  7889  wemaplem1  7967  wemaplem2  7968  wemapwe  8135  wemapweOLD  8136  dif1card  8384  infxpenlem  8387  pwsdompw  8580  infmap2  8594  sornom  8653  isfin5  8675  isfin6  8676  domtriomlem  8818  axdc2lem  8824  axdclem2  8896  pwcfsdom  8954  cfpwsdom  8955  alephom  8956  fpwwe2lem7  9010  fpwwe2lem9  9012  pwxpndom2  9039  tskcard  9155  ordpipq  9316  adderpqlem  9328  mulerpqlem  9329  mulcanenq  9334  lterpq  9344  ltanq  9345  ltmnq  9346  ltaddnq  9348  ltrnq  9353  archnq  9354  reclem4pr  9424  ltasr  9473  sqgt0sr  9479  axpre-ltadd  9540  axpre-mulgt0  9541  ltadd1  10015  leadd2  10017  ltmul2  10389  lemul2  10391  lemul1a  10392  ltdiv1  10402  ltdiv2  10426  lediv2  10431  uzindOLD  10951  xleadd1  11443  xltadd2  11445  xsubge0  11449  xlemul1a  11476  xlemul1  11478  xlemul2  11479  xltmul2  11481  ltdifltdiv  11929  fzennn  12041  monoord  12100  monoord2  12101  ltexp2r  12184  leexp1a  12186  sqlecan  12236  bernneq  12254  faclbnd  12330  faclbnd3  12332  faclbnd4lem1  12333  faclbnd4lem2  12334  faclbnd4lem3  12335  faclbnd4lem4  12336  faclbnd6  12339  facubnd  12340  rlimcld2  13357  isercoll2  13447  climsup  13448  iseraltlem2  13461  fsumabs  13571  fsumrlim  13581  climcndslem1  13617  climcndslem2  13618  supcvg  13623  geomulcvg  13641  cvgrat  13648  ruclem2  13819  ruclem8  13824  sadcaddlem  13959  sadcadd  13960  nn0seqcvgd  14051  algcvg  14057  algcvga  14060  eucalgcvga  14067  isprm5  14105  qnumgt0  14135  pcprendvds2  14217  pcpremul  14219  pcadd2  14261  prmreclem4  14289  prmreclem5  14290  prmreclem6  14291  2expltfac  14428  xpsle  14829  mreexexlemd  14892  issubc  15058  latjlej2  15546  latmlem2  15562  sylow1lem3  16413  isslw  16421  fislw  16438  efgi  16530  lt6abl  16685  ablfac1eu  16911  isabv  17248  abvtri  17259  cayleyhamilton1  19157  isucn  20513  ispsmet  20540  psmettri2  20545  ismet  20558  isxmet  20559  xmettri2  20575  imasdsf1olem  20608  imasf1oxmet  20610  blvalps  20620  blval  20621  comet  20748  stdbdxmet  20750  nrmmetd  20827  tngngp  20900  nmofval  20953  nmolb2d  20957  nmoi  20967  nmoix  20968  icopnfhmeo  21175  xrhmeo  21178  evth2  21192  pi1grplem  21281  minveclem6  21581  ovolfiniun  21644  ovoliunlem3  21647  voliunlem3  21694  ioombl1  21704  mbfmax  21788  mbfpos  21790  itg1climres  21853  mbfi1fseqlem2  21855  mbfi1fseqlem6  21859  mbfi1fseq  21860  mbfmullem  21864  itg2split  21888  itg2monolem1  21889  itg2monolem3  21891  itg2mono  21892  itg2i1fseqle  21893  itg2i1fseq  21894  itg2i1fseq2  21895  itg2addlem  21897  rolle  22123  dvlip  22126  c1lip1  22130  dvcnvrelem1  22150  dvcvx  22153  ply1divex  22269  q1pval  22286  fta1glem2  22299  fta1g  22300  fta1b  22302  plydivlem3  22422  fta1lem  22434  fta1  22435  aalioulem3  22461  aalioulem4  22462  aaliou3lem2  22470  aaliou3lem8  22472  aaliou3lem9  22477  ulmdvlem1  22526  ulmdvlem3  22528  abelthlem2  22558  abelthlem7a  22563  argrege0  22721  cxplt  22800  cxplea  22802  cxple2  22803  cxplt3  22806  rlimcxp  23028  scvxcvx  23040  jensenlem2  23042  ftalem3  23073  ftalem7  23077  vmalelog  23205  chtub  23212  chpchtsum  23219  bclbnd  23280  efexple  23281  bposlem5  23288  bposlem6  23289  bposlem7  23290  lgsdilem  23322  dchrisumlem3  23401  dchrmusumlema  23403  dchrmusum2  23404  dchrvmasumlem2  23408  dchrvmasumlema  23410  dchrvmasumiflem1  23411  dchrisum0flblem2  23419  dchrisum0flb  23420  dchrisum0lema  23424  dchrisum0lem1b  23425  dchrisum0lem2  23428  pntrlog2bndlem2  23488  pntibndlem2  23501  pntlemf  23515  ostth2lem1  23528  qabvle  23535  legso  23709  brbtwn2  23881  axlowdim  23937  sizeusglecusg  24159  isrusgra  24600  extwwlkfablem2  24752  isnvlem  25176  nvtri  25246  nmlnoubi  25384  nmblolbii  25387  nmblolbi  25388  blocnilem  25392  sii  25442  ubthlem2  25460  minvecolem3  25465  minvecolem5  25470  minvecolem6  25471  norm-ii  25728  norm3dif  25740  norm3adifi  25743  bcs  25771  pjnorm  26315  pjnel  26317  nmbdoplbi  26616  nmbdoplb  26617  nmcoplb  26622  lnconi  26625  nmbdfnlb  26642  nmcfnlb  26646  pjdifnormi  26759  mdslmd2i  26922  cvmd  26928  cvexch  26966  cdj1i  27025  cdj3lem1  27026  cdj3lem2b  27029  cdj3lem3b  27032  cdj3i  27033  isoun  27189  mul2lt0rlt0  27230  isomnd  27350  omndadd  27355  omndmul  27363  ogrpaddltbi  27368  ogrpinvlt  27373  isinftm  27384  archiabllem2b  27399  gsumle  27430  pstmxmet  27509  xrmulc1cn  27545  lmdvg  27568  nexple  27642  logblt  27659  faeval  27855  brfae  27857  sconpht  28311  snmlval  28413  lediv2aALT  28515  ntrivcvgtail  28608  faclim  28745  poseq  28907  sltval2  28990  sltres  28998  nodense  29023  nobndup  29034  nobnddown  29035  fvtransport  29256  idinside  29308  btwnconn1lem7  29317  btwnconn1lem11  29321  btwnconn1lem12  29322  heicant  29624  itg2addnclem  29641  itg2addnclem3  29643  itg2gt0cn  29645  ftc1anclem6  29670  ftc1anc  29673  ftc2nc  29674  dvasin  29678  areacirclem1  29682  nn0prpwlem  29715  seqpo  29841  incsequz  29842  metf1o  29849  mettrifi  29851  cntotbnd  29893  heiborlem4  29911  heiborlem6  29913  heiborlem10  29917  bfplem1  29919  bfplem2  29920  irrapxlem2  30361  irrapxlem4  30363  irrapxlem5  30364  irrapxlem6  30365  pellexlem3  30369  monotuz  30479  monotoddzzfi  30480  monotoddzz  30481  expmordi  30485  jm2.17a  30500  jm2.17b  30501  rmygeid  30504  rmydioph  30560  expdiophlem1  30567  expdiophlem2  30568  ttac  30582  fnwe2lem2  30601  monoords  31073  evthiccabs  31093  ioossioobi  31121  climinf  31148  climinff  31153  ltmod  31180  dvbdfbdioolem2  31259  ioodvbdlimc1lem1  31261  ioodvbdlimc1lem2  31262  ioodvbdlimc2lem  31264  iblspltprt  31291  itgspltprt  31297  stoweidlem3  31303  dirkercncflem4  31406  fourierdlem2  31409  fourierdlem3  31410  fourierdlem4  31411  fourierdlem6  31413  fourierdlem7  31414  fourierdlem11  31418  fourierdlem12  31419  fourierdlem14  31421  fourierdlem15  31422  fourierdlem19  31426  fourierdlem34  31441  fourierdlem35  31442  fourierdlem39  31446  fourierdlem41  31448  fourierdlem42  31449  fourierdlem45  31452  fourierdlem48  31455  fourierdlem49  31456  fourierdlem50  31457  fourierdlem51  31458  fourierdlem73  31480  fourierdlem76  31483  fourierdlem77  31484  fourierdlem79  31486  fourierdlem81  31488  fourierdlem83  31490  fourierdlem89  31496  fourierdlem90  31497  fourierdlem91  31498  fourierdlem92  31499  fourierdlem100  31507  fourierdlem107  31514  fourierdlem109  31516  fourierdlem111  31518  fourierdlem112  31519  fouriersw  31532  2elfz2melfz  31803  ismgmALT2  31973  iscmgmALT2  31974  issgrpALT2  31975  iscsgrpALT2  31976  lindslinindsimp2lem5  32136  isopos  33977  oplecon3b  33997  atlatle  34117  4at2  34410  pmaple  34557  islaut  34879  lautcnvle  34885  lautco  34893  ltrncnvel  34938  cdlemeg49lebilem  35335  cdlemg17h  35464  tendoset  35555  tendotp  35557  cdlemk39s  35735
  Copyright terms: Public domain W3C validator