Theorem breq12d 5116

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570   class class class wbr 5103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104

This theorem is used by:  breq123d  5117  3brtr3d  5136  3brtr4d  5137  sbcbr  5160  pocl  5571  csbcnvgALTOLD  5868  cnvpo  6285  sbcfungOLD  6558  isoeq1  7319  isocnv  7332  isotr  7338  caovordig  7620  caovordg  7622  caovord2d  7624  caovord  7626  ofrfvalg  7687  ofrval  7691  ofrfval2  7700  caofref  7710  fnwelem  8130  poseq  8157  fundmeng  9042  enrefnn  9056  xpsneng  9063  xpcomeng  9070  xpdom2g  9074  limensuc  9155  infensuc  9156  pssnn  9166  unxpdom  9232  dif1ennnALT  9250  unfilem3  9280  fodomfi  9285  domunfican  9294  marypha1lem  9406  infsupprpr  9479  wemaplem1  9521  wemaplem2  9522  wemapwe  9679  ssttrcl  9697  ttrcltr  9698  ttrclss  9702  dmttrcl  9703  rnttrcl  9704  ttrclselem2  9708  dif1card  10016  infxpenlem  10019  nnadju  10203  pwsdompw  10208  infmap2  10222  sornom  10282  isfin5  10304  isfin6  10305  domtriomlem  10447  axdc2lem  10453  axdclem2  10525  pwcfsdom  10595  cfpwsdom  10596  alephom  10597  fpwwe2lem6  10648  fpwwe2lem8  10650  tskcard  10793  ordpipq  10954  adderpqlem  10966  mulerpqlem  10967  mulcanenq  10972  lterpq  10982  ltanq  10983  ltmnq  10984  ltaddnq  10986  ltrnq  10991  archnq  10992  reclem4pr  11062  ltasr  11112  sqgt0sr  11118  axpre-ltadd  11179  axpre-mulgt0  11180  ltadd1  11708  leadd2  11710  ltmul2  12093  lemul2  12095  lemul1a  12096  ltdiv1  12106  ltdiv2  12128  lediv2  12132  div4p1lem1div2  12526  nn0ledivnn  13160  xleadd1  13310  xltadd2  13312  xsubge0  13316  xlemul1a  13343  xlemul1  13345  xlemul2  13346  xltmul2  13348  ltdifltdiv  13898  fzennn  14035  monoord  14099  monoord2  14100  expmordi  14234  ltexp2r  14240  leexp1a  14242  sqlecan  14276  bernneq  14296  faclbnd  14357  faclbnd3  14359  faclbnd4lem1  14360  faclbnd4lem2  14361  faclbnd4lem3  14362  faclbnd4lem4  14363  faclbnd6  14366  facubnd  14367  rlimcld2  15668  isercoll2  15759  climsup  15760  iseraltlem2  15773  fsumabs  15891  fsumrlim  15901  climcndslem1  15941  climcndslem2  15942  supcvg  15948  geomulcvg  15968  cvgrat  15975  ntrivcvgtail  15992  ruclem2  16323  ruclem8  16328  addmodlteqALT  16418  fproddvdsd  16428  sadcaddlem  16550  sadcadd  16551  nn0seqcvgd  16663  algcvg  16669  algcvga  16672  eucalgcvga  16679  isprm5  16801  qnumgt0  16844  pcprendvds2  16936  pcpremul  16938  pcadd2  16985  prmreclem4  17014  prmreclem5  17015  prmreclem6  17016  2expltfac  17187  xpsle  17668  mreexexlemd  17735  issubc  17927  latjlej2  18545  latmlem2  18561  ischn  18698  chnltm1  18700  chnind  18712  chnub  18713  sylow1lem3  19730  isslw  19738  fislw  19755  efgi  19849  lt6abl  20025  ablfac1eu  20205  isomnd  20253  omndadd  20258  omndmul  20265  ogrpinvlt  20274  gsumle  20275  isabv  20980  abvtri  20991  psdmul  22397  cayleyhamilton1  23120  isucn  24506  ispsmet  24533  psmettri2  24538  ismet  24552  isxmet  24553  xmettri2  24569  imasdsf1olem  24602  imasf1oxmet  24604  blvalps  24614  blval  24615  comet  24742  stdbdxmet  24744  nrmmetd  24803  tngngp  24883  tngngp3  24885  nmofval  24943  nmolb2d  24947  nmoi  24957  nmoix  24958  icopnfhmeo  25174  xrhmeo  25177  evth2  25191  pi1grplem  25280  minveclem6  25665  ovolfiniun  25732  ovoliunlem3  25735  voliunlem3  25783  ioombl1  25793  mbfmax  25880  mbfpos  25882  itg1climres  25945  mbfi1fseqlem2  25947  mbfi1fseqlem6  25951  mbfi1fseq  25952  mbfmullem  25956  itg2split  25980  itg2monolem1  25981  itg2monolem3  25983  itg2mono  25984  itg2i1fseqle  25985  itg2i1fseq  25986  itg2i1fseq2  25987  itg2addlem  25989  rolle  26220  dvlip  26223  c1lip1  26227  dvcnvrelem1  26247  dvcvx  26250  ply1divex  26365  q1pval  26383  fta1glem2  26397  fta1g  26398  fta1b  26400  plydivlem3  26528  fta1lem  26540  fta1  26541  aalioulem3  26573  aalioulem4  26574  aaliou3lem2  26582  aaliou3lem8  26584  aaliou3lem9  26589  ulmdvlem1  26639  ulmdvlem3  26641  abelthlem2  26671  abelthlem7a  26676  argrege0  26851  cxplt  26934  cxplea  26936  cxple2  26937  cxplt3  26940  logbleb  27023  logblt  27024  rlimcxp  27213  scvxcvx  27225  jensenlem2  27227  ftalem3  27314  ftalem7  27318  vmalelog  27444  chtub  27451  chpchtsum  27458  bclbnd  27519  efexple  27520  bposlem5  27527  bposlem6  27528  bposlem7  27529  lgsdilem  27563  2lgslem1a2  27629  2sqreuop  27701  2sqreuopnn  27702  2sqreuoplt  27703  2sqreuopltb  27704  2sqreuopnnlt  27705  2sqreuopnnltb  27706  dchrisumlem3  27730  dchrmusumlema  27732  dchrmusum2  27733  dchrvmasumlem2  27737  dchrvmasumlema  27739  dchrvmasumiflem1  27740  dchrisum0flblem2  27748  dchrisum0flb  27749  dchrisum0lema  27753  dchrisum0lem1b  27754  dchrisum0lem2  27757  pntrlog2bndlem2  27817  pntibndlem2  27830  pntlemf  27844  ostth2lem1  27857  qabvle  27864  ltsval2  27895  ltsres  27901  nolesgn2o  27910  nogesgn1o  27912  nodense  27931  nolt02o  27934  nogt01o  27935  noresle  27936  nosupbnd2lem1  27954  nosupbnd2  27955  noinfbnd2lem1  27969  noinfbnd2  27970  addsproplem1  28237  addsprop  28244  ltadds2im  28254  leadds2im  28256  leadds1  28257  leadds2  28258  ltadds1  28260  ltsubs1  28344  ltsubs2  28345  ltsubsubsbd  28351  ltsubsubs2bd  28352  posdifsd  28366  subsge0d  28368  mulsproplemcbv  28383  mulsproplem1  28384  mulsprop  28398  lemulsd  28406  ltmuls1d  28441  ltmulnegs1d  28444  ltmulnegs2d  28445  lemuls1ad  28450  zsoring  28677  pw2gt0divsd  28713  pw2ge0divsd  28714  legso  28944  iscgra  29198  isleag  29248  angmgmaddov2  29271  iseqlg  29294  brbtwn2  29365  axlowdim  29421  ewlksfval  30064  isnvlem  31094  nvtri  31154  nmlnoubi  31280  nmblolbii  31283  nmblolbi  31284  blocnilem  31288  sii  31338  ubthlem2  31355  minvecolem3  31360  minvecolem5  31365  minvecolem6  31366  norm-ii  31622  norm3dif  31634  norm3adifi  31637  bcs  31665  pjnorm  32208  pjnel  32210  nmbdoplbi  32508  nmbdoplb  32509  nmcoplb  32514  lnconi  32517  nmbdfnlb  32534  nmcfnlb  32538  pjdifnormi  32651  mdslmd2i  32814  cvmd  32820  cvexch  32858  cdj1i  32917  cdj3lem1  32918  cdj3lem2b  32921  cdj3lem3b  32924  cdj3i  32925  fnfvor  33085  ofrco  33086  isoun  33177  nexple  33306  ismnt  33426  mgcmntco  33437  dfmgc2lem  33438  dfmgc2  33439  mgcf1o  33446  isinftm  33624  rlocaddval  33712  rlocmulval  33713  fldext2chn  34241  constrextdg2lem  34261  constrext2chn  34272  xrmulc1cn  34443  lmdvg  34466  faeval  34760  brfae  34762  inelcarsg  34825  carsgsigalem  34829  carsgclctunlem2  34833  carsgclctun  34835  hgt750lemc  35158  hgt750lemd  35159  hgt749d  35160  fineqvnttrclse  35653  sconnpht  35811  snmlval  35913  satfv1lem  35944  satfv1  35945  satfv0fun  35953  satfv0fvfmla0  35995  lediv2aALT  36259  faclim  36328  fvtransport  36615  idinside  36667  btwnconn1lem7  36676  btwnconn1lem11  36680  btwnconn1lem12  36681  ditgeq123dv  36844  cbvditgdavw2  36921  nn0prpwlem  36944  weiunval  37084  weiunfrlem  37086  bj-opabco  37943  poimirlem29  38401  heicant  38407  itg2addnclem  38423  itg2addnclem3  38425  itg2gt0cn  38427  ftc1anclem6  38450  ftc1anc  38453  ftc2nc  38454  dvasin  38456  areacirclem1  38460  seqpo  38500  incsequz  38501  metf1o  38508  mettrifi  38510  cntotbnd  38549  heiborlem4  38567  heiborlem6  38569  heiborlem10  38573  bfplem1  38575  bfplem2  38576  isopos  40056  oplecon3b  40076  atlatle  40196  4at2  40490  pmaple  40637  islaut  40959  lautcnvle  40965  lautco  40973  ltrncnvel  41018  cdlemeg49lebilem  41415  cdlemg17h  41544  tendoset  41635  tendotp  41637  cdlemk39s  41815  lcmineqlem23  42920  lcmineqlem  42921  intlewftc  42930  aks4d1p1p4  42940  dvle2  42941  aks4d1p8d2  42954  aks4d1p9  42957  aks4d1  42958  2ap1caineq  43014  sticksstones1  43015  sticksstones2  43016  sticksstones3  43017  sticksstones8  43022  sticksstones10  43024  sticksstones11  43025  sticksstones12a  43026  sticksstones15  43030  aks6d1c7lem3  43051  unitscyglem1  43064  brif12  43098  dvdsexpnn0  43212  dvdsexpb  43213  reltsub1  43264  irrapxlem2  43667  irrapxlem4  43669  irrapxlem5  43670  irrapxlem6  43671  pellexlem3  43675  monotuz  43785  monotoddzzfi  43786  monotoddzz  43787  jm2.17a  43804  jm2.17b  43805  rmygeid  43808  rmydioph  43858  expdiophlem1  43865  expdiophlem2  43866  ttac  43880  fnwe2lem2  43895  relexp01min  44556  cvgdvgrat  45140  relpeq1  45770  monoords  46133  supxrgelem  46170  supxrge  46171  abslt2sqd  46193  ltmulneg  46224  ltdiv23neg  46226  monoordxrv  46312  monoordxr  46313  monoord2xrv  46314  monoord2xr  46315  evthiccabs  46329  sqrlearg  46386  climinf  46439  climinff  46444  limsupres  46536  climinf2  46538  climinf2mpt  46545  climinfmpt  46546  supcnvlimsup  46571  liminfval2  46599  liminfltlem  46635  fprodsubrecnncnvlem  46738  fprodaddrecnncnvlem  46740  ioodvbdlimc1lem1  46762  ioodvbdlimc1lem2  46763  ioodvbdlimc2lem  46765  iblspltprt  46804  itgspltprt  46810  stoweidlem3  46834  fourierdlem2  46940  fourierdlem3  46941  fourierdlem11  46949  fourierdlem12  46950  fourierdlem15  46953  fourierdlem34  46972  fourierdlem41  46979  fourierdlem48  46985  fourierdlem49  46986  fourierdlem79  47016  fourierdlem83  47020  fourierdlem89  47026  fourierdlem91  47028  fourierdlem100  47037  fourierdlem107  47044  fourierdlem109  47046  fourierdlem112  47049  etransclem31  47096  etransclem32  47097  rrndistlt  47121  ioorrnopn  47136  ioorrnopnxrlem  47137  sge0less  47223  sge0le  47238  sge0split  47240  sge0lempt  47241  sge0iunmptlemre  47246  sge0isum  47258  sge0seq  47277  meaiuninclem  47311  meaiininclem  47317  meaiininc  47318  isome  47325  omeunile  47336  omeiunlempt  47351  carageniuncllem2  47353  0ome  47360  isomenndlem  47361  isomennd  47362  ovnssle  47392  ovnsubadd  47403  hsphoidmvle2  47416  hsphoidmvle  47417  hoidmvval0  47418  hoidmv1lelem1  47422  hoidmv1lelem2  47423  hoidmv1lelem3  47424  hoidmv1le  47425  hoidmvlelem1  47426  hoidmvlelem2  47427  hoidmvlelem3  47428  hoidmvlelem4  47429  hoidmvlelem5  47430  hoidmvle  47431  hoidifhspdmvle  47451  hspmbllem2  47458  hspmbl  47460  ovnsubadd2lem  47476  ovolval4lem2  47481  ovolval4  47482  ovolval5lem2  47484  vonioolem2  47512  vonioo  47513  vonicclem2  47515  vonicc  47516  smfid  47583  smflimlem3  47604  ormkglobd  47708  chnerlem1  47713  squeezedltsq  47733  2elfz2melfz  48209  smonoord  48268  iccpart  48319  iccpartimp  48320  iccpartres  48321  sqrtpwpw2p  48444  grlicsym  48932  grlictr  48934  ismgmALT  49141  iscmgmALT  49142  issgrpALT  49143  iscsgrpALT  49144  lindslinindsimp2lem5  49395  rrx2plordisom  49656  aacllem  50775