Theorem breq12d 5160

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

Step	Hyp	Ref	Expression
1		breq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		breq12d.2	. 2 ⊢ (𝜑 → 𝐶 = 𝐷)
3		breq12 5152	. 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐷))
4	1, 2, 3	syl2anc 584	1 ⊢ (𝜑 → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐷))

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1536   class class class wbr 5147

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-br 5148

This theorem is referenced by:  breq123d  5161  3brtr3d  5178  3brtr4d  5179  sbcbr  5202  pocl  5604  csbcnvgALT  5897  cnvpo  6308  sbcfung  6591  isoeq1  7336  isocnv  7349  isotr  7355  caovordig  7637  caovordg  7639  caovord2d  7641  caovord  7643  ofrfvalg  7704  ofrval  7708  ofrfval2  7717  caofref  7727  fnwelem  8154  poseq  8181  fundmeng  9070  enrefnn  9085  xpsneng  9094  xpcomeng  9102  xpdom2g  9106  limensuc  9192  infensuc  9193  pssnn  9206  unxpdom  9286  dif1ennnALT  9308  unfilem3  9342  fodomfi  9347  domunfican  9358  fodomfiOLD  9367  marypha1lem  9470  infsupprpr  9541  wemaplem1  9583  wemaplem2  9584  wemapwe  9734  ssttrcl  9752  ttrcltr  9753  ttrclss  9757  dmttrcl  9758  rnttrcl  9759  ttrclselem2  9763  dif1card  10047  infxpenlem  10050  nnadju  10235  pwsdompw  10240  infmap2  10254  sornom  10314  isfin5  10336  isfin6  10337  domtriomlem  10479  axdc2lem  10485  axdclem2  10557  pwcfsdom  10620  cfpwsdom  10621  alephom  10622  fpwwe2lem6  10673  fpwwe2lem8  10675  tskcard  10818  ordpipq  10979  adderpqlem  10991  mulerpqlem  10992  mulcanenq  10997  lterpq  11007  ltanq  11008  ltmnq  11009  ltaddnq  11011  ltrnq  11016  archnq  11017  reclem4pr  11087  ltasr  11137  sqgt0sr  11143  axpre-ltadd  11204  axpre-mulgt0  11205  ltadd1  11727  leadd2  11729  ltmul2  12115  lemul2  12117  lemul1a  12118  ltdiv1  12129  ltdiv2  12151  lediv2  12155  div4p1lem1div2  12518  nn0ledivnn  13145  xleadd1  13293  xltadd2  13295  xsubge0  13299  xlemul1a  13326  xlemul1  13328  xlemul2  13329  xltmul2  13331  ltdifltdiv  13870  fzennn  14005  monoord  14069  monoord2  14070  expmordi  14203  ltexp2r  14209  leexp1a  14211  sqlecan  14244  bernneq  14264  faclbnd  14325  faclbnd3  14327  faclbnd4lem1  14328  faclbnd4lem2  14329  faclbnd4lem3  14330  faclbnd4lem4  14331  faclbnd6  14334  facubnd  14335  rlimcld2  15610  isercoll2  15701  climsup  15702  iseraltlem2  15715  fsumabs  15833  fsumrlim  15843  climcndslem1  15881  climcndslem2  15882  supcvg  15888  geomulcvg  15908  cvgrat  15915  ntrivcvgtail  15932  ruclem2  16264  ruclem8  16269  addmodlteqALT  16358  fproddvdsd  16368  sadcaddlem  16490  sadcadd  16491  nn0seqcvgd  16603  algcvg  16609  algcvga  16612  eucalgcvga  16619  isprm5  16740  qnumgt0  16783  pcprendvds2  16874  pcpremul  16876  pcadd2  16923  prmreclem4  16952  prmreclem5  16953  prmreclem6  16954  2expltfac  17126  xpsle  17625  mreexexlemd  17688  issubc  17885  latjlej2  18511  latmlem2  18527  sylow1lem3  19632  isslw  19640  fislw  19657  efgi  19751  lt6abl  19927  ablfac1eu  20107  isabv  20828  abvtri  20839  psdmul  22187  cayleyhamilton1  22913  isucn  24302  ispsmet  24329  psmettri2  24334  ismet  24348  isxmet  24349  xmettri2  24365  imasdsf1olem  24398  imasf1oxmet  24400  blvalps  24410  blval  24411  comet  24541  stdbdxmet  24543  nrmmetd  24602  tngngp  24690  tngngp3  24692  nmofval  24750  nmolb2d  24754  nmoi  24764  nmoix  24765  icopnfhmeo  24987  xrhmeo  24990  evth2  25005  pi1grplem  25095  minveclem6  25481  ovolfiniun  25549  ovoliunlem3  25552  voliunlem3  25600  ioombl1  25610  mbfmax  25697  mbfpos  25699  itg1climres  25763  mbfi1fseqlem2  25765  mbfi1fseqlem6  25769  mbfi1fseq  25770  mbfmullem  25774  itg2split  25798  itg2monolem1  25799  itg2monolem3  25801  itg2mono  25802  itg2i1fseqle  25803  itg2i1fseq  25804  itg2i1fseq2  25805  itg2addlem  25807  rolle  26042  dvlip  26046  c1lip1  26050  dvcnvrelem1  26070  dvcvx  26073  ply1divex  26190  q1pval  26208  fta1glem2  26222  fta1g  26223  fta1b  26225  plydivlem3  26351  fta1lem  26363  fta1  26364  aalioulem3  26390  aalioulem4  26391  aaliou3lem2  26399  aaliou3lem8  26401  aaliou3lem9  26406  ulmdvlem1  26457  ulmdvlem3  26459  abelthlem2  26490  abelthlem7a  26495  argrege0  26667  cxplt  26750  cxplea  26752  cxple2  26753  cxplt3  26756  logbleb  26840  logblt  26841  rlimcxp  27031  scvxcvx  27043  jensenlem2  27045  ftalem3  27132  ftalem7  27136  vmalelog  27263  chtub  27270  chpchtsum  27277  bclbnd  27338  efexple  27339  bposlem5  27346  bposlem6  27347  bposlem7  27348  lgsdilem  27382  2lgslem1a2  27448  2sqreuop  27520  2sqreuopnn  27521  2sqreuoplt  27522  2sqreuopltb  27523  2sqreuopnnlt  27524  2sqreuopnnltb  27525  dchrisumlem3  27549  dchrmusumlema  27551  dchrmusum2  27552  dchrvmasumlem2  27556  dchrvmasumlema  27558  dchrvmasumiflem1  27559  dchrisum0flblem2  27567  dchrisum0flb  27568  dchrisum0lema  27572  dchrisum0lem1b  27573  dchrisum0lem2  27576  pntrlog2bndlem2  27636  pntibndlem2  27649  pntlemf  27663  ostth2lem1  27676  qabvle  27683  sltval2  27715  sltres  27721  nolesgn2o  27730  nogesgn1o  27732  nodense  27751  nolt02o  27754  nogt01o  27755  noresle  27756  nosupbnd2lem1  27774  nosupbnd2  27775  noinfbnd2lem1  27789  noinfbnd2  27790  addsproplem1  28016  addsprop  28023  sltadd2im  28033  sleadd2im  28035  sleadd1  28036  sleadd2  28037  sltadd1  28039  sltsub1  28120  sltsub2  28121  sltsubsubbd  28127  sltsubsub2bd  28128  posdifsd  28141  subsge0d  28143  mulsproplemcbv  28155  mulsproplem1  28156  mulsprop  28170  slemuld  28178  sltmul1d  28213  sltmulneg1d  28216  sltmulneg2d  28217  slemul1ad  28222  legso  28621  iscgra  28831  isleag  28869  iseqlg  28889  brbtwn2  28934  axlowdim  28990  ewlksfval  29633  isnvlem  30638  nvtri  30698  nmlnoubi  30824  nmblolbii  30827  nmblolbi  30828  blocnilem  30832  sii  30882  ubthlem2  30899  minvecolem3  30904  minvecolem5  30909  minvecolem6  30910  norm-ii  31166  norm3dif  31178  norm3adifi  31181  bcs  31209  pjnorm  31752  pjnel  31754  nmbdoplbi  32052  nmbdoplb  32053  nmcoplb  32058  lnconi  32061  nmbdfnlb  32078  nmcfnlb  32082  pjdifnormi  32195  mdslmd2i  32358  cvmd  32364  cvexch  32402  cdj1i  32461  cdj3lem1  32462  cdj3lem2b  32465  cdj3lem3b  32468  cdj3i  32469  isoun  32716  ismnt  32957  mgcmntco  32968  dfmgc2lem  32969  dfmgc2  32970  mgcf1o  32977  ischn  32980  chnltm1  32982  chnind  32984  chnub  32985  isomnd  33060  omndadd  33065  omndmul  33073  ogrpinvlt  33082  gsumle  33083  isinftm  33170  rlocaddval  33254  rlocmulval  33255  fldext2chn  33733  xrmulc1cn  33890  lmdvg  33913  nexple  33989  faeval  34226  brfae  34228  inelcarsg  34292  carsgsigalem  34296  carsgclctunlem2  34300  carsgclctun  34302  hgt750lemc  34640  hgt750lemd  34641  hgt749d  34642  sconnpht  35213  snmlval  35315  satfv1lem  35346  satfv1  35347  satfv0fun  35355  satfv0fvfmla0  35397  lediv2aALT  35661  faclim  35725  fvtransport  36013  idinside  36065  btwnconn1lem7  36074  btwnconn1lem11  36078  btwnconn1lem12  36079  ditgeq123dv  36203  cbvditgdavw2  36280  nn0prpwlem  36304  weiunlem1  36444  weiunfrlem  36446  bj-opabco  37170  poimirlem29  37635  heicant  37641  itg2addnclem  37657  itg2addnclem3  37659  itg2gt0cn  37661  ftc1anclem6  37684  ftc1anc  37687  ftc2nc  37688  dvasin  37690  areacirclem1  37694  seqpo  37733  incsequz  37734  metf1o  37741  mettrifi  37743  cntotbnd  37782  heiborlem4  37800  heiborlem6  37802  heiborlem10  37806  bfplem1  37808  bfplem2  37809  isopos  39161  oplecon3b  39181  atlatle  39301  4at2  39596  pmaple  39743  islaut  40065  lautcnvle  40071  lautco  40079  ltrncnvel  40124  cdlemeg49lebilem  40521  cdlemg17h  40650  tendoset  40741  tendotp  40743  cdlemk39s  40921  lcmineqlem23  42032  lcmineqlem  42033  intlewftc  42042  aks4d1p1p4  42052  dvle2  42053  aks4d1p8d2  42066  aks4d1p9  42069  aks4d1  42070  2ap1caineq  42126  sticksstones1  42127  sticksstones2  42128  sticksstones3  42129  sticksstones8  42134  sticksstones10  42136  sticksstones11  42137  sticksstones12a  42138  sticksstones15  42142  aks6d1c7lem3  42163  unitscyglem1  42176  factwoffsmonot  42223  brif12  42242  dvdsexpnn0  42347  dvdsexpb  42348  reltsub1  42392  irrapxlem2  42810  irrapxlem4  42812  irrapxlem5  42813  irrapxlem6  42814  pellexlem3  42818  monotuz  42929  monotoddzzfi  42930  monotoddzz  42931  jm2.17a  42948  jm2.17b  42949  rmygeid  42952  rmydioph  43002  expdiophlem1  43009  expdiophlem2  43010  ttac  43024  fnwe2lem2  43039  relexp01min  43702  cvgdvgrat  44308  monoords  45247  supxrgelem  45286  supxrge  45287  abslt2sqd  45309  ltmulneg  45341  ltdiv23neg  45343  monoordxrv  45431  monoordxr  45432  monoord2xrv  45433  monoord2xr  45434  evthiccabs  45448  sqrlearg  45505  climinf  45561  climinff  45566  limsupres  45660  climinf2  45662  climinf2mpt  45669  climinfmpt  45670  supcnvlimsup  45695  liminfval2  45723  liminflelimsuplem  45730  liminfltlem  45759  fprodsubrecnncnvlem  45862  fprodaddrecnncnvlem  45864  ioodvbdlimc1lem1  45886  ioodvbdlimc1lem2  45887  ioodvbdlimc2lem  45889  iblspltprt  45928  itgspltprt  45934  stoweidlem3  45958  fourierdlem2  46064  fourierdlem3  46065  fourierdlem11  46073  fourierdlem12  46074  fourierdlem15  46077  fourierdlem34  46096  fourierdlem41  46103  fourierdlem48  46109  fourierdlem49  46110  fourierdlem79  46140  fourierdlem83  46144  fourierdlem89  46150  fourierdlem91  46152  fourierdlem100  46161  fourierdlem107  46168  fourierdlem109  46170  fourierdlem112  46173  etransclem31  46220  etransclem32  46221  rrndistlt  46245  ioorrnopn  46260  ioorrnopnxrlem  46261  sge0less  46347  sge0le  46362  sge0split  46364  sge0lempt  46365  sge0iunmptlemre  46370  sge0isum  46382  sge0seq  46401  meaiuninclem  46435  meaiininclem  46441  meaiininc  46442  isome  46449  omeunile  46460  omeiunlempt  46475  carageniuncllem2  46477  0ome  46484  isomenndlem  46485  isomennd  46486  ovnssle  46516  ovnsubadd  46527  hsphoidmvle2  46540  hsphoidmvle  46541  hoidmvval0  46542  hoidmv1lelem1  46546  hoidmv1lelem2  46547  hoidmv1lelem3  46548  hoidmv1le  46549  hoidmvlelem1  46550  hoidmvlelem2  46551  hoidmvlelem3  46552  hoidmvlelem4  46553  hoidmvlelem5  46554  hoidmvle  46555  hoidifhspdmvle  46575  hspmbllem2  46582  hspmbl  46584  ovnsubadd2lem  46600  ovolval4lem2  46605  ovolval4  46606  ovolval5lem2  46608  vonioolem2  46636  vonioo  46637  vonicclem2  46639  vonicc  46640  smfid  46707  smflimlem3  46728  natglobalincr  46830  tworepnotupword  46839  2elfz2melfz  47267  smonoord  47295  iccpart  47340  iccpartimp  47341  iccpartres  47342  sqrtpwpw2p  47462  grlicsym  47908  grlictr  47910  ismgmALT  48066  iscmgmALT  48067  issgrpALT  48068  iscsgrpALT  48069  lindslinindsimp2lem5  48307  rrx2plordisom  48572  aacllem  49031