Theorem breq12d 5115

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

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

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-br 5103

This theorem is referenced by:  breq123d  5116  3brtr3d  5133  3brtr4d  5134  sbcbr  5157  pocl  5547  csbcnvgALT  5838  cnvpo  6248  sbcfung  6524  isoeq1  7274  isocnv  7287  isotr  7293  caovordig  7574  caovordg  7576  caovord2d  7578  caovord  7580  ofrfvalg  7641  ofrval  7645  ofrfval2  7654  caofref  7664  fnwelem  8087  poseq  8114  fundmeng  8980  enrefnn  8995  xpsneng  9003  xpcomeng  9010  xpdom2g  9014  limensuc  9095  infensuc  9096  pssnn  9109  unxpdom  9176  dif1ennnALT  9198  unfilem3  9232  fodomfi  9237  domunfican  9248  fodomfiOLD  9257  marypha1lem  9360  infsupprpr  9433  wemaplem1  9475  wemaplem2  9476  wemapwe  9626  ssttrcl  9644  ttrcltr  9645  ttrclss  9649  dmttrcl  9650  rnttrcl  9651  ttrclselem2  9655  dif1card  9939  infxpenlem  9942  nnadju  10127  pwsdompw  10132  infmap2  10146  sornom  10206  isfin5  10228  isfin6  10229  domtriomlem  10371  axdc2lem  10377  axdclem2  10449  pwcfsdom  10512  cfpwsdom  10513  alephom  10514  fpwwe2lem6  10565  fpwwe2lem8  10567  tskcard  10710  ordpipq  10871  adderpqlem  10883  mulerpqlem  10884  mulcanenq  10889  lterpq  10899  ltanq  10900  ltmnq  10901  ltaddnq  10903  ltrnq  10908  archnq  10909  reclem4pr  10979  ltasr  11029  sqgt0sr  11035  axpre-ltadd  11096  axpre-mulgt0  11097  ltadd1  11621  leadd2  11623  ltmul2  12009  lemul2  12011  lemul1a  12012  ltdiv1  12023  ltdiv2  12045  lediv2  12049  div4p1lem1div2  12413  nn0ledivnn  13042  xleadd1  13191  xltadd2  13193  xsubge0  13197  xlemul1a  13224  xlemul1  13226  xlemul2  13227  xltmul2  13229  ltdifltdiv  13772  fzennn  13909  monoord  13973  monoord2  13974  expmordi  14108  ltexp2r  14114  leexp1a  14116  sqlecan  14150  bernneq  14170  faclbnd  14231  faclbnd3  14233  faclbnd4lem1  14234  faclbnd4lem2  14235  faclbnd4lem3  14236  faclbnd4lem4  14237  faclbnd6  14240  facubnd  14241  rlimcld2  15520  isercoll2  15611  climsup  15612  iseraltlem2  15625  fsumabs  15743  fsumrlim  15753  climcndslem1  15791  climcndslem2  15792  supcvg  15798  geomulcvg  15818  cvgrat  15825  ntrivcvgtail  15842  ruclem2  16176  ruclem8  16181  addmodlteqALT  16271  fproddvdsd  16281  sadcaddlem  16403  sadcadd  16404  nn0seqcvgd  16516  algcvg  16522  algcvga  16525  eucalgcvga  16532  isprm5  16653  qnumgt0  16696  pcprendvds2  16788  pcpremul  16790  pcadd2  16837  prmreclem4  16866  prmreclem5  16867  prmreclem6  16868  2expltfac  17039  xpsle  17518  mreexexlemd  17585  issubc  17777  latjlej2  18395  latmlem2  18411  sylow1lem3  19514  isslw  19522  fislw  19539  efgi  19633  lt6abl  19809  ablfac1eu  19989  isomnd  20037  omndadd  20042  omndmul  20049  ogrpinvlt  20058  gsumle  20059  isabv  20731  abvtri  20742  psdmul  22086  cayleyhamilton1  22812  isucn  24198  ispsmet  24225  psmettri2  24230  ismet  24244  isxmet  24245  xmettri2  24261  imasdsf1olem  24294  imasf1oxmet  24296  blvalps  24306  blval  24307  comet  24434  stdbdxmet  24436  nrmmetd  24495  tngngp  24575  tngngp3  24577  nmofval  24635  nmolb2d  24639  nmoi  24649  nmoix  24650  icopnfhmeo  24874  xrhmeo  24877  evth2  24892  pi1grplem  24982  minveclem6  25367  ovolfiniun  25435  ovoliunlem3  25438  voliunlem3  25486  ioombl1  25496  mbfmax  25583  mbfpos  25585  itg1climres  25648  mbfi1fseqlem2  25650  mbfi1fseqlem6  25654  mbfi1fseq  25655  mbfmullem  25659  itg2split  25683  itg2monolem1  25684  itg2monolem3  25686  itg2mono  25687  itg2i1fseqle  25688  itg2i1fseq  25689  itg2i1fseq2  25690  itg2addlem  25692  rolle  25927  dvlip  25931  c1lip1  25935  dvcnvrelem1  25955  dvcvx  25958  ply1divex  26075  q1pval  26093  fta1glem2  26107  fta1g  26108  fta1b  26110  plydivlem3  26236  fta1lem  26248  fta1  26249  aalioulem3  26275  aalioulem4  26276  aaliou3lem2  26284  aaliou3lem8  26286  aaliou3lem9  26291  ulmdvlem1  26342  ulmdvlem3  26344  abelthlem2  26375  abelthlem7a  26380  argrege0  26553  cxplt  26636  cxplea  26638  cxple2  26639  cxplt3  26642  logbleb  26726  logblt  26727  rlimcxp  26917  scvxcvx  26929  jensenlem2  26931  ftalem3  27018  ftalem7  27022  vmalelog  27149  chtub  27156  chpchtsum  27163  bclbnd  27224  efexple  27225  bposlem5  27232  bposlem6  27233  bposlem7  27234  lgsdilem  27268  2lgslem1a2  27334  2sqreuop  27406  2sqreuopnn  27407  2sqreuoplt  27408  2sqreuopltb  27409  2sqreuopnnlt  27410  2sqreuopnnltb  27411  dchrisumlem3  27435  dchrmusumlema  27437  dchrmusum2  27438  dchrvmasumlem2  27442  dchrvmasumlema  27444  dchrvmasumiflem1  27445  dchrisum0flblem2  27453  dchrisum0flb  27454  dchrisum0lema  27458  dchrisum0lem1b  27459  dchrisum0lem2  27462  pntrlog2bndlem2  27522  pntibndlem2  27535  pntlemf  27549  ostth2lem1  27562  qabvle  27569  sltval2  27601  sltres  27607  nolesgn2o  27616  nogesgn1o  27618  nodense  27637  nolt02o  27640  nogt01o  27641  noresle  27642  nosupbnd2lem1  27660  nosupbnd2  27661  noinfbnd2lem1  27675  noinfbnd2  27676  addsproplem1  27916  addsprop  27923  sltadd2im  27933  sleadd2im  27935  sleadd1  27936  sleadd2  27937  sltadd1  27939  sltsub1  28020  sltsub2  28021  sltsubsubbd  28027  sltsubsub2bd  28028  posdifsd  28041  subsge0d  28043  mulsproplemcbv  28058  mulsproplem1  28059  mulsprop  28073  slemuld  28081  sltmul1d  28116  sltmulneg1d  28119  sltmulneg2d  28120  slemul1ad  28125  zsoring  28336  pw2gt0divsd  28372  pw2ge0divsd  28373  legso  28579  iscgra  28789  isleag  28827  iseqlg  28847  brbtwn2  28885  axlowdim  28941  ewlksfval  29582  isnvlem  30589  nvtri  30649  nmlnoubi  30775  nmblolbii  30778  nmblolbi  30779  blocnilem  30783  sii  30833  ubthlem2  30850  minvecolem3  30855  minvecolem5  30860  minvecolem6  30861  norm-ii  31117  norm3dif  31129  norm3adifi  31132  bcs  31160  pjnorm  31703  pjnel  31705  nmbdoplbi  32003  nmbdoplb  32004  nmcoplb  32009  lnconi  32012  nmbdfnlb  32029  nmcfnlb  32033  pjdifnormi  32146  mdslmd2i  32309  cvmd  32315  cvexch  32353  cdj1i  32412  cdj3lem1  32413  cdj3lem2b  32416  cdj3lem3b  32419  cdj3i  32420  isoun  32675  nexple  32819  ismnt  32955  mgcmntco  32966  dfmgc2lem  32967  dfmgc2  32968  mgcf1o  32975  ischn  32978  chnltm1  32980  chnind  32983  chnub  32984  isinftm  33150  rlocaddval  33235  rlocmulval  33236  fldext2chn  33711  constrextdg2lem  33731  constrext2chn  33742  xrmulc1cn  33913  lmdvg  33936  faeval  34229  brfae  34231  inelcarsg  34295  carsgsigalem  34299  carsgclctunlem2  34303  carsgclctun  34305  hgt750lemc  34631  hgt750lemd  34632  hgt749d  34633  sconnpht  35209  snmlval  35311  satfv1lem  35342  satfv1  35343  satfv0fun  35351  satfv0fvfmla0  35393  lediv2aALT  35657  faclim  35726  fvtransport  36013  idinside  36065  btwnconn1lem7  36074  btwnconn1lem11  36078  btwnconn1lem12  36079  ditgeq123dv  36202  cbvditgdavw2  36279  nn0prpwlem  36303  weiunlem1  36443  weiunfrlem  36445  bj-opabco  37169  poimirlem29  37636  heicant  37642  itg2addnclem  37658  itg2addnclem3  37660  itg2gt0cn  37662  ftc1anclem6  37685  ftc1anc  37688  ftc2nc  37689  dvasin  37691  areacirclem1  37695  seqpo  37734  incsequz  37735  metf1o  37742  mettrifi  37744  cntotbnd  37783  heiborlem4  37801  heiborlem6  37803  heiborlem10  37807  bfplem1  37809  bfplem2  37810  isopos  39166  oplecon3b  39186  atlatle  39306  4at2  39601  pmaple  39748  islaut  40070  lautcnvle  40076  lautco  40084  ltrncnvel  40129  cdlemeg49lebilem  40526  cdlemg17h  40655  tendoset  40746  tendotp  40748  cdlemk39s  40926  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  brif12  42206  dvdsexpnn0  42315  dvdsexpb  42316  reltsub1  42367  irrapxlem2  42804  irrapxlem4  42806  irrapxlem5  42807  irrapxlem6  42808  pellexlem3  42812  monotuz  42923  monotoddzzfi  42924  monotoddzz  42925  jm2.17a  42942  jm2.17b  42943  rmygeid  42946  rmydioph  42996  expdiophlem1  43003  expdiophlem2  43004  ttac  43018  fnwe2lem2  43033  relexp01min  43695  cvgdvgrat  44295  relpeq1  44927  monoords  45288  supxrgelem  45326  supxrge  45327  abslt2sqd  45349  ltmulneg  45381  ltdiv23neg  45383  monoordxrv  45470  monoordxr  45471  monoord2xrv  45472  monoord2xr  45473  evthiccabs  45487  sqrlearg  45544  climinf  45597  climinff  45602  limsupres  45696  climinf2  45698  climinf2mpt  45705  climinfmpt  45706  supcnvlimsup  45731  liminfval2  45759  liminfltlem  45795  fprodsubrecnncnvlem  45898  fprodaddrecnncnvlem  45900  ioodvbdlimc1lem1  45922  ioodvbdlimc1lem2  45923  ioodvbdlimc2lem  45925  iblspltprt  45964  itgspltprt  45970  stoweidlem3  45994  fourierdlem2  46100  fourierdlem3  46101  fourierdlem11  46109  fourierdlem12  46110  fourierdlem15  46113  fourierdlem34  46132  fourierdlem41  46139  fourierdlem48  46145  fourierdlem49  46146  fourierdlem79  46176  fourierdlem83  46180  fourierdlem89  46186  fourierdlem91  46188  fourierdlem100  46197  fourierdlem107  46204  fourierdlem109  46206  fourierdlem112  46209  etransclem31  46256  etransclem32  46257  rrndistlt  46281  ioorrnopn  46296  ioorrnopnxrlem  46297  sge0less  46383  sge0le  46398  sge0split  46400  sge0lempt  46401  sge0iunmptlemre  46406  sge0isum  46418  sge0seq  46437  meaiuninclem  46471  meaiininclem  46477  meaiininc  46478  isome  46485  omeunile  46496  omeiunlempt  46511  carageniuncllem2  46513  0ome  46520  isomenndlem  46521  isomennd  46522  ovnssle  46552  ovnsubadd  46563  hsphoidmvle2  46576  hsphoidmvle  46577  hoidmvval0  46578  hoidmv1lelem1  46582  hoidmv1lelem2  46583  hoidmv1lelem3  46584  hoidmv1le  46585  hoidmvlelem1  46586  hoidmvlelem2  46587  hoidmvlelem3  46588  hoidmvlelem4  46589  hoidmvlelem5  46590  hoidmvle  46591  hoidifhspdmvle  46611  hspmbllem2  46618  hspmbl  46620  ovnsubadd2lem  46636  ovolval4lem2  46641  ovolval4  46642  ovolval5lem2  46644  vonioolem2  46672  vonioo  46673  vonicclem2  46675  vonicc  46676  smfid  46743  smflimlem3  46764  ormkglobd  46866  natglobalincr  46868  tworepnotupword  46877  squeezedltsq  46880  2elfz2melfz  47312  smonoord  47365  iccpart  47410  iccpartimp  47411  iccpartres  47412  sqrtpwpw2p  47532  grlicsym  47998  grlictr  48000  ismgmALT  48204  iscmgmALT  48205  issgrpALT  48206  iscsgrpALT  48207  lindslinindsimp2lem5  48444  rrx2plordisom  48705  aacllem  49783