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

Theorem breq12d 4817
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 4809 . 2 ((𝐴 = 𝐵𝐶 = 𝐷) → (𝐴𝑅𝐶𝐵𝑅𝐷))
41, 2, 3syl2anc 696 1 (𝜑 → (𝐴𝑅𝐶𝐵𝑅𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196   = wceq 1632   class class class wbr 4804
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-rab 3059  df-v 3342  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-sn 4322  df-pr 4324  df-op 4328  df-br 4805
This theorem is referenced by:  breq123d  4818  3brtr3d  4835  3brtr4d  4836  sbcbr  4859  pocl  5194  csbcnvgALT  5462  cnvpo  5834  sbcfung  6073  isoeq1  6730  isocnv  6743  isotr  6749  caovordig  7004  caovordg  7006  caovord2d  7008  caovord  7010  ofrfval  7070  ofrval  7072  ofrfval2  7080  caofref  7088  fnwelem  7460  fundmeng  8196  xpsneng  8210  xpcomeng  8217  xpdom2g  8221  map2xp  8295  mapdom3  8297  limensuc  8302  infensuc  8303  unxpdom  8332  pssnn  8343  dif1en  8358  unfilem3  8391  unfi  8392  domunfican  8398  fodomfi  8404  marypha1lem  8504  wemaplem1  8616  wemaplem2  8617  wemapwe  8767  dif1card  9023  infxpenlem  9026  pwsdompw  9218  infmap2  9232  sornom  9291  isfin5  9313  isfin6  9314  domtriomlem  9456  axdc2lem  9462  axdclem2  9534  pwcfsdom  9597  cfpwsdom  9598  alephom  9599  fpwwe2lem7  9650  fpwwe2lem9  9652  pwxpndom2  9679  tskcard  9795  ordpipq  9956  adderpqlem  9968  mulerpqlem  9969  mulcanenq  9974  lterpq  9984  ltanq  9985  ltmnq  9986  ltaddnq  9988  ltrnq  9993  archnq  9994  reclem4pr  10064  ltasr  10113  sqgt0sr  10119  axpre-ltadd  10180  axpre-mulgt0  10181  ltadd1  10687  leadd2  10689  ltmul2  11066  lemul2  11068  lemul1a  11069  ltdiv1  11079  ltdiv2  11101  lediv2  11105  div4p1lem1div2  11479  nn0ledivnn  12134  xleadd1  12278  xltadd2  12280  xsubge0  12284  xlemul1a  12311  xlemul1  12313  xlemul2  12314  xltmul2  12316  ltdifltdiv  12829  fzennn  12961  monoord  13025  monoord2  13026  ltexp2r  13111  leexp1a  13113  sqlecan  13165  bernneq  13184  faclbnd  13271  faclbnd3  13273  faclbnd4lem1  13274  faclbnd4lem2  13275  faclbnd4lem3  13276  faclbnd4lem4  13277  faclbnd6  13280  facubnd  13281  rlimcld2  14508  isercoll2  14598  climsup  14599  iseraltlem2  14612  fsumabs  14732  fsumrlim  14742  climcndslem1  14780  climcndslem2  14781  supcvg  14787  geomulcvg  14806  cvgrat  14814  ntrivcvgtail  14831  fprodle  14926  ruclem2  15160  ruclem8  15165  addmodlteqALT  15249  fproddvdsd  15261  sadcaddlem  15381  sadcadd  15382  nn0seqcvgd  15485  algcvg  15491  algcvga  15494  eucalgcvga  15501  isprm5  15621  qnumgt0  15660  pcprendvds2  15748  pcpremul  15750  pcadd2  15796  prmreclem4  15825  prmreclem5  15826  prmreclem6  15827  2expltfac  16001  xpsle  16443  mreexexlemd  16506  issubc  16696  latjlej2  17267  latmlem2  17283  sylow1lem3  18215  isslw  18223  fislw  18240  efgi  18332  lt6abl  18496  ablfac1eu  18672  isabv  19021  abvtri  19032  cayleyhamilton1  20899  isucn  22283  ispsmet  22310  psmettri2  22315  ismet  22329  isxmet  22330  xmettri2  22346  imasdsf1olem  22379  imasf1oxmet  22381  blvalps  22391  blval  22392  comet  22519  stdbdxmet  22521  nrmmetd  22580  tngngp  22659  tngngp3  22661  nmofval  22719  nmolb2d  22723  nmoi  22733  nmoix  22734  icopnfhmeo  22943  xrhmeo  22946  evth2  22960  pi1grplem  23049  minveclem6  23405  ovolfiniun  23469  ovoliunlem3  23472  voliunlem3  23520  ioombl1  23530  mbfmax  23615  mbfpos  23617  itg1climres  23680  mbfi1fseqlem2  23682  mbfi1fseqlem6  23686  mbfi1fseq  23687  mbfmullem  23691  itg2split  23715  itg2monolem1  23716  itg2monolem3  23718  itg2mono  23719  itg2i1fseqle  23720  itg2i1fseq  23721  itg2i1fseq2  23722  itg2addlem  23724  rolle  23952  dvlip  23955  c1lip1  23959  dvcnvrelem1  23979  dvcvx  23982  ply1divex  24095  q1pval  24112  fta1glem2  24125  fta1g  24126  fta1b  24128  plydivlem3  24249  fta1lem  24261  fta1  24262  aalioulem3  24288  aalioulem4  24289  aaliou3lem2  24297  aaliou3lem8  24299  aaliou3lem9  24304  ulmdvlem1  24353  ulmdvlem3  24355  abelthlem2  24385  abelthlem7a  24390  argrege0  24556  cxplt  24639  cxplea  24641  cxple2  24642  cxplt3  24645  logbleb  24720  logblt  24721  rlimcxp  24899  scvxcvx  24911  jensenlem2  24913  ftalem3  25000  ftalem7  25004  vmalelog  25129  chtub  25136  chpchtsum  25143  bclbnd  25204  efexple  25205  bposlem5  25212  bposlem6  25213  bposlem7  25214  lgsdilem  25248  2lgslem1a2  25314  dchrisumlem3  25379  dchrmusumlema  25381  dchrmusum2  25382  dchrvmasumlem2  25386  dchrvmasumlema  25388  dchrvmasumiflem1  25389  dchrisum0flblem2  25397  dchrisum0flb  25398  dchrisum0lema  25402  dchrisum0lem1b  25403  dchrisum0lem2  25406  pntrlog2bndlem2  25466  pntibndlem2  25479  pntlemf  25493  ostth2lem1  25506  qabvle  25513  legso  25693  iscgra  25900  isleag  25932  iseqlg  25946  brbtwn2  25984  axlowdim  26040  ewlksfval  26707  isnvlem  27774  nvtri  27834  nmlnoubi  27960  nmblolbii  27963  nmblolbi  27964  blocnilem  27968  sii  28018  ubthlem2  28036  minvecolem3  28041  minvecolem5  28046  minvecolem6  28047  norm-ii  28304  norm3dif  28316  norm3adifi  28319  bcs  28347  pjnorm  28892  pjnel  28894  nmbdoplbi  29192  nmbdoplb  29193  nmcoplb  29198  lnconi  29201  nmbdfnlb  29218  nmcfnlb  29222  pjdifnormi  29335  mdslmd2i  29498  cvmd  29504  cvexch  29542  cdj1i  29601  cdj3lem1  29602  cdj3lem2b  29605  cdj3lem3b  29608  cdj3i  29609  isoun  29788  isomnd  30010  omndadd  30015  omndmul  30023  ogrpinvlt  30033  isinftm  30044  gsumle  30088  xrmulc1cn  30285  lmdvg  30308  nexple  30380  faeval  30618  brfae  30620  inelcarsg  30682  carsgsigalem  30686  carsgclctunlem2  30690  carsgclctun  30692  hgt750lemc  31034  hgt750lemd  31035  hgt749d  31036  sconnpht  31518  snmlval  31620  lediv2aALT  31878  faclim  31939  poseq  32059  sltval2  32115  sltres  32121  nolesgn2o  32130  nodense  32148  nolt02o  32151  noresle  32152  nosupbnd2lem1  32167  nosupbnd2  32168  fvtransport  32445  idinside  32497  btwnconn1lem7  32506  btwnconn1lem11  32510  btwnconn1lem12  32511  nn0prpwlem  32623  poimirlem29  33751  heicant  33757  itg2addnclem  33774  itg2addnclem3  33776  itg2gt0cn  33778  ftc1anclem6  33803  ftc1anc  33806  ftc2nc  33807  dvasin  33809  areacirclem1  33813  seqpo  33856  incsequz  33857  metf1o  33864  mettrifi  33866  cntotbnd  33908  heiborlem4  33926  heiborlem6  33928  heiborlem10  33932  bfplem1  33934  bfplem2  33935  isopos  34970  oplecon3b  34990  atlatle  35110  4at2  35403  pmaple  35550  islaut  35872  lautcnvle  35878  lautco  35886  ltrncnvel  35931  cdlemeg49lebilem  36329  cdlemg17h  36458  tendoset  36549  tendotp  36551  cdlemk39s  36729  irrapxlem2  37889  irrapxlem4  37891  irrapxlem5  37892  irrapxlem6  37893  pellexlem3  37897  monotuz  38008  monotoddzzfi  38009  monotoddzz  38010  expmordi  38014  jm2.17a  38029  jm2.17b  38030  rmygeid  38033  rmydioph  38083  expdiophlem1  38090  expdiophlem2  38091  ttac  38105  fnwe2lem2  38123  relexp01min  38507  cvgdvgrat  39014  monoords  40010  supxrgelem  40051  supxrge  40052  abslt2sqd  40074  ltmulneg  40113  ltdiv23neg  40115  monoordxrv  40210  monoordxr  40211  monoord2xrv  40212  monoord2xr  40213  evthiccabs  40221  sqrlearg  40283  climinf  40341  climinff  40346  limsupres  40440  climinf2  40442  climinf2mpt  40449  climinfmpt  40450  supcnvlimsup  40475  liminfval2  40503  liminflelimsuplem  40510  liminfltlem  40539  fprodsubrecnncnvlem  40624  fprodaddrecnncnvlem  40626  ioodvbdlimc1lem1  40649  ioodvbdlimc1lem2  40650  ioodvbdlimc2lem  40652  iblspltprt  40692  itgspltprt  40698  stoweidlem3  40723  fourierdlem2  40829  fourierdlem3  40830  fourierdlem11  40838  fourierdlem12  40839  fourierdlem15  40842  fourierdlem34  40861  fourierdlem41  40868  fourierdlem48  40874  fourierdlem49  40875  fourierdlem79  40905  fourierdlem83  40909  fourierdlem89  40915  fourierdlem91  40917  fourierdlem100  40926  fourierdlem107  40933  fourierdlem109  40935  fourierdlem112  40938  etransclem31  40985  etransclem32  40986  rrndistlt  41013  ioorrnopn  41028  ioorrnopnxrlem  41029  sge0less  41112  sge0le  41127  sge0split  41129  sge0lempt  41130  sge0iunmptlemre  41135  sge0isum  41147  sge0seq  41166  meaiuninclem  41200  meaiininclem  41206  meaiininc  41207  isome  41214  omeunile  41225  omeiunlempt  41240  carageniuncllem2  41242  0ome  41249  isomenndlem  41250  isomennd  41251  ovnsslelem  41280  ovnssle  41281  ovnsubadd  41292  hsphoidmvle2  41305  hsphoidmvle  41306  hoidmvval0  41307  hoidmv1lelem1  41311  hoidmv1lelem2  41312  hoidmv1lelem3  41313  hoidmv1le  41314  hoidmvlelem1  41315  hoidmvlelem2  41316  hoidmvlelem3  41317  hoidmvlelem4  41318  hoidmvlelem5  41319  hoidmvle  41320  hoidifhspdmvle  41340  hspmbllem2  41347  hspmbl  41349  ovnsubadd2lem  41365  ovolval4lem2  41370  ovolval4  41371  ovolval5lem2  41373  vonioolem2  41401  vonioo  41402  vonicclem2  41404  vonicc  41405  smfid  41467  smflimlem3  41487  2elfz2melfz  41838  smonoord  41851  iccpart  41862  iccpartimp  41863  iccpartres  41864  sqrtpwpw2p  41960  ismgmALT  42369  iscmgmALT  42370  issgrpALT  42371  iscsgrpALT  42372  lindslinindsimp2lem5  42761  aacllem  43060
  Copyright terms: Public domain W3C validator