Theorem breq12d 5156

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 5148	. 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐷))
4	1, 2, 3	syl2anc 584	1 ⊢ (𝜑 → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐷))

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540   class class class wbr 5143

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-br 5144

This theorem is referenced by:  breq123d  5157  3brtr3d  5174  3brtr4d  5175  sbcbr  5198  pocl  5600  csbcnvgALT  5895  cnvpo  6307  sbcfung  6590  isoeq1  7337  isocnv  7350  isotr  7356  caovordig  7638  caovordg  7640  caovord2d  7642  caovord  7644  ofrfvalg  7705  ofrval  7709  ofrfval2  7718  caofref  7728  fnwelem  8156  poseq  8183  fundmeng  9072  enrefnn  9087  xpsneng  9096  xpcomeng  9104  xpdom2g  9108  limensuc  9194  infensuc  9195  pssnn  9208  unxpdom  9289  dif1ennnALT  9311  unfilem3  9345  fodomfi  9350  domunfican  9361  fodomfiOLD  9370  marypha1lem  9473  infsupprpr  9544  wemaplem1  9586  wemaplem2  9587  wemapwe  9737  ssttrcl  9755  ttrcltr  9756  ttrclss  9760  dmttrcl  9761  rnttrcl  9762  ttrclselem2  9766  dif1card  10050  infxpenlem  10053  nnadju  10238  pwsdompw  10243  infmap2  10257  sornom  10317  isfin5  10339  isfin6  10340  domtriomlem  10482  axdc2lem  10488  axdclem2  10560  pwcfsdom  10623  cfpwsdom  10624  alephom  10625  fpwwe2lem6  10676  fpwwe2lem8  10678  tskcard  10821  ordpipq  10982  adderpqlem  10994  mulerpqlem  10995  mulcanenq  11000  lterpq  11010  ltanq  11011  ltmnq  11012  ltaddnq  11014  ltrnq  11019  archnq  11020  reclem4pr  11090  ltasr  11140  sqgt0sr  11146  axpre-ltadd  11207  axpre-mulgt0  11208  ltadd1  11730  leadd2  11732  ltmul2  12118  lemul2  12120  lemul1a  12121  ltdiv1  12132  ltdiv2  12154  lediv2  12158  div4p1lem1div2  12521  nn0ledivnn  13148  xleadd1  13297  xltadd2  13299  xsubge0  13303  xlemul1a  13330  xlemul1  13332  xlemul2  13333  xltmul2  13335  ltdifltdiv  13874  fzennn  14009  monoord  14073  monoord2  14074  expmordi  14207  ltexp2r  14213  leexp1a  14215  sqlecan  14248  bernneq  14268  faclbnd  14329  faclbnd3  14331  faclbnd4lem1  14332  faclbnd4lem2  14333  faclbnd4lem3  14334  faclbnd4lem4  14335  faclbnd6  14338  facubnd  14339  rlimcld2  15614  isercoll2  15705  climsup  15706  iseraltlem2  15719  fsumabs  15837  fsumrlim  15847  climcndslem1  15885  climcndslem2  15886  supcvg  15892  geomulcvg  15912  cvgrat  15919  ntrivcvgtail  15936  ruclem2  16268  ruclem8  16273  addmodlteqALT  16362  fproddvdsd  16372  sadcaddlem  16494  sadcadd  16495  nn0seqcvgd  16607  algcvg  16613  algcvga  16616  eucalgcvga  16623  isprm5  16744  qnumgt0  16787  pcprendvds2  16879  pcpremul  16881  pcadd2  16928  prmreclem4  16957  prmreclem5  16958  prmreclem6  16959  2expltfac  17130  xpsle  17624  mreexexlemd  17687  issubc  17880  latjlej2  18499  latmlem2  18515  sylow1lem3  19618  isslw  19626  fislw  19643  efgi  19737  lt6abl  19913  ablfac1eu  20093  isabv  20812  abvtri  20823  psdmul  22170  cayleyhamilton1  22898  isucn  24287  ispsmet  24314  psmettri2  24319  ismet  24333  isxmet  24334  xmettri2  24350  imasdsf1olem  24383  imasf1oxmet  24385  blvalps  24395  blval  24396  comet  24526  stdbdxmet  24528  nrmmetd  24587  tngngp  24675  tngngp3  24677  nmofval  24735  nmolb2d  24739  nmoi  24749  nmoix  24750  icopnfhmeo  24974  xrhmeo  24977  evth2  24992  pi1grplem  25082  minveclem6  25468  ovolfiniun  25536  ovoliunlem3  25539  voliunlem3  25587  ioombl1  25597  mbfmax  25684  mbfpos  25686  itg1climres  25749  mbfi1fseqlem2  25751  mbfi1fseqlem6  25755  mbfi1fseq  25756  mbfmullem  25760  itg2split  25784  itg2monolem1  25785  itg2monolem3  25787  itg2mono  25788  itg2i1fseqle  25789  itg2i1fseq  25790  itg2i1fseq2  25791  itg2addlem  25793  rolle  26028  dvlip  26032  c1lip1  26036  dvcnvrelem1  26056  dvcvx  26059  ply1divex  26176  q1pval  26194  fta1glem2  26208  fta1g  26209  fta1b  26211  plydivlem3  26337  fta1lem  26349  fta1  26350  aalioulem3  26376  aalioulem4  26377  aaliou3lem2  26385  aaliou3lem8  26387  aaliou3lem9  26392  ulmdvlem1  26443  ulmdvlem3  26445  abelthlem2  26476  abelthlem7a  26481  argrege0  26653  cxplt  26736  cxplea  26738  cxple2  26739  cxplt3  26742  logbleb  26826  logblt  26827  rlimcxp  27017  scvxcvx  27029  jensenlem2  27031  ftalem3  27118  ftalem7  27122  vmalelog  27249  chtub  27256  chpchtsum  27263  bclbnd  27324  efexple  27325  bposlem5  27332  bposlem6  27333  bposlem7  27334  lgsdilem  27368  2lgslem1a2  27434  2sqreuop  27506  2sqreuopnn  27507  2sqreuoplt  27508  2sqreuopltb  27509  2sqreuopnnlt  27510  2sqreuopnnltb  27511  dchrisumlem3  27535  dchrmusumlema  27537  dchrmusum2  27538  dchrvmasumlem2  27542  dchrvmasumlema  27544  dchrvmasumiflem1  27545  dchrisum0flblem2  27553  dchrisum0flb  27554  dchrisum0lema  27558  dchrisum0lem1b  27559  dchrisum0lem2  27562  pntrlog2bndlem2  27622  pntibndlem2  27635  pntlemf  27649  ostth2lem1  27662  qabvle  27669  sltval2  27701  sltres  27707  nolesgn2o  27716  nogesgn1o  27718  nodense  27737  nolt02o  27740  nogt01o  27741  noresle  27742  nosupbnd2lem1  27760  nosupbnd2  27761  noinfbnd2lem1  27775  noinfbnd2  27776  addsproplem1  28002  addsprop  28009  sltadd2im  28019  sleadd2im  28021  sleadd1  28022  sleadd2  28023  sltadd1  28025  sltsub1  28106  sltsub2  28107  sltsubsubbd  28113  sltsubsub2bd  28114  posdifsd  28127  subsge0d  28129  mulsproplemcbv  28141  mulsproplem1  28142  mulsprop  28156  slemuld  28164  sltmul1d  28199  sltmulneg1d  28202  sltmulneg2d  28203  slemul1ad  28208  legso  28607  iscgra  28817  isleag  28855  iseqlg  28875  brbtwn2  28920  axlowdim  28976  ewlksfval  29619  isnvlem  30629  nvtri  30689  nmlnoubi  30815  nmblolbii  30818  nmblolbi  30819  blocnilem  30823  sii  30873  ubthlem2  30890  minvecolem3  30895  minvecolem5  30900  minvecolem6  30901  norm-ii  31157  norm3dif  31169  norm3adifi  31172  bcs  31200  pjnorm  31743  pjnel  31745  nmbdoplbi  32043  nmbdoplb  32044  nmcoplb  32049  lnconi  32052  nmbdfnlb  32069  nmcfnlb  32073  pjdifnormi  32186  mdslmd2i  32349  cvmd  32355  cvexch  32393  cdj1i  32452  cdj3lem1  32453  cdj3lem2b  32456  cdj3lem3b  32459  cdj3i  32460  isoun  32711  nexple  32833  ismnt  32973  mgcmntco  32984  dfmgc2lem  32985  dfmgc2  32986  mgcf1o  32993  ischn  32996  chnltm1  32998  chnind  33001  chnub  33002  isomnd  33078  omndadd  33083  omndmul  33091  ogrpinvlt  33100  gsumle  33101  isinftm  33188  rlocaddval  33272  rlocmulval  33273  fldext2chn  33769  constrextdg2lem  33789  xrmulc1cn  33929  lmdvg  33952  faeval  34247  brfae  34249  inelcarsg  34313  carsgsigalem  34317  carsgclctunlem2  34321  carsgclctun  34323  hgt750lemc  34662  hgt750lemd  34663  hgt749d  34664  sconnpht  35234  snmlval  35336  satfv1lem  35367  satfv1  35368  satfv0fun  35376  satfv0fvfmla0  35418  lediv2aALT  35682  faclim  35746  fvtransport  36033  idinside  36085  btwnconn1lem7  36094  btwnconn1lem11  36098  btwnconn1lem12  36099  ditgeq123dv  36222  cbvditgdavw2  36299  nn0prpwlem  36323  weiunlem1  36463  weiunfrlem  36465  bj-opabco  37189  poimirlem29  37656  heicant  37662  itg2addnclem  37678  itg2addnclem3  37680  itg2gt0cn  37682  ftc1anclem6  37705  ftc1anc  37708  ftc2nc  37709  dvasin  37711  areacirclem1  37715  seqpo  37754  incsequz  37755  metf1o  37762  mettrifi  37764  cntotbnd  37803  heiborlem4  37821  heiborlem6  37823  heiborlem10  37827  bfplem1  37829  bfplem2  37830  isopos  39181  oplecon3b  39201  atlatle  39321  4at2  39616  pmaple  39763  islaut  40085  lautcnvle  40091  lautco  40099  ltrncnvel  40144  cdlemeg49lebilem  40541  cdlemg17h  40670  tendoset  40761  tendotp  40763  cdlemk39s  40941  lcmineqlem23  42052  lcmineqlem  42053  intlewftc  42062  aks4d1p1p4  42072  dvle2  42073  aks4d1p8d2  42086  aks4d1p9  42089  aks4d1  42090  2ap1caineq  42146  sticksstones1  42147  sticksstones2  42148  sticksstones3  42149  sticksstones8  42154  sticksstones10  42156  sticksstones11  42157  sticksstones12a  42158  sticksstones15  42162  aks6d1c7lem3  42183  unitscyglem1  42196  factwoffsmonot  42243  brif12  42264  dvdsexpnn0  42369  dvdsexpb  42370  reltsub1  42416  irrapxlem2  42834  irrapxlem4  42836  irrapxlem5  42837  irrapxlem6  42838  pellexlem3  42842  monotuz  42953  monotoddzzfi  42954  monotoddzz  42955  jm2.17a  42972  jm2.17b  42973  rmygeid  42976  rmydioph  43026  expdiophlem1  43033  expdiophlem2  43034  ttac  43048  fnwe2lem2  43063  relexp01min  43726  cvgdvgrat  44332  relpeq1  44965  monoords  45309  supxrgelem  45348  supxrge  45349  abslt2sqd  45371  ltmulneg  45403  ltdiv23neg  45405  monoordxrv  45492  monoordxr  45493  monoord2xrv  45494  monoord2xr  45495  evthiccabs  45509  sqrlearg  45566  climinf  45621  climinff  45626  limsupres  45720  climinf2  45722  climinf2mpt  45729  climinfmpt  45730  supcnvlimsup  45755  liminfval2  45783  liminflelimsuplem  45790  liminfltlem  45819  fprodsubrecnncnvlem  45922  fprodaddrecnncnvlem  45924  ioodvbdlimc1lem1  45946  ioodvbdlimc1lem2  45947  ioodvbdlimc2lem  45949  iblspltprt  45988  itgspltprt  45994  stoweidlem3  46018  fourierdlem2  46124  fourierdlem3  46125  fourierdlem11  46133  fourierdlem12  46134  fourierdlem15  46137  fourierdlem34  46156  fourierdlem41  46163  fourierdlem48  46169  fourierdlem49  46170  fourierdlem79  46200  fourierdlem83  46204  fourierdlem89  46210  fourierdlem91  46212  fourierdlem100  46221  fourierdlem107  46228  fourierdlem109  46230  fourierdlem112  46233  etransclem31  46280  etransclem32  46281  rrndistlt  46305  ioorrnopn  46320  ioorrnopnxrlem  46321  sge0less  46407  sge0le  46422  sge0split  46424  sge0lempt  46425  sge0iunmptlemre  46430  sge0isum  46442  sge0seq  46461  meaiuninclem  46495  meaiininclem  46501  meaiininc  46502  isome  46509  omeunile  46520  omeiunlempt  46535  carageniuncllem2  46537  0ome  46544  isomenndlem  46545  isomennd  46546  ovnssle  46576  ovnsubadd  46587  hsphoidmvle2  46600  hsphoidmvle  46601  hoidmvval0  46602  hoidmv1lelem1  46606  hoidmv1lelem2  46607  hoidmv1lelem3  46608  hoidmv1le  46609  hoidmvlelem1  46610  hoidmvlelem2  46611  hoidmvlelem3  46612  hoidmvlelem4  46613  hoidmvlelem5  46614  hoidmvle  46615  hoidifhspdmvle  46635  hspmbllem2  46642  hspmbl  46644  ovnsubadd2lem  46660  ovolval4lem2  46665  ovolval4  46666  ovolval5lem2  46668  vonioolem2  46696  vonioo  46697  vonicclem2  46699  vonicc  46700  smfid  46767  smflimlem3  46788  ormkglobd  46890  natglobalincr  46892  tworepnotupword  46901  2elfz2melfz  47330  smonoord  47358  iccpart  47403  iccpartimp  47404  iccpartres  47405  sqrtpwpw2p  47525  grlicsym  47973  grlictr  47975  ismgmALT  48139  iscmgmALT  48140  issgrpALT  48141  iscsgrpALT  48142  lindslinindsimp2lem5  48379  rrx2plordisom  48644  aacllem  49320