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

Theorem breq12d 4439
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 4431 . 2  |-  ( ( A  =  B  /\  C  =  D )  ->  ( A R C  <-> 
B R D ) )
41, 2, 3syl2anc 665 1  |-  ( ph  ->  ( A R C  <-> 
B R D ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187    = wceq 1437   class class class wbr 4426
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-rab 2791  df-v 3089  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-nul 3768  df-if 3916  df-sn 4003  df-pr 4005  df-op 4009  df-br 4427
This theorem is referenced by:  breq123d  4440  3brtr3d  4455  3brtr4d  4456  sbcbr  4478  pocl  4782  csbcnvgALT  5039  cnvpo  5394  sbcfung  5624  isoeq1  6225  isocnv  6236  isotr  6242  caovordig  6488  caovordg  6490  caovord2d  6492  caovord  6494  ofrfval  6553  ofrval  6555  ofrfval2  6563  caofref  6571  fnwelem  6922  fundmeng  7651  xpsneng  7663  xpcomeng  7670  xpdom2g  7674  map2xp  7748  mapdom3  7750  limensuc  7755  infensuc  7756  unxpdom  7785  pssnn  7796  dif1en  7810  unfilem3  7843  unfi  7844  domunfican  7850  fodomfi  7856  marypha1lem  7953  wemaplem1  8061  wemaplem2  8062  wemapwe  8201  dif1card  8440  infxpenlem  8443  pwsdompw  8632  infmap2  8646  sornom  8705  isfin5  8727  isfin6  8728  domtriomlem  8870  axdc2lem  8876  axdclem2  8948  pwcfsdom  9006  cfpwsdom  9007  alephom  9008  fpwwe2lem7  9060  fpwwe2lem9  9062  pwxpndom2  9089  tskcard  9205  ordpipq  9366  adderpqlem  9378  mulerpqlem  9379  mulcanenq  9384  lterpq  9394  ltanq  9395  ltmnq  9396  ltaddnq  9398  ltrnq  9403  archnq  9404  reclem4pr  9474  ltasr  9523  sqgt0sr  9529  axpre-ltadd  9590  axpre-mulgt0  9591  ltadd1  10080  leadd2  10082  ltmul2  10455  lemul2  10457  lemul1a  10458  ltdiv1  10468  ltdiv2  10491  lediv2  10496  xleadd1  11541  xltadd2  11543  xsubge0  11547  xlemul1a  11574  xlemul1  11576  xlemul2  11577  xltmul2  11579  ltdifltdiv  12063  fzennn  12178  monoord  12240  monoord2  12241  ltexp2r  12326  leexp1a  12328  sqlecan  12378  bernneq  12395  faclbnd  12472  faclbnd3  12474  faclbnd4lem1  12475  faclbnd4lem2  12476  faclbnd4lem3  12477  faclbnd4lem4  12478  faclbnd6  12481  facubnd  12482  rlimcld2  13620  isercoll2  13710  climsup  13711  iseraltlem2  13727  fsumabs  13839  fsumrlim  13849  climcndslem1  13885  climcndslem2  13886  supcvg  13892  geomulcvg  13910  cvgrat  13917  ntrivcvgtail  13934  fprodle  14028  ruclem2  14262  ruclem8  14267  sadcaddlem  14405  sadcadd  14406  nn0seqcvgd  14500  algcvg  14506  algcvga  14509  eucalgcvga  14516  isprm5  14613  qnumgt0  14661  pcprendvds2  14745  pcpremul  14747  pcadd2  14789  prmreclem4  14817  prmreclem5  14818  prmreclem6  14819  2expltfac  15017  xpsle  15429  mreexexlemd  15492  issubc  15682  latjlej2  16254  latmlem2  16270  sylow1lem3  17178  isslw  17186  fislw  17203  efgi  17295  lt6abl  17455  ablfac1eu  17632  isabv  17973  abvtri  17984  cayleyhamilton1  19838  isucn  21215  ispsmet  21242  psmettri2  21247  ismet  21260  isxmet  21261  xmettri2  21277  imasdsf1olem  21310  imasf1oxmet  21312  blvalps  21322  blval  21323  comet  21450  stdbdxmet  21452  nrmmetd  21511  tngngp  21584  nmofval  21637  nmolb2d  21641  nmoi  21651  nmoix  21652  icopnfhmeo  21858  xrhmeo  21861  evth2  21875  pi1grplem  21964  minveclem6  22260  ovolfiniun  22323  ovoliunlem3  22326  voliunlem3  22373  ioombl1  22383  mbfmax  22473  mbfpos  22475  itg1climres  22540  mbfi1fseqlem2  22542  mbfi1fseqlem6  22546  mbfi1fseq  22547  mbfmullem  22551  itg2split  22575  itg2monolem1  22576  itg2monolem3  22578  itg2mono  22579  itg2i1fseqle  22580  itg2i1fseq  22581  itg2i1fseq2  22582  itg2addlem  22584  rolle  22810  dvlip  22813  c1lip1  22817  dvcnvrelem1  22837  dvcvx  22840  ply1divex  22953  q1pval  22970  fta1glem2  22983  fta1g  22984  fta1b  22986  plydivlem3  23107  fta1lem  23119  fta1  23120  aalioulem3  23146  aalioulem4  23147  aaliou3lem2  23155  aaliou3lem8  23157  aaliou3lem9  23162  ulmdvlem1  23211  ulmdvlem3  23213  abelthlem2  23243  abelthlem7a  23248  argrege0  23416  cxplt  23495  cxplea  23497  cxple2  23498  cxplt3  23501  logbleb  23576  logblt  23577  rlimcxp  23755  scvxcvx  23767  jensenlem2  23769  ftalem3  23855  ftalem7  23859  vmalelog  23987  chtub  23994  chpchtsum  24001  bclbnd  24062  efexple  24063  bposlem5  24070  bposlem6  24071  bposlem7  24072  lgsdilem  24104  dchrisumlem3  24183  dchrmusumlema  24185  dchrmusum2  24186  dchrvmasumlem2  24190  dchrvmasumlema  24192  dchrvmasumiflem1  24193  dchrisum0flblem2  24201  dchrisum0flb  24202  dchrisum0lema  24206  dchrisum0lem1b  24207  dchrisum0lem2  24210  pntrlog2bndlem2  24270  pntibndlem2  24283  pntlemf  24297  ostth2lem1  24310  qabvle  24317  legso  24495  iscgra  24698  brbtwn2  24772  axlowdim  24828  sizeusglecusg  25050  isrusgra  25491  extwwlkfablem2  25642  isnvlem  26065  nvtri  26135  nmlnoubi  26273  nmblolbii  26276  nmblolbi  26277  blocnilem  26281  sii  26331  ubthlem2  26349  minvecolem3  26354  minvecolem5  26359  minvecolem6  26360  norm-ii  26617  norm3dif  26629  norm3adifi  26632  bcs  26660  pjnorm  27203  pjnel  27205  nmbdoplbi  27503  nmbdoplb  27504  nmcoplb  27509  lnconi  27512  nmbdfnlb  27529  nmcfnlb  27533  pjdifnormi  27646  mdslmd2i  27809  cvmd  27815  cvexch  27853  cdj1i  27912  cdj3lem1  27913  cdj3lem2b  27916  cdj3lem3b  27919  cdj3i  27920  isoun  28113  isomnd  28293  omndadd  28298  omndmul  28306  ogrpinvlt  28316  isinftm  28327  gsumle  28371  xrmulc1cn  28566  lmdvg  28589  nexple  28661  faeval  28899  brfae  28901  inelcarsg  28963  carsgsigalem  28967  carsgclctunlem2  28971  carsgclctun  28973  sconpht  29731  snmlval  29833  lediv2aALT  30100  faclim  30160  poseq  30269  sltval2  30321  sltres  30329  nodense  30354  nobndup  30365  nobnddown  30366  fvtransport  30575  idinside  30627  btwnconn1lem7  30636  btwnconn1lem11  30640  btwnconn1lem12  30641  nn0prpwlem  30754  poimirlem29  31663  heicant  31669  itg2addnclem  31687  itg2addnclem3  31689  itg2gt0cn  31691  ftc1anclem6  31716  ftc1anc  31719  ftc2nc  31720  dvasin  31722  areacirclem1  31726  seqpo  31770  incsequz  31771  metf1o  31778  mettrifi  31780  cntotbnd  31822  heiborlem4  31840  heiborlem6  31842  heiborlem10  31846  bfplem1  31848  bfplem2  31849  isopos  32445  oplecon3b  32465  atlatle  32585  4at2  32878  pmaple  33025  islaut  33347  lautcnvle  33353  lautco  33361  ltrncnvel  33406  cdlemeg49lebilem  33805  cdlemg17h  33934  tendoset  34025  tendotp  34027  cdlemk39s  34205  irrapxlem2  35367  irrapxlem4  35369  irrapxlem5  35370  irrapxlem6  35371  pellexlem3  35375  monotuz  35485  monotoddzzfi  35486  monotoddzz  35487  expmordi  35491  jm2.17a  35506  jm2.17b  35507  rmygeid  35510  rmydioph  35565  expdiophlem1  35572  expdiophlem2  35573  ttac  35587  fnwe2lem2  35605  relexp01min  35934  cvgdvgrat  36289  monoords  37113  supxrgelem  37159  supxrge  37160  evthiccabs  37168  climinf  37246  climinfOLD  37247  climinff  37252  climinffOLD  37253  ioodvbdlimc1lem1  37365  ioodvbdlimc1lem2  37366  ioodvbdlimc2lem  37368  iblspltprt  37409  itgspltprt  37415  stoweidlem3  37422  fourierdlem2  37530  fourierdlem3  37531  fourierdlem11  37539  fourierdlem12  37540  fourierdlem15  37543  fourierdlem34  37562  fourierdlem41  37569  fourierdlem48  37576  fourierdlem49  37577  fourierdlem79  37607  fourierdlem83  37611  fourierdlem89  37617  fourierdlem91  37619  fourierdlem100  37628  fourierdlem107  37635  fourierdlem109  37637  fourierdlem112  37640  etransclem31  37687  etransclem32  37688  sge0less  37758  sge0le  37773  sge0split  37775  sge0lempt  37776  sge0iunmptlemre  37781  isome  37814  omeunile  37825  omeiunlempt  37840  carageniuncllem2  37842  smonoord  38098  iccpart  38110  iccpartimp  38111  iccpartres  38112  2elfz2melfz  38397  ismgmALT  38607  iscmgmALT  38608  issgrpALT  38609  iscsgrpALT  38610  lindslinindsimp2lem5  39005  aacllem  39291
  Copyright terms: Public domain W3C validator