Theorem breq12d 5111

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541   class class class wbr 5098

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-br 5099

This theorem is referenced by:  breq123d  5112  3brtr3d  5129  3brtr4d  5130  sbcbr  5153  pocl  5540  csbcnvgALT  5833  cnvpo  6245  sbcfung  6516  isoeq1  7263  isocnv  7276  isotr  7282  caovordig  7563  caovordg  7565  caovord2d  7567  caovord  7569  ofrfvalg  7630  ofrval  7634  ofrfval2  7643  caofref  7653  fnwelem  8073  poseq  8100  fundmeng  8969  enrefnn  8983  xpsneng  8990  xpcomeng  8997  xpdom2g  9001  limensuc  9082  infensuc  9083  pssnn  9093  unxpdom  9159  dif1ennnALT  9177  unfilem3  9207  fodomfi  9212  domunfican  9222  fodomfiOLD  9230  marypha1lem  9336  infsupprpr  9409  wemaplem1  9451  wemaplem2  9452  wemapwe  9606  ssttrcl  9624  ttrcltr  9625  ttrclss  9629  dmttrcl  9630  rnttrcl  9631  ttrclselem2  9635  dif1card  9920  infxpenlem  9923  nnadju  10108  pwsdompw  10113  infmap2  10127  sornom  10187  isfin5  10209  isfin6  10210  domtriomlem  10352  axdc2lem  10358  axdclem2  10430  pwcfsdom  10494  cfpwsdom  10495  alephom  10496  fpwwe2lem6  10547  fpwwe2lem8  10549  tskcard  10692  ordpipq  10853  adderpqlem  10865  mulerpqlem  10866  mulcanenq  10871  lterpq  10881  ltanq  10882  ltmnq  10883  ltaddnq  10885  ltrnq  10890  archnq  10891  reclem4pr  10961  ltasr  11011  sqgt0sr  11017  axpre-ltadd  11078  axpre-mulgt0  11079  ltadd1  11604  leadd2  11606  ltmul2  11992  lemul2  11994  lemul1a  11995  ltdiv1  12006  ltdiv2  12028  lediv2  12032  div4p1lem1div2  12396  nn0ledivnn  13020  xleadd1  13170  xltadd2  13172  xsubge0  13176  xlemul1a  13203  xlemul1  13205  xlemul2  13206  xltmul2  13208  ltdifltdiv  13754  fzennn  13891  monoord  13955  monoord2  13956  expmordi  14090  ltexp2r  14096  leexp1a  14098  sqlecan  14132  bernneq  14152  faclbnd  14213  faclbnd3  14215  faclbnd4lem1  14216  faclbnd4lem2  14217  faclbnd4lem3  14218  faclbnd4lem4  14219  faclbnd6  14222  facubnd  14223  rlimcld2  15501  isercoll2  15592  climsup  15593  iseraltlem2  15606  fsumabs  15724  fsumrlim  15734  climcndslem1  15772  climcndslem2  15773  supcvg  15779  geomulcvg  15799  cvgrat  15806  ntrivcvgtail  15823  ruclem2  16157  ruclem8  16162  addmodlteqALT  16252  fproddvdsd  16262  sadcaddlem  16384  sadcadd  16385  nn0seqcvgd  16497  algcvg  16503  algcvga  16506  eucalgcvga  16513  isprm5  16634  qnumgt0  16677  pcprendvds2  16769  pcpremul  16771  pcadd2  16818  prmreclem4  16847  prmreclem5  16848  prmreclem6  16849  2expltfac  17020  xpsle  17500  mreexexlemd  17567  issubc  17759  latjlej2  18377  latmlem2  18393  ischn  18530  chnltm1  18532  chnind  18544  chnub  18545  sylow1lem3  19529  isslw  19537  fislw  19554  efgi  19648  lt6abl  19824  ablfac1eu  20004  isomnd  20052  omndadd  20057  omndmul  20064  ogrpinvlt  20073  gsumle  20074  isabv  20744  abvtri  20755  psdmul  22109  cayleyhamilton1  22836  isucn  24221  ispsmet  24248  psmettri2  24253  ismet  24267  isxmet  24268  xmettri2  24284  imasdsf1olem  24317  imasf1oxmet  24319  blvalps  24329  blval  24330  comet  24457  stdbdxmet  24459  nrmmetd  24518  tngngp  24598  tngngp3  24600  nmofval  24658  nmolb2d  24662  nmoi  24672  nmoix  24673  icopnfhmeo  24897  xrhmeo  24900  evth2  24915  pi1grplem  25005  minveclem6  25390  ovolfiniun  25458  ovoliunlem3  25461  voliunlem3  25509  ioombl1  25519  mbfmax  25606  mbfpos  25608  itg1climres  25671  mbfi1fseqlem2  25673  mbfi1fseqlem6  25677  mbfi1fseq  25678  mbfmullem  25682  itg2split  25706  itg2monolem1  25707  itg2monolem3  25709  itg2mono  25710  itg2i1fseqle  25711  itg2i1fseq  25712  itg2i1fseq2  25713  itg2addlem  25715  rolle  25950  dvlip  25954  c1lip1  25958  dvcnvrelem1  25978  dvcvx  25981  ply1divex  26098  q1pval  26116  fta1glem2  26130  fta1g  26131  fta1b  26133  plydivlem3  26259  fta1lem  26271  fta1  26272  aalioulem3  26298  aalioulem4  26299  aaliou3lem2  26307  aaliou3lem8  26309  aaliou3lem9  26314  ulmdvlem1  26365  ulmdvlem3  26367  abelthlem2  26398  abelthlem7a  26403  argrege0  26576  cxplt  26659  cxplea  26661  cxple2  26662  cxplt3  26665  logbleb  26749  logblt  26750  rlimcxp  26940  scvxcvx  26952  jensenlem2  26954  ftalem3  27041  ftalem7  27045  vmalelog  27172  chtub  27179  chpchtsum  27186  bclbnd  27247  efexple  27248  bposlem5  27255  bposlem6  27256  bposlem7  27257  lgsdilem  27291  2lgslem1a2  27357  2sqreuop  27429  2sqreuopnn  27430  2sqreuoplt  27431  2sqreuopltb  27432  2sqreuopnnlt  27433  2sqreuopnnltb  27434  dchrisumlem3  27458  dchrmusumlema  27460  dchrmusum2  27461  dchrvmasumlem2  27465  dchrvmasumlema  27467  dchrvmasumiflem1  27468  dchrisum0flblem2  27476  dchrisum0flb  27477  dchrisum0lema  27481  dchrisum0lem1b  27482  dchrisum0lem2  27485  pntrlog2bndlem2  27545  pntibndlem2  27558  pntlemf  27572  ostth2lem1  27585  qabvle  27592  ltsval2  27624  ltsres  27630  nolesgn2o  27639  nogesgn1o  27641  nodense  27660  nolt02o  27663  nogt01o  27664  noresle  27665  nosupbnd2lem1  27683  nosupbnd2  27684  noinfbnd2lem1  27698  noinfbnd2  27699  addsproplem1  27965  addsprop  27972  ltadds2im  27982  leadds2im  27984  leadds1  27985  leadds2  27986  ltadds1  27988  ltsubs1  28072  ltsubs2  28073  ltsubsubsbd  28079  ltsubsubs2bd  28080  posdifsd  28094  subsge0d  28096  mulsproplemcbv  28111  mulsproplem1  28112  mulsprop  28126  lemulsd  28134  ltmuls1d  28169  ltmulnegs1d  28172  ltmulnegs2d  28173  lemuls1ad  28178  zsoring  28405  pw2gt0divsd  28441  pw2ge0divsd  28442  legso  28671  iscgra  28881  isleag  28919  iseqlg  28939  brbtwn2  28978  axlowdim  29034  ewlksfval  29675  isnvlem  30685  nvtri  30745  nmlnoubi  30871  nmblolbii  30874  nmblolbi  30875  blocnilem  30879  sii  30929  ubthlem2  30946  minvecolem3  30951  minvecolem5  30956  minvecolem6  30957  norm-ii  31213  norm3dif  31225  norm3adifi  31228  bcs  31256  pjnorm  31799  pjnel  31801  nmbdoplbi  32099  nmbdoplb  32100  nmcoplb  32105  lnconi  32108  nmbdfnlb  32125  nmcfnlb  32129  pjdifnormi  32242  mdslmd2i  32405  cvmd  32411  cvexch  32449  cdj1i  32508  cdj3lem1  32509  cdj3lem2b  32512  cdj3lem3b  32515  cdj3i  32516  fnfvor  32687  ofrco  32688  isoun  32781  nexple  32925  ismnt  33065  mgcmntco  33076  dfmgc2lem  33077  dfmgc2  33078  mgcf1o  33085  isinftm  33263  rlocaddval  33350  rlocmulval  33351  fldext2chn  33885  constrextdg2lem  33905  constrext2chn  33916  xrmulc1cn  34087  lmdvg  34110  faeval  34403  brfae  34405  inelcarsg  34468  carsgsigalem  34472  carsgclctunlem2  34476  carsgclctun  34478  hgt750lemc  34804  hgt750lemd  34805  hgt749d  34806  fineqvnttrclse  35280  sconnpht  35423  snmlval  35525  satfv1lem  35556  satfv1  35557  satfv0fun  35565  satfv0fvfmla0  35607  lediv2aALT  35871  faclim  35940  fvtransport  36226  idinside  36278  btwnconn1lem7  36287  btwnconn1lem11  36291  btwnconn1lem12  36292  ditgeq123dv  36415  cbvditgdavw2  36492  nn0prpwlem  36516  weiunval  36656  weiunfrlem  36658  bj-opabco  37393  poimirlem29  37850  heicant  37856  itg2addnclem  37872  itg2addnclem3  37874  itg2gt0cn  37876  ftc1anclem6  37899  ftc1anc  37902  ftc2nc  37903  dvasin  37905  areacirclem1  37909  seqpo  37948  incsequz  37949  metf1o  37956  mettrifi  37958  cntotbnd  37997  heiborlem4  38015  heiborlem6  38017  heiborlem10  38021  bfplem1  38023  bfplem2  38024  isopos  39450  oplecon3b  39470  atlatle  39590  4at2  39884  pmaple  40031  islaut  40353  lautcnvle  40359  lautco  40367  ltrncnvel  40412  cdlemeg49lebilem  40809  cdlemg17h  40938  tendoset  41029  tendotp  41031  cdlemk39s  41209  lcmineqlem23  42315  lcmineqlem  42316  intlewftc  42325  aks4d1p1p4  42335  dvle2  42336  aks4d1p8d2  42349  aks4d1p9  42352  aks4d1  42353  2ap1caineq  42409  sticksstones1  42410  sticksstones2  42411  sticksstones3  42412  sticksstones8  42417  sticksstones10  42419  sticksstones11  42420  sticksstones12a  42421  sticksstones15  42425  aks6d1c7lem3  42446  unitscyglem1  42459  brif12  42491  dvdsexpnn0  42599  dvdsexpb  42600  reltsub1  42651  irrapxlem2  43075  irrapxlem4  43077  irrapxlem5  43078  irrapxlem6  43079  pellexlem3  43083  monotuz  43193  monotoddzzfi  43194  monotoddzz  43195  jm2.17a  43212  jm2.17b  43213  rmygeid  43216  rmydioph  43266  expdiophlem1  43273  expdiophlem2  43274  ttac  43288  fnwe2lem2  43303  relexp01min  43964  cvgdvgrat  44564  relpeq1  45195  monoords  45555  supxrgelem  45592  supxrge  45593  abslt2sqd  45615  ltmulneg  45646  ltdiv23neg  45648  monoordxrv  45735  monoordxr  45736  monoord2xrv  45737  monoord2xr  45738  evthiccabs  45752  sqrlearg  45809  climinf  45862  climinff  45867  limsupres  45959  climinf2  45961  climinf2mpt  45968  climinfmpt  45969  supcnvlimsup  45994  liminfval2  46022  liminfltlem  46058  fprodsubrecnncnvlem  46161  fprodaddrecnncnvlem  46163  ioodvbdlimc1lem1  46185  ioodvbdlimc1lem2  46186  ioodvbdlimc2lem  46188  iblspltprt  46227  itgspltprt  46233  stoweidlem3  46257  fourierdlem2  46363  fourierdlem3  46364  fourierdlem11  46372  fourierdlem12  46373  fourierdlem15  46376  fourierdlem34  46395  fourierdlem41  46402  fourierdlem48  46408  fourierdlem49  46409  fourierdlem79  46439  fourierdlem83  46443  fourierdlem89  46449  fourierdlem91  46451  fourierdlem100  46460  fourierdlem107  46467  fourierdlem109  46469  fourierdlem112  46472  etransclem31  46519  etransclem32  46520  rrndistlt  46544  ioorrnopn  46559  ioorrnopnxrlem  46560  sge0less  46646  sge0le  46661  sge0split  46663  sge0lempt  46664  sge0iunmptlemre  46669  sge0isum  46681  sge0seq  46700  meaiuninclem  46734  meaiininclem  46740  meaiininc  46741  isome  46748  omeunile  46759  omeiunlempt  46774  carageniuncllem2  46776  0ome  46783  isomenndlem  46784  isomennd  46785  ovnssle  46815  ovnsubadd  46826  hsphoidmvle2  46839  hsphoidmvle  46840  hoidmvval0  46841  hoidmv1lelem1  46845  hoidmv1lelem2  46846  hoidmv1lelem3  46847  hoidmv1le  46848  hoidmvlelem1  46849  hoidmvlelem2  46850  hoidmvlelem3  46851  hoidmvlelem4  46852  hoidmvlelem5  46853  hoidmvle  46854  hoidifhspdmvle  46874  hspmbllem2  46881  hspmbl  46883  ovnsubadd2lem  46899  ovolval4lem2  46904  ovolval4  46905  ovolval5lem2  46907  vonioolem2  46935  vonioo  46936  vonicclem2  46938  vonicc  46939  smfid  47006  smflimlem3  47027  ormkglobd  47129  natglobalincr  47131  chnerlem1  47136  squeezedltsq  47142  2elfz2melfz  47574  smonoord  47627  iccpart  47672  iccpartimp  47673  iccpartres  47674  sqrtpwpw2p  47794  grlicsym  48269  grlictr  48271  ismgmALT  48479  iscmgmALT  48480  issgrpALT  48481  iscsgrpALT  48482  lindslinindsimp2lem5  48718  rrx2plordisom  48979  aacllem  50056