Theorem breq12d 5108

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

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

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 2705

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 2712  df-cleq 2725  df-clel 2808  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-br 5096

This theorem is referenced by:  breq123d  5109  3brtr3d  5126  3brtr4d  5127  sbcbr  5150  pocl  5537  csbcnvgALT  5831  cnvpo  6242  sbcfung  6513  isoeq1  7260  isocnv  7273  isotr  7279  caovordig  7560  caovordg  7562  caovord2d  7564  caovord  7566  ofrfvalg  7627  ofrval  7631  ofrfval2  7640  caofref  7650  fnwelem  8070  poseq  8097  fundmeng  8964  enrefnn  8978  xpsneng  8985  xpcomeng  8992  xpdom2g  8996  limensuc  9077  infensuc  9078  pssnn  9088  unxpdom  9153  dif1ennnALT  9171  unfilem3  9201  fodomfi  9206  domunfican  9216  fodomfiOLD  9224  marypha1lem  9327  infsupprpr  9400  wemaplem1  9442  wemaplem2  9443  wemapwe  9597  ssttrcl  9615  ttrcltr  9616  ttrclss  9620  dmttrcl  9621  rnttrcl  9622  ttrclselem2  9626  dif1card  9911  infxpenlem  9914  nnadju  10099  pwsdompw  10104  infmap2  10118  sornom  10178  isfin5  10200  isfin6  10201  domtriomlem  10343  axdc2lem  10349  axdclem2  10421  pwcfsdom  10484  cfpwsdom  10485  alephom  10486  fpwwe2lem6  10537  fpwwe2lem8  10539  tskcard  10682  ordpipq  10843  adderpqlem  10855  mulerpqlem  10856  mulcanenq  10861  lterpq  10871  ltanq  10872  ltmnq  10873  ltaddnq  10875  ltrnq  10880  archnq  10881  reclem4pr  10951  ltasr  11001  sqgt0sr  11007  axpre-ltadd  11068  axpre-mulgt0  11069  ltadd1  11594  leadd2  11596  ltmul2  11982  lemul2  11984  lemul1a  11985  ltdiv1  11996  ltdiv2  12018  lediv2  12022  div4p1lem1div2  12386  nn0ledivnn  13015  xleadd1  13164  xltadd2  13166  xsubge0  13170  xlemul1a  13197  xlemul1  13199  xlemul2  13200  xltmul2  13202  ltdifltdiv  13748  fzennn  13885  monoord  13949  monoord2  13950  expmordi  14084  ltexp2r  14090  leexp1a  14092  sqlecan  14126  bernneq  14146  faclbnd  14207  faclbnd3  14209  faclbnd4lem1  14210  faclbnd4lem2  14211  faclbnd4lem3  14212  faclbnd4lem4  14213  faclbnd6  14216  facubnd  14217  rlimcld2  15495  isercoll2  15586  climsup  15587  iseraltlem2  15600  fsumabs  15718  fsumrlim  15728  climcndslem1  15766  climcndslem2  15767  supcvg  15773  geomulcvg  15793  cvgrat  15800  ntrivcvgtail  15817  ruclem2  16151  ruclem8  16156  addmodlteqALT  16246  fproddvdsd  16256  sadcaddlem  16378  sadcadd  16379  nn0seqcvgd  16491  algcvg  16497  algcvga  16500  eucalgcvga  16507  isprm5  16628  qnumgt0  16671  pcprendvds2  16763  pcpremul  16765  pcadd2  16812  prmreclem4  16841  prmreclem5  16842  prmreclem6  16843  2expltfac  17014  xpsle  17493  mreexexlemd  17560  issubc  17752  latjlej2  18370  latmlem2  18386  ischn  18523  chnltm1  18525  chnind  18537  chnub  18538  sylow1lem3  19522  isslw  19530  fislw  19547  efgi  19641  lt6abl  19817  ablfac1eu  19997  isomnd  20045  omndadd  20050  omndmul  20057  ogrpinvlt  20066  gsumle  20067  isabv  20736  abvtri  20747  psdmul  22091  cayleyhamilton1  22817  isucn  24202  ispsmet  24229  psmettri2  24234  ismet  24248  isxmet  24249  xmettri2  24265  imasdsf1olem  24298  imasf1oxmet  24300  blvalps  24310  blval  24311  comet  24438  stdbdxmet  24440  nrmmetd  24499  tngngp  24579  tngngp3  24581  nmofval  24639  nmolb2d  24643  nmoi  24653  nmoix  24654  icopnfhmeo  24878  xrhmeo  24881  evth2  24896  pi1grplem  24986  minveclem6  25371  ovolfiniun  25439  ovoliunlem3  25442  voliunlem3  25490  ioombl1  25500  mbfmax  25587  mbfpos  25589  itg1climres  25652  mbfi1fseqlem2  25654  mbfi1fseqlem6  25658  mbfi1fseq  25659  mbfmullem  25663  itg2split  25687  itg2monolem1  25688  itg2monolem3  25690  itg2mono  25691  itg2i1fseqle  25692  itg2i1fseq  25693  itg2i1fseq2  25694  itg2addlem  25696  rolle  25931  dvlip  25935  c1lip1  25939  dvcnvrelem1  25959  dvcvx  25962  ply1divex  26079  q1pval  26097  fta1glem2  26111  fta1g  26112  fta1b  26114  plydivlem3  26240  fta1lem  26252  fta1  26253  aalioulem3  26279  aalioulem4  26280  aaliou3lem2  26288  aaliou3lem8  26290  aaliou3lem9  26295  ulmdvlem1  26346  ulmdvlem3  26348  abelthlem2  26379  abelthlem7a  26384  argrege0  26557  cxplt  26640  cxplea  26642  cxple2  26643  cxplt3  26646  logbleb  26730  logblt  26731  rlimcxp  26921  scvxcvx  26933  jensenlem2  26935  ftalem3  27022  ftalem7  27026  vmalelog  27153  chtub  27160  chpchtsum  27167  bclbnd  27228  efexple  27229  bposlem5  27236  bposlem6  27237  bposlem7  27238  lgsdilem  27272  2lgslem1a2  27338  2sqreuop  27410  2sqreuopnn  27411  2sqreuoplt  27412  2sqreuopltb  27413  2sqreuopnnlt  27414  2sqreuopnnltb  27415  dchrisumlem3  27439  dchrmusumlema  27441  dchrmusum2  27442  dchrvmasumlem2  27446  dchrvmasumlema  27448  dchrvmasumiflem1  27449  dchrisum0flblem2  27457  dchrisum0flb  27458  dchrisum0lema  27462  dchrisum0lem1b  27463  dchrisum0lem2  27466  pntrlog2bndlem2  27526  pntibndlem2  27539  pntlemf  27553  ostth2lem1  27566  qabvle  27573  sltval2  27605  sltres  27611  nolesgn2o  27620  nogesgn1o  27622  nodense  27641  nolt02o  27644  nogt01o  27645  noresle  27646  nosupbnd2lem1  27664  nosupbnd2  27665  noinfbnd2lem1  27679  noinfbnd2  27680  addsproplem1  27922  addsprop  27929  sltadd2im  27939  sleadd2im  27941  sleadd1  27942  sleadd2  27943  sltadd1  27945  sltsub1  28026  sltsub2  28027  sltsubsubbd  28033  sltsubsub2bd  28034  posdifsd  28047  subsge0d  28049  mulsproplemcbv  28064  mulsproplem1  28065  mulsprop  28079  slemuld  28087  sltmul1d  28122  sltmulneg1d  28125  sltmulneg2d  28126  slemul1ad  28131  zsoring  28342  pw2gt0divsd  28378  pw2ge0divsd  28379  legso  28587  iscgra  28797  isleag  28835  iseqlg  28855  brbtwn2  28894  axlowdim  28950  ewlksfval  29591  isnvlem  30601  nvtri  30661  nmlnoubi  30787  nmblolbii  30790  nmblolbi  30791  blocnilem  30795  sii  30845  ubthlem2  30862  minvecolem3  30867  minvecolem5  30872  minvecolem6  30873  norm-ii  31129  norm3dif  31141  norm3adifi  31144  bcs  31172  pjnorm  31715  pjnel  31717  nmbdoplbi  32015  nmbdoplb  32016  nmcoplb  32021  lnconi  32024  nmbdfnlb  32041  nmcfnlb  32045  pjdifnormi  32158  mdslmd2i  32321  cvmd  32327  cvexch  32365  cdj1i  32424  cdj3lem1  32425  cdj3lem2b  32428  cdj3lem3b  32431  cdj3i  32432  fnfvor  32603  ofrco  32604  isoun  32694  nexple  32838  ismnt  32975  mgcmntco  32986  dfmgc2lem  32987  dfmgc2  32988  mgcf1o  32995  isinftm  33161  rlocaddval  33246  rlocmulval  33247  fldext2chn  33752  constrextdg2lem  33772  constrext2chn  33783  xrmulc1cn  33954  lmdvg  33977  faeval  34270  brfae  34272  inelcarsg  34335  carsgsigalem  34339  carsgclctunlem2  34343  carsgclctun  34345  hgt750lemc  34671  hgt750lemd  34672  hgt749d  34673  fineqvnttrclse  35155  sconnpht  35284  snmlval  35386  satfv1lem  35417  satfv1  35418  satfv0fun  35426  satfv0fvfmla0  35468  lediv2aALT  35732  faclim  35801  fvtransport  36087  idinside  36139  btwnconn1lem7  36148  btwnconn1lem11  36152  btwnconn1lem12  36153  ditgeq123dv  36276  cbvditgdavw2  36353  nn0prpwlem  36377  weiunlem1  36517  weiunfrlem  36519  bj-opabco  37243  poimirlem29  37699  heicant  37705  itg2addnclem  37721  itg2addnclem3  37723  itg2gt0cn  37725  ftc1anclem6  37748  ftc1anc  37751  ftc2nc  37752  dvasin  37754  areacirclem1  37758  seqpo  37797  incsequz  37798  metf1o  37805  mettrifi  37807  cntotbnd  37846  heiborlem4  37864  heiborlem6  37866  heiborlem10  37870  bfplem1  37872  bfplem2  37873  isopos  39289  oplecon3b  39309  atlatle  39429  4at2  39723  pmaple  39870  islaut  40192  lautcnvle  40198  lautco  40206  ltrncnvel  40251  cdlemeg49lebilem  40648  cdlemg17h  40777  tendoset  40868  tendotp  40870  cdlemk39s  41048  lcmineqlem23  42154  lcmineqlem  42155  intlewftc  42164  aks4d1p1p4  42174  dvle2  42175  aks4d1p8d2  42188  aks4d1p9  42191  aks4d1  42192  2ap1caineq  42248  sticksstones1  42249  sticksstones2  42250  sticksstones3  42251  sticksstones8  42256  sticksstones10  42258  sticksstones11  42259  sticksstones12a  42260  sticksstones15  42264  aks6d1c7lem3  42285  unitscyglem1  42298  brif12  42333  dvdsexpnn0  42442  dvdsexpb  42443  reltsub1  42494  irrapxlem2  42930  irrapxlem4  42932  irrapxlem5  42933  irrapxlem6  42934  pellexlem3  42938  monotuz  43048  monotoddzzfi  43049  monotoddzz  43050  jm2.17a  43067  jm2.17b  43068  rmygeid  43071  rmydioph  43121  expdiophlem1  43128  expdiophlem2  43129  ttac  43143  fnwe2lem2  43158  relexp01min  43820  cvgdvgrat  44420  relpeq1  45051  monoords  45412  supxrgelem  45450  supxrge  45451  abslt2sqd  45473  ltmulneg  45504  ltdiv23neg  45506  monoordxrv  45593  monoordxr  45594  monoord2xrv  45595  monoord2xr  45596  evthiccabs  45610  sqrlearg  45667  climinf  45720  climinff  45725  limsupres  45817  climinf2  45819  climinf2mpt  45826  climinfmpt  45827  supcnvlimsup  45852  liminfval2  45880  liminfltlem  45916  fprodsubrecnncnvlem  46019  fprodaddrecnncnvlem  46021  ioodvbdlimc1lem1  46043  ioodvbdlimc1lem2  46044  ioodvbdlimc2lem  46046  iblspltprt  46085  itgspltprt  46091  stoweidlem3  46115  fourierdlem2  46221  fourierdlem3  46222  fourierdlem11  46230  fourierdlem12  46231  fourierdlem15  46234  fourierdlem34  46253  fourierdlem41  46260  fourierdlem48  46266  fourierdlem49  46267  fourierdlem79  46297  fourierdlem83  46301  fourierdlem89  46307  fourierdlem91  46309  fourierdlem100  46318  fourierdlem107  46325  fourierdlem109  46327  fourierdlem112  46330  etransclem31  46377  etransclem32  46378  rrndistlt  46402  ioorrnopn  46417  ioorrnopnxrlem  46418  sge0less  46504  sge0le  46519  sge0split  46521  sge0lempt  46522  sge0iunmptlemre  46527  sge0isum  46539  sge0seq  46558  meaiuninclem  46592  meaiininclem  46598  meaiininc  46599  isome  46606  omeunile  46617  omeiunlempt  46632  carageniuncllem2  46634  0ome  46641  isomenndlem  46642  isomennd  46643  ovnssle  46673  ovnsubadd  46684  hsphoidmvle2  46697  hsphoidmvle  46698  hoidmvval0  46699  hoidmv1lelem1  46703  hoidmv1lelem2  46704  hoidmv1lelem3  46705  hoidmv1le  46706  hoidmvlelem1  46707  hoidmvlelem2  46708  hoidmvlelem3  46709  hoidmvlelem4  46710  hoidmvlelem5  46711  hoidmvle  46712  hoidifhspdmvle  46732  hspmbllem2  46739  hspmbl  46741  ovnsubadd2lem  46757  ovolval4lem2  46762  ovolval4  46763  ovolval5lem2  46765  vonioolem2  46793  vonioo  46794  vonicclem2  46796  vonicc  46797  smfid  46864  smflimlem3  46885  ormkglobd  46987  natglobalincr  46989  chnerlem1  46994  squeezedltsq  47000  2elfz2melfz  47432  smonoord  47485  iccpart  47530  iccpartimp  47531  iccpartres  47532  sqrtpwpw2p  47652  grlicsym  48127  grlictr  48129  ismgmALT  48337  iscmgmALT  48338  issgrpALT  48339  iscsgrpALT  48340  lindslinindsimp2lem5  48577  rrx2plordisom  48838  aacllem  49916