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

Theorem breq12d 4436
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 4428 . 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 4423
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-rab 2780  df-v 3082  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3912  df-sn 3999  df-pr 4001  df-op 4005  df-br 4424
This theorem is referenced by:  breq123d  4437  3brtr3d  4453  3brtr4d  4454  sbcbr  4476  pocl  4781  csbcnvgALT  5038  cnvpo  5393  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  7654  xpsneng  7666  xpcomeng  7673  xpdom2g  7677  map2xp  7751  mapdom3  7753  limensuc  7758  infensuc  7759  unxpdom  7788  pssnn  7799  dif1en  7813  unfilem3  7846  unfi  7847  domunfican  7853  fodomfi  7859  marypha1lem  7956  wemaplem1  8070  wemaplem2  8071  wemapwe  8210  dif1card  8449  infxpenlem  8452  pwsdompw  8641  infmap2  8655  sornom  8714  isfin5  8736  isfin6  8737  domtriomlem  8879  axdc2lem  8885  axdclem2  8957  pwcfsdom  9015  cfpwsdom  9016  alephom  9017  fpwwe2lem7  9068  fpwwe2lem9  9070  pwxpndom2  9097  tskcard  9213  ordpipq  9374  adderpqlem  9386  mulerpqlem  9387  mulcanenq  9392  lterpq  9402  ltanq  9403  ltmnq  9404  ltaddnq  9406  ltrnq  9411  archnq  9412  reclem4pr  9482  ltasr  9531  sqgt0sr  9537  axpre-ltadd  9598  axpre-mulgt0  9599  ltadd1  10088  leadd2  10090  ltmul2  10463  lemul2  10465  lemul1a  10466  ltdiv1  10476  ltdiv2  10499  lediv2  10503  xleadd1  11548  xltadd2  11550  xsubge0  11554  xlemul1a  11581  xlemul1  11583  xlemul2  11584  xltmul2  11586  ltdifltdiv  12072  fzennn  12187  monoord  12249  monoord2  12250  ltexp2r  12335  leexp1a  12337  sqlecan  12387  bernneq  12404  faclbnd  12481  faclbnd3  12483  faclbnd4lem1  12484  faclbnd4lem2  12485  faclbnd4lem3  12486  faclbnd4lem4  12487  faclbnd6  12490  facubnd  12491  rlimcld2  13641  isercoll2  13731  climsup  13732  iseraltlem2  13748  fsumabs  13860  fsumrlim  13870  climcndslem1  13906  climcndslem2  13907  supcvg  13913  geomulcvg  13931  cvgrat  13938  ntrivcvgtail  13955  fprodle  14049  ruclem2  14283  ruclem8  14288  sadcaddlem  14430  sadcadd  14431  nn0seqcvgd  14528  algcvg  14534  algcvga  14537  eucalgcvga  14544  isprm5  14650  qnumgt0  14698  pcprendvds2  14790  pcpremul  14792  pcadd2  14834  prmreclem4  14862  prmreclem5  14863  prmreclem6  14864  2expltfac  15062  xpsle  15486  mreexexlemd  15549  issubc  15739  latjlej2  16311  latmlem2  16327  sylow1lem3  17251  isslw  17259  fislw  17276  efgi  17368  lt6abl  17528  ablfac1eu  17705  isabv  18046  abvtri  18057  cayleyhamilton1  19914  isucn  21291  ispsmet  21318  psmettri2  21323  ismet  21336  isxmet  21337  xmettri2  21353  imasdsf1olem  21386  imasf1oxmet  21388  blvalps  21398  blval  21399  comet  21526  stdbdxmet  21528  nrmmetd  21587  tngngp  21660  nmofval  21717  nmolb2d  21721  nmoi  21731  nmoix  21732  nmofvalOLD  21736  nmoiOLD  21747  nmoixOLD  21748  icopnfhmeo  21969  xrhmeo  21972  evth2  21986  pi1grplem  22078  minveclem6  22374  minveclem6OLD  22386  ovolfiniun  22452  ovoliunlem3  22455  voliunlem3  22503  ioombl1  22513  mbfmax  22603  mbfpos  22605  itg1climres  22670  mbfi1fseqlem2  22672  mbfi1fseqlem6  22676  mbfi1fseq  22677  mbfmullem  22681  itg2split  22705  itg2monolem1  22706  itg2monolem3  22708  itg2mono  22709  itg2i1fseqle  22710  itg2i1fseq  22711  itg2i1fseq2  22712  itg2addlem  22714  rolle  22940  dvlip  22943  c1lip1  22947  dvcnvrelem1  22967  dvcvx  22970  ply1divex  23085  q1pval  23102  fta1glem2  23115  fta1g  23116  fta1b  23118  plydivlem3  23246  fta1lem  23258  fta1  23259  aalioulem3  23288  aalioulem4  23289  aaliou3lem2  23297  aaliou3lem8  23299  aaliou3lem9  23304  ulmdvlem1  23353  ulmdvlem3  23355  abelthlem2  23385  abelthlem7a  23390  argrege0  23558  cxplt  23637  cxplea  23639  cxple2  23640  cxplt3  23643  logbleb  23718  logblt  23719  rlimcxp  23897  scvxcvx  23909  jensenlem2  23911  ftalem3  23997  ftalem7  24003  vmalelog  24131  chtub  24138  chpchtsum  24145  bclbnd  24206  efexple  24207  bposlem5  24214  bposlem6  24215  bposlem7  24216  lgsdilem  24248  dchrisumlem3  24327  dchrmusumlema  24329  dchrmusum2  24330  dchrvmasumlem2  24334  dchrvmasumlema  24336  dchrvmasumiflem1  24337  dchrisum0flblem2  24345  dchrisum0flb  24346  dchrisum0lema  24350  dchrisum0lem1b  24351  dchrisum0lem2  24354  pntrlog2bndlem2  24414  pntibndlem2  24427  pntlemf  24441  ostth2lem1  24454  qabvle  24461  legso  24642  iscgra  24849  isleag  24881  iseqlg  24895  brbtwn2  24933  axlowdim  24989  sizeusglecusg  25212  isrusgra  25653  extwwlkfablem2  25804  isnvlem  26227  nvtri  26297  nmlnoubi  26435  nmblolbii  26438  nmblolbi  26439  blocnilem  26443  sii  26493  ubthlem2  26511  minvecolem3  26516  minvecolem5  26521  minvecolem6  26522  minvecolem3OLD  26526  minvecolem5OLD  26531  minvecolem6OLD  26532  norm-ii  26789  norm3dif  26801  norm3adifi  26804  bcs  26832  pjnorm  27375  pjnel  27377  nmbdoplbi  27675  nmbdoplb  27676  nmcoplb  27681  lnconi  27684  nmbdfnlb  27701  nmcfnlb  27705  pjdifnormi  27818  mdslmd2i  27981  cvmd  27987  cvexch  28025  cdj1i  28084  cdj3lem1  28085  cdj3lem2b  28088  cdj3lem3b  28091  cdj3i  28092  isoun  28284  isomnd  28471  omndadd  28476  omndmul  28484  ogrpinvlt  28494  isinftm  28505  gsumle  28549  xrmulc1cn  28744  lmdvg  28767  nexple  28839  faeval  29077  brfae  29079  inelcarsg  29151  carsgsigalem  29155  carsgclctunlem2  29159  carsgclctun  29161  sconpht  29960  snmlval  30062  lediv2aALT  30329  faclim  30389  poseq  30498  sltval2  30550  sltres  30558  nodense  30583  nobndup  30594  nobnddown  30595  fvtransport  30804  idinside  30856  btwnconn1lem7  30865  btwnconn1lem11  30869  btwnconn1lem12  30870  nn0prpwlem  30983  poimirlem29  31933  heicant  31939  itg2addnclem  31957  itg2addnclem3  31959  itg2gt0cn  31961  ftc1anclem6  31986  ftc1anc  31989  ftc2nc  31990  dvasin  31992  areacirclem1  31996  seqpo  32040  incsequz  32041  metf1o  32048  mettrifi  32050  cntotbnd  32092  heiborlem4  32110  heiborlem6  32112  heiborlem10  32116  bfplem1  32118  bfplem2  32119  isopos  32715  oplecon3b  32735  atlatle  32855  4at2  33148  pmaple  33295  islaut  33617  lautcnvle  33623  lautco  33631  ltrncnvel  33676  cdlemeg49lebilem  34075  cdlemg17h  34204  tendoset  34295  tendotp  34297  cdlemk39s  34475  irrapxlem2  35637  irrapxlem4  35639  irrapxlem5  35640  irrapxlem6  35641  pellexlem3  35645  monotuz  35759  monotoddzzfi  35760  monotoddzz  35761  expmordi  35765  jm2.17a  35780  jm2.17b  35781  rmygeid  35784  rmydioph  35839  expdiophlem1  35846  expdiophlem2  35847  ttac  35861  fnwe2lem2  35879  relexp01min  36275  cvgdvgrat  36632  monoords  37468  supxrgelem  37514  supxrge  37515  evthiccabs  37542  climinf  37624  climinfOLD  37625  climinff  37630  climinffOLD  37631  ioodvbdlimc1lem1  37743  ioodvbdlimc1lem2  37744  ioodvbdlimc1lem1OLD  37745  ioodvbdlimc1lem2OLD  37746  ioodvbdlimc2lem  37748  ioodvbdlimc2lemOLD  37749  iblspltprt  37790  itgspltprt  37796  stoweidlem3  37803  fourierdlem2  37911  fourierdlem3  37912  fourierdlem11  37920  fourierdlem12  37921  fourierdlem15  37924  fourierdlem34  37944  fourierdlem41  37951  fourierdlem48  37958  fourierdlem49  37959  fourierdlem79  37989  fourierdlem83  37993  fourierdlem89  37999  fourierdlem91  38001  fourierdlem100  38010  fourierdlem107  38017  fourierdlem109  38019  fourierdlem112  38022  etransclem31  38070  etransclem32  38071  sge0less  38142  sge0le  38157  sge0split  38159  sge0lempt  38160  sge0iunmptlemre  38165  sge0isum  38177  isome  38223  omeunile  38234  omeiunlempt  38249  carageniuncllem2  38251  0ome  38258  isomenndlem  38259  isomennd  38260  ovnsslelem  38286  ovnssle  38287  ovnsubadd  38298  hsphoidmvle2  38311  hsphoidmvle  38312  hoidmvval0  38313  hoidmv1lelem1  38317  hoidmv1lelem2  38318  hoidmv1lelem3  38319  hoidmv1le  38320  hoidmvlelem1  38321  hoidmvlelem2  38322  hoidmvlelem3  38323  hoidmvlelem4  38324  hoidmvlelem5  38325  hoidmvle  38326  smonoord  38588  iccpart  38600  iccpartimp  38601  iccpartres  38602  2elfz2melfz  38912  ismgmALT  39478  iscmgmALT  39479  issgrpALT  39480  iscsgrpALT  39481  lindslinindsimp2lem5  39876  aacllem  40161
  Copyright terms: Public domain W3C validator