Theorem breq12d 5088

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1539   class class class wbr 5075

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-rab 3074  df-v 3435  df-dif 3891  df-un 3893  df-nul 4258  df-if 4461  df-sn 4563  df-pr 4565  df-op 4569  df-br 5076

This theorem is referenced by:  breq123d  5089  3brtr3d  5106  3brtr4d  5107  sbcbr  5130  pocl  5511  poclOLD  5512  csbcnvgALT  5796  cnvpo  6194  sbcfung  6465  isoeq1  7197  isocnv  7210  isotr  7216  caovordig  7486  caovordg  7488  caovord2d  7490  caovord  7492  ofrfvalg  7550  ofrval  7554  ofrfval2  7563  caofref  7571  fnwelem  7981  fundmeng  8831  enrefnn  8846  xpsneng  8852  xpcomeng  8860  xpdom2g  8864  limensuc  8950  infensuc  8951  pssnn  8960  unxpdom  9039  pssnnOLD  9049  dif1enALT  9059  unfilem3  9089  unfiOLD  9090  domunfican  9096  fodomfi  9101  marypha1lem  9201  infsupprpr  9272  wemaplem1  9314  wemaplem2  9315  wemapwe  9464  ssttrcl  9482  ttrcltr  9483  ttrclss  9487  dmttrcl  9488  rnttrcl  9489  ttrclselem2  9493  dif1card  9775  infxpenlem  9778  nnadju  9962  pwsdompw  9969  infmap2  9983  sornom  10042  isfin5  10064  isfin6  10065  domtriomlem  10207  axdc2lem  10213  axdclem2  10285  pwcfsdom  10348  cfpwsdom  10349  alephom  10350  fpwwe2lem6  10401  fpwwe2lem8  10403  tskcard  10546  ordpipq  10707  adderpqlem  10719  mulerpqlem  10720  mulcanenq  10725  lterpq  10735  ltanq  10736  ltmnq  10737  ltaddnq  10739  ltrnq  10744  archnq  10745  reclem4pr  10815  ltasr  10865  sqgt0sr  10871  axpre-ltadd  10932  axpre-mulgt0  10933  ltadd1  11451  leadd2  11453  ltmul2  11835  lemul2  11837  lemul1a  11838  ltdiv1  11848  ltdiv2  11870  lediv2  11874  div4p1lem1div2  12237  nn0ledivnn  12852  xleadd1  12998  xltadd2  13000  xsubge0  13004  xlemul1a  13031  xlemul1  13033  xlemul2  13034  xltmul2  13036  ltdifltdiv  13563  fzennn  13697  monoord  13762  monoord2  13763  expmordi  13894  ltexp2r  13900  leexp1a  13902  sqlecan  13934  bernneq  13953  faclbnd  14013  faclbnd3  14015  faclbnd4lem1  14016  faclbnd4lem2  14017  faclbnd4lem3  14018  faclbnd4lem4  14019  faclbnd6  14022  facubnd  14023  rlimcld2  15296  isercoll2  15389  climsup  15390  iseraltlem2  15403  fsumabs  15522  fsumrlim  15532  climcndslem1  15570  climcndslem2  15571  supcvg  15577  geomulcvg  15597  cvgrat  15604  ntrivcvgtail  15621  ruclem2  15950  ruclem8  15955  addmodlteqALT  16043  fproddvdsd  16053  sadcaddlem  16173  sadcadd  16174  nn0seqcvgd  16284  algcvg  16290  algcvga  16293  eucalgcvga  16300  isprm5  16421  qnumgt0  16463  pcprendvds2  16551  pcpremul  16553  pcadd2  16600  prmreclem4  16629  prmreclem5  16630  prmreclem6  16631  2expltfac  16803  xpsle  17299  mreexexlemd  17362  issubc  17559  latjlej2  18181  latmlem2  18197  sylow1lem3  19214  isslw  19222  fislw  19239  efgi  19334  lt6abl  19505  ablfac1eu  19685  isabv  20088  abvtri  20099  cayleyhamilton1  22050  isucn  23439  ispsmet  23466  psmettri2  23471  ismet  23485  isxmet  23486  xmettri2  23502  imasdsf1olem  23535  imasf1oxmet  23537  blvalps  23547  blval  23548  comet  23678  stdbdxmet  23680  nrmmetd  23739  tngngp  23827  tngngp3  23829  nmofval  23887  nmolb2d  23891  nmoi  23901  nmoix  23902  icopnfhmeo  24115  xrhmeo  24118  evth2  24132  pi1grplem  24221  minveclem6  24607  ovolfiniun  24674  ovoliunlem3  24677  voliunlem3  24725  ioombl1  24735  mbfmax  24822  mbfpos  24824  itg1climres  24888  mbfi1fseqlem2  24890  mbfi1fseqlem6  24894  mbfi1fseq  24895  mbfmullem  24899  itg2split  24923  itg2monolem1  24924  itg2monolem3  24926  itg2mono  24927  itg2i1fseqle  24928  itg2i1fseq  24929  itg2i1fseq2  24930  itg2addlem  24932  rolle  25163  dvlip  25166  c1lip1  25170  dvcnvrelem1  25190  dvcvx  25193  ply1divex  25310  q1pval  25327  fta1glem2  25340  fta1g  25341  fta1b  25343  plydivlem3  25464  fta1lem  25476  fta1  25477  aalioulem3  25503  aalioulem4  25504  aaliou3lem2  25512  aaliou3lem8  25514  aaliou3lem9  25519  ulmdvlem1  25568  ulmdvlem3  25570  abelthlem2  25600  abelthlem7a  25605  argrege0  25775  cxplt  25858  cxplea  25860  cxple2  25861  cxplt3  25864  logbleb  25942  logblt  25943  rlimcxp  26132  scvxcvx  26144  jensenlem2  26146  ftalem3  26233  ftalem7  26237  vmalelog  26362  chtub  26369  chpchtsum  26376  bclbnd  26437  efexple  26438  bposlem5  26445  bposlem6  26446  bposlem7  26447  lgsdilem  26481  2lgslem1a2  26547  2sqreuop  26619  2sqreuopnn  26620  2sqreuoplt  26621  2sqreuopltb  26622  2sqreuopnnlt  26623  2sqreuopnnltb  26624  dchrisumlem3  26648  dchrmusumlema  26650  dchrmusum2  26651  dchrvmasumlem2  26655  dchrvmasumlema  26657  dchrvmasumiflem1  26658  dchrisum0flblem2  26666  dchrisum0flb  26667  dchrisum0lema  26671  dchrisum0lem1b  26672  dchrisum0lem2  26675  pntrlog2bndlem2  26735  pntibndlem2  26748  pntlemf  26762  ostth2lem1  26775  qabvle  26782  legso  26969  iscgra  27179  isleag  27217  iseqlg  27237  brbtwn2  27282  axlowdim  27338  ewlksfval  27977  isnvlem  28981  nvtri  29041  nmlnoubi  29167  nmblolbii  29170  nmblolbi  29171  blocnilem  29175  sii  29225  ubthlem2  29242  minvecolem3  29247  minvecolem5  29252  minvecolem6  29253  norm-ii  29509  norm3dif  29521  norm3adifi  29524  bcs  29552  pjnorm  30095  pjnel  30097  nmbdoplbi  30395  nmbdoplb  30396  nmcoplb  30401  lnconi  30404  nmbdfnlb  30421  nmcfnlb  30425  pjdifnormi  30538  mdslmd2i  30701  cvmd  30707  cvexch  30745  cdj1i  30804  cdj3lem1  30805  cdj3lem2b  30808  cdj3lem3b  30811  cdj3i  30812  isoun  31043  ismnt  31270  mgcmntco  31281  dfmgc2lem  31282  dfmgc2  31283  mgcf1o  31290  isomnd  31336  omndadd  31341  omndmul  31349  ogrpinvlt  31358  gsumle  31359  isinftm  31444  xrmulc1cn  31889  lmdvg  31912  nexple  31986  faeval  32223  brfae  32225  inelcarsg  32287  carsgsigalem  32291  carsgclctunlem2  32295  carsgclctun  32297  hgt750lemc  32636  hgt750lemd  32637  hgt749d  32638  sconnpht  33200  snmlval  33302  satfv1lem  33333  satfv1  33334  satfv0fun  33342  satfv0fvfmla0  33384  lediv2aALT  33644  faclim  33721  poseq  33811  sltval2  33868  sltres  33874  nolesgn2o  33883  nogesgn1o  33885  nodense  33904  nolt02o  33907  nogt01o  33908  noresle  33909  nosupbnd2lem1  33927  nosupbnd2  33928  noinfbnd2lem1  33942  noinfbnd2  33943  fvtransport  34343  idinside  34395  btwnconn1lem7  34404  btwnconn1lem11  34408  btwnconn1lem12  34409  nn0prpwlem  34520  bj-opabco  35368  poimirlem29  35815  heicant  35821  itg2addnclem  35837  itg2addnclem3  35839  itg2gt0cn  35841  ftc1anclem6  35864  ftc1anc  35867  ftc2nc  35868  dvasin  35870  areacirclem1  35874  seqpo  35914  incsequz  35915  metf1o  35922  mettrifi  35924  cntotbnd  35963  heiborlem4  35981  heiborlem6  35983  heiborlem10  35987  bfplem1  35989  bfplem2  35990  isopos  37201  oplecon3b  37221  atlatle  37341  4at2  37635  pmaple  37782  islaut  38104  lautcnvle  38110  lautco  38118  ltrncnvel  38163  cdlemeg49lebilem  38560  cdlemg17h  38689  tendoset  38780  tendotp  38782  cdlemk39s  38960  lcmineqlem23  40066  lcmineqlem  40067  intlewftc  40076  aks4d1p1p4  40086  dvle2  40087  aks4d1p8d2  40100  aks4d1p9  40103  aks4d1  40104  2ap1caineq  40108  sticksstones1  40109  sticksstones2  40110  sticksstones3  40111  sticksstones8  40116  sticksstones10  40118  sticksstones11  40119  sticksstones12a  40120  sticksstones15  40124  factwoffsmonot  40170  brif12  40207  dvdsexpnn0  40348  dvdsexpb  40349  reltsub1  40376  irrapxlem2  40652  irrapxlem4  40654  irrapxlem5  40655  irrapxlem6  40656  pellexlem3  40660  monotuz  40770  monotoddzzfi  40771  monotoddzz  40772  jm2.17a  40789  jm2.17b  40790  rmygeid  40793  rmydioph  40843  expdiophlem1  40850  expdiophlem2  40851  ttac  40865  fnwe2lem2  40883  relexp01min  41328  cvgdvgrat  41938  monoords  42843  supxrgelem  42883  supxrge  42884  abslt2sqd  42906  ltmulneg  42939  ltdiv23neg  42941  monoordxrv  43029  monoordxr  43030  monoord2xrv  43031  monoord2xr  43032  evthiccabs  43041  sqrlearg  43098  climinf  43154  climinff  43159  limsupres  43253  climinf2  43255  climinf2mpt  43262  climinfmpt  43263  supcnvlimsup  43288  liminfval2  43316  liminflelimsuplem  43323  liminfltlem  43352  fprodsubrecnncnvlem  43455  fprodaddrecnncnvlem  43457  ioodvbdlimc1lem1  43479  ioodvbdlimc1lem2  43480  ioodvbdlimc2lem  43482  iblspltprt  43521  itgspltprt  43527  stoweidlem3  43551  fourierdlem2  43657  fourierdlem3  43658  fourierdlem11  43666  fourierdlem12  43667  fourierdlem15  43670  fourierdlem34  43689  fourierdlem41  43696  fourierdlem48  43702  fourierdlem49  43703  fourierdlem79  43733  fourierdlem83  43737  fourierdlem89  43743  fourierdlem91  43745  fourierdlem100  43754  fourierdlem107  43761  fourierdlem109  43763  fourierdlem112  43766  etransclem31  43813  etransclem32  43814  rrndistlt  43838  ioorrnopn  43853  ioorrnopnxrlem  43854  sge0less  43937  sge0le  43952  sge0split  43954  sge0lempt  43955  sge0iunmptlemre  43960  sge0isum  43972  sge0seq  43991  meaiuninclem  44025  meaiininclem  44031  meaiininc  44032  isome  44039  omeunile  44050  omeiunlempt  44065  carageniuncllem2  44067  0ome  44074  isomenndlem  44075  isomennd  44076  ovnsslelem  44105  ovnssle  44106  ovnsubadd  44117  hsphoidmvle2  44130  hsphoidmvle  44131  hoidmvval0  44132  hoidmv1lelem1  44136  hoidmv1lelem2  44137  hoidmv1lelem3  44138  hoidmv1le  44139  hoidmvlelem1  44140  hoidmvlelem2  44141  hoidmvlelem3  44142  hoidmvlelem4  44143  hoidmvlelem5  44144  hoidmvle  44145  hoidifhspdmvle  44165  hspmbllem2  44172  hspmbl  44174  ovnsubadd2lem  44190  ovolval4lem2  44195  ovolval4  44196  ovolval5lem2  44198  vonioolem2  44226  vonioo  44227  vonicclem2  44229  vonicc  44230  smfid  44297  smflimlem3  44318  2elfz2melfz  44821  smonoord  44834  iccpart  44879  iccpartimp  44880  iccpartres  44881  sqrtpwpw2p  45001  ismgmALT  45428  iscmgmALT  45429  issgrpALT  45430  iscsgrpALT  45431  lindslinindsimp2lem5  45814  rrx2plordisom  46080  aacllem  46516  natglobalincr  46523  tworepnotupword  46532