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

Theorem breq12d 4408
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 4400 . 2  |-  ( ( A  =  B  /\  C  =  D )  ->  ( A R C  <-> 
B R D ) )
41, 2, 3syl2anc 673 1  |-  ( ph  ->  ( A R C  <-> 
B R D ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189    = wceq 1452   class class class wbr 4395
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451
This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3an 1009  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-rab 2765  df-v 3033  df-dif 3393  df-un 3395  df-in 3397  df-ss 3404  df-nul 3723  df-if 3873  df-sn 3960  df-pr 3962  df-op 3966  df-br 4396
This theorem is referenced by:  breq123d  4409  3brtr3d  4425  3brtr4d  4426  sbcbr  4448  pocl  4767  csbcnvgALT  5024  cnvpo  5381  sbcfung  5612  isoeq1  6228  isocnv  6239  isotr  6245  caovordig  6493  caovordg  6495  caovord2d  6497  caovord  6499  ofrfval  6558  ofrval  6560  ofrfval2  6568  caofref  6576  fnwelem  6930  fundmeng  7662  xpsneng  7675  xpcomeng  7682  xpdom2g  7686  map2xp  7760  mapdom3  7762  limensuc  7767  infensuc  7768  unxpdom  7797  pssnn  7808  dif1en  7822  unfilem3  7855  unfi  7856  domunfican  7862  fodomfi  7868  marypha1lem  7965  wemaplem1  8079  wemaplem2  8080  wemapwe  8220  dif1card  8459  infxpenlem  8462  pwsdompw  8652  infmap2  8666  sornom  8725  isfin5  8747  isfin6  8748  domtriomlem  8890  axdc2lem  8896  axdclem2  8968  pwcfsdom  9026  cfpwsdom  9027  alephom  9028  fpwwe2lem7  9079  fpwwe2lem9  9081  pwxpndom2  9108  tskcard  9224  ordpipq  9385  adderpqlem  9397  mulerpqlem  9398  mulcanenq  9403  lterpq  9413  ltanq  9414  ltmnq  9415  ltaddnq  9417  ltrnq  9422  archnq  9423  reclem4pr  9493  ltasr  9542  sqgt0sr  9548  axpre-ltadd  9609  axpre-mulgt0  9610  ltadd1  10102  leadd2  10104  ltmul2  10478  lemul2  10480  lemul1a  10481  ltdiv1  10491  ltdiv2  10514  lediv2  10518  xleadd1  11566  xltadd2  11568  xsubge0  11572  xlemul1a  11599  xlemul1  11601  xlemul2  11602  xltmul2  11604  ltdifltdiv  12099  fzennn  12219  monoord  12281  monoord2  12282  ltexp2r  12367  leexp1a  12369  sqlecan  12419  bernneq  12436  faclbnd  12513  faclbnd3  12515  faclbnd4lem1  12516  faclbnd4lem2  12517  faclbnd4lem3  12518  faclbnd4lem4  12519  faclbnd6  12522  facubnd  12523  rlimcld2  13719  isercoll2  13809  climsup  13810  iseraltlem2  13826  fsumabs  13938  fsumrlim  13948  climcndslem1  13984  climcndslem2  13985  supcvg  13991  geomulcvg  14009  cvgrat  14016  ntrivcvgtail  14033  fprodle  14127  ruclem2  14361  ruclem8  14366  addmodlteqALT  14437  sadcaddlem  14510  sadcadd  14511  nn0seqcvgd  14608  algcvg  14614  algcvga  14617  eucalgcvga  14624  isprm5  14730  qnumgt0  14778  pcprendvds2  14870  pcpremul  14872  pcadd2  14914  prmreclem4  14942  prmreclem5  14943  prmreclem6  14944  2expltfac  15141  xpsle  15565  mreexexlemd  15628  issubc  15818  latjlej2  16390  latmlem2  16406  sylow1lem3  17330  isslw  17338  fislw  17355  efgi  17447  lt6abl  17607  ablfac1eu  17784  isabv  18125  abvtri  18136  cayleyhamilton1  19993  isucn  21371  ispsmet  21398  psmettri2  21403  ismet  21416  isxmet  21417  xmettri2  21433  imasdsf1olem  21466  imasf1oxmet  21468  blvalps  21478  blval  21479  comet  21606  stdbdxmet  21608  nrmmetd  21667  tngngp  21740  nmofval  21797  nmolb2d  21801  nmoi  21811  nmoix  21812  nmofvalOLD  21816  nmoiOLD  21827  nmoixOLD  21828  icopnfhmeo  22049  xrhmeo  22052  evth2  22066  pi1grplem  22158  minveclem6  22454  minveclem6OLD  22466  ovolfiniun  22532  ovoliunlem3  22535  voliunlem3  22584  ioombl1  22594  mbfmax  22684  mbfpos  22686  itg1climres  22751  mbfi1fseqlem2  22753  mbfi1fseqlem6  22757  mbfi1fseq  22758  mbfmullem  22762  itg2split  22786  itg2monolem1  22787  itg2monolem3  22789  itg2mono  22790  itg2i1fseqle  22791  itg2i1fseq  22792  itg2i1fseq2  22793  itg2addlem  22795  rolle  23021  dvlip  23024  c1lip1  23028  dvcnvrelem1  23048  dvcvx  23051  ply1divex  23166  q1pval  23183  fta1glem2  23196  fta1g  23197  fta1b  23199  plydivlem3  23327  fta1lem  23339  fta1  23340  aalioulem3  23369  aalioulem4  23370  aaliou3lem2  23378  aaliou3lem8  23380  aaliou3lem9  23385  ulmdvlem1  23434  ulmdvlem3  23436  abelthlem2  23466  abelthlem7a  23471  argrege0  23639  cxplt  23718  cxplea  23720  cxple2  23721  cxplt3  23724  logbleb  23799  logblt  23800  rlimcxp  23978  scvxcvx  23990  jensenlem2  23992  ftalem3  24078  ftalem7  24084  vmalelog  24212  chtub  24219  chpchtsum  24226  bclbnd  24287  efexple  24288  bposlem5  24295  bposlem6  24296  bposlem7  24297  lgsdilem  24329  dchrisumlem3  24408  dchrmusumlema  24410  dchrmusum2  24411  dchrvmasumlem2  24415  dchrvmasumlema  24417  dchrvmasumiflem1  24418  dchrisum0flblem2  24426  dchrisum0flb  24427  dchrisum0lema  24431  dchrisum0lem1b  24432  dchrisum0lem2  24435  pntrlog2bndlem2  24495  pntibndlem2  24508  pntlemf  24522  ostth2lem1  24535  qabvle  24542  legso  24723  iscgra  24930  isleag  24962  iseqlg  24976  brbtwn2  25014  axlowdim  25070  sizeusglecusg  25293  isrusgra  25734  extwwlkfablem2  25885  isnvlem  26310  nvtri  26380  nmlnoubi  26518  nmblolbii  26521  nmblolbi  26522  blocnilem  26526  sii  26576  ubthlem2  26594  minvecolem3  26599  minvecolem5  26604  minvecolem6  26605  minvecolem3OLD  26609  minvecolem5OLD  26614  minvecolem6OLD  26615  norm-ii  26872  norm3dif  26884  norm3adifi  26887  bcs  26915  pjnorm  27458  pjnel  27460  nmbdoplbi  27758  nmbdoplb  27759  nmcoplb  27764  lnconi  27767  nmbdfnlb  27784  nmcfnlb  27788  pjdifnormi  27901  mdslmd2i  28064  cvmd  28070  cvexch  28108  cdj1i  28167  cdj3lem1  28168  cdj3lem2b  28171  cdj3lem3b  28174  cdj3i  28175  isoun  28357  isomnd  28538  omndadd  28543  omndmul  28551  ogrpinvlt  28561  isinftm  28572  gsumle  28616  xrmulc1cn  28810  lmdvg  28833  nexple  28905  faeval  29142  brfae  29144  inelcarsg  29216  carsgsigalem  29220  carsgclctunlem2  29224  carsgclctun  29226  sconpht  30024  snmlval  30126  lediv2aALT  30393  faclim  30453  poseq  30562  sltval2  30614  sltres  30622  nodense  30649  nobndup  30660  nobnddown  30661  fvtransport  30870  idinside  30922  btwnconn1lem7  30931  btwnconn1lem11  30935  btwnconn1lem12  30936  nn0prpwlem  31049  poimirlem29  32033  heicant  32039  itg2addnclem  32057  itg2addnclem3  32059  itg2gt0cn  32061  ftc1anclem6  32086  ftc1anc  32089  ftc2nc  32090  dvasin  32092  areacirclem1  32096  seqpo  32140  incsequz  32141  metf1o  32148  mettrifi  32150  cntotbnd  32192  heiborlem4  32210  heiborlem6  32212  heiborlem10  32216  bfplem1  32218  bfplem2  32219  isopos  32817  oplecon3b  32837  atlatle  32957  4at2  33250  pmaple  33397  islaut  33719  lautcnvle  33725  lautco  33733  ltrncnvel  33778  cdlemeg49lebilem  34177  cdlemg17h  34306  tendoset  34397  tendotp  34399  cdlemk39s  34577  irrapxlem2  35738  irrapxlem4  35740  irrapxlem5  35741  irrapxlem6  35742  pellexlem3  35746  monotuz  35860  monotoddzzfi  35861  monotoddzz  35862  expmordi  35866  jm2.17a  35881  jm2.17b  35882  rmygeid  35885  rmydioph  35940  expdiophlem1  35947  expdiophlem2  35948  ttac  35962  fnwe2lem2  35980  relexp01min  36376  cvgdvgrat  36732  monoords  37602  supxrgelem  37647  supxrge  37648  abslt2sqd  37670  evthiccabs  37689  climinf  37781  climinfOLD  37782  climinff  37787  climinffOLD  37788  ioodvbdlimc1lem1  37900  ioodvbdlimc1lem2  37901  ioodvbdlimc1lem1OLD  37902  ioodvbdlimc1lem2OLD  37903  ioodvbdlimc2lem  37905  ioodvbdlimc2lemOLD  37906  iblspltprt  37947  itgspltprt  37953  stoweidlem3  37975  fourierdlem2  38083  fourierdlem3  38084  fourierdlem11  38092  fourierdlem12  38093  fourierdlem15  38096  fourierdlem34  38116  fourierdlem41  38123  fourierdlem48  38130  fourierdlem49  38131  fourierdlem79  38161  fourierdlem83  38165  fourierdlem89  38171  fourierdlem91  38173  fourierdlem100  38182  fourierdlem107  38189  fourierdlem109  38191  fourierdlem112  38194  etransclem31  38242  etransclem32  38243  rrndistlt  38271  sge0less  38348  sge0le  38363  sge0split  38365  sge0lempt  38366  sge0iunmptlemre  38371  sge0isum  38383  sge0seq  38402  isome  38434  omeunile  38445  omeiunlempt  38460  carageniuncllem2  38462  0ome  38469  isomenndlem  38470  isomennd  38471  ovnsslelem  38500  ovnssle  38501  ovnsubadd  38512  hsphoidmvle2  38525  hsphoidmvle  38526  hoidmvval0  38527  hoidmv1lelem1  38531  hoidmv1lelem2  38532  hoidmv1lelem3  38533  hoidmv1le  38534  hoidmvlelem1  38535  hoidmvlelem2  38536  hoidmvlelem3  38537  hoidmvlelem4  38538  hoidmvlelem5  38539  hoidmvle  38540  hoidifhspdmvle  38560  hspmbllem2  38567  hspmbl  38569  ovnsubadd2lem  38585  ovolval4lem2  38590  ovolval4  38591  ovolval5lem2  38593  smonoord  38863  iccpart  38875  iccpartimp  38876  iccpartres  38877  2elfz2melfz  39203  ewlksfval  39807  ismgmALT  40367  iscmgmALT  40368  issgrpALT  40369  iscsgrpALT  40370  lindslinindsimp2lem5  40763  aacllem  41046
  Copyright terms: Public domain W3C validator