Theorem breq12d 5052

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1543   class class class wbr 5039

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-rab 3060  df-v 3400  df-dif 3856  df-un 3858  df-nul 4224  df-if 4426  df-sn 4528  df-pr 4530  df-op 4534  df-br 5040

This theorem is referenced by:  breq123d  5053  3brtr3d  5070  3brtr4d  5071  sbcbr  5094  pocl  5460  poclOLD  5461  csbcnvgALT  5738  cnvpo  6130  sbcfung  6382  isoeq1  7104  isocnv  7117  isotr  7123  caovordig  7391  caovordg  7393  caovord2d  7395  caovord  7397  ofrfvalg  7454  ofrval  7458  ofrfval2  7467  caofref  7475  fnwelem  7876  fundmeng  8687  enrefnn  8702  xpsneng  8708  xpcomeng  8715  xpdom2g  8719  limensuc  8801  infensuc  8802  pssnn  8824  unxpdom  8861  pssnnOLD  8872  dif1enOLD  8885  unfilem3  8915  unfiOLD  8916  domunfican  8922  fodomfi  8927  marypha1lem  9027  infsupprpr  9098  wemaplem1  9140  wemaplem2  9141  wemapwe  9290  dif1card  9589  infxpenlem  9592  nnadju  9776  pwsdompw  9783  infmap2  9797  sornom  9856  isfin5  9878  isfin6  9879  domtriomlem  10021  axdc2lem  10027  axdclem2  10099  pwcfsdom  10162  cfpwsdom  10163  alephom  10164  fpwwe2lem6  10215  fpwwe2lem8  10217  tskcard  10360  ordpipq  10521  adderpqlem  10533  mulerpqlem  10534  mulcanenq  10539  lterpq  10549  ltanq  10550  ltmnq  10551  ltaddnq  10553  ltrnq  10558  archnq  10559  reclem4pr  10629  ltasr  10679  sqgt0sr  10685  axpre-ltadd  10746  axpre-mulgt0  10747  ltadd1  11264  leadd2  11266  ltmul2  11648  lemul2  11650  lemul1a  11651  ltdiv1  11661  ltdiv2  11683  lediv2  11687  div4p1lem1div2  12050  nn0ledivnn  12664  xleadd1  12810  xltadd2  12812  xsubge0  12816  xlemul1a  12843  xlemul1  12845  xlemul2  12846  xltmul2  12848  ltdifltdiv  13374  fzennn  13506  monoord  13571  monoord2  13572  expmordi  13702  ltexp2r  13708  leexp1a  13710  sqlecan  13742  bernneq  13761  faclbnd  13821  faclbnd3  13823  faclbnd4lem1  13824  faclbnd4lem2  13825  faclbnd4lem3  13826  faclbnd4lem4  13827  faclbnd6  13830  facubnd  13831  rlimcld2  15104  isercoll2  15197  climsup  15198  iseraltlem2  15211  fsumabs  15328  fsumrlim  15338  climcndslem1  15376  climcndslem2  15377  supcvg  15383  geomulcvg  15403  cvgrat  15410  ntrivcvgtail  15427  ruclem2  15756  ruclem8  15761  addmodlteqALT  15849  fproddvdsd  15859  sadcaddlem  15979  sadcadd  15980  nn0seqcvgd  16090  algcvg  16096  algcvga  16099  eucalgcvga  16106  isprm5  16227  qnumgt0  16269  pcprendvds2  16357  pcpremul  16359  pcadd2  16406  prmreclem4  16435  prmreclem5  16436  prmreclem6  16437  2expltfac  16609  xpsle  17038  mreexexlemd  17101  issubc  17295  latjlej2  17914  latmlem2  17930  sylow1lem3  18943  isslw  18951  fislw  18968  efgi  19063  lt6abl  19234  ablfac1eu  19414  isabv  19809  abvtri  19820  cayleyhamilton1  21743  isucn  23129  ispsmet  23156  psmettri2  23161  ismet  23175  isxmet  23176  xmettri2  23192  imasdsf1olem  23225  imasf1oxmet  23227  blvalps  23237  blval  23238  comet  23365  stdbdxmet  23367  nrmmetd  23426  tngngp  23506  tngngp3  23508  nmofval  23566  nmolb2d  23570  nmoi  23580  nmoix  23581  icopnfhmeo  23794  xrhmeo  23797  evth2  23811  pi1grplem  23900  minveclem6  24285  ovolfiniun  24352  ovoliunlem3  24355  voliunlem3  24403  ioombl1  24413  mbfmax  24500  mbfpos  24502  itg1climres  24566  mbfi1fseqlem2  24568  mbfi1fseqlem6  24572  mbfi1fseq  24573  mbfmullem  24577  itg2split  24601  itg2monolem1  24602  itg2monolem3  24604  itg2mono  24605  itg2i1fseqle  24606  itg2i1fseq  24607  itg2i1fseq2  24608  itg2addlem  24610  rolle  24841  dvlip  24844  c1lip1  24848  dvcnvrelem1  24868  dvcvx  24871  ply1divex  24988  q1pval  25005  fta1glem2  25018  fta1g  25019  fta1b  25021  plydivlem3  25142  fta1lem  25154  fta1  25155  aalioulem3  25181  aalioulem4  25182  aaliou3lem2  25190  aaliou3lem8  25192  aaliou3lem9  25197  ulmdvlem1  25246  ulmdvlem3  25248  abelthlem2  25278  abelthlem7a  25283  argrege0  25453  cxplt  25536  cxplea  25538  cxple2  25539  cxplt3  25542  logbleb  25620  logblt  25621  rlimcxp  25810  scvxcvx  25822  jensenlem2  25824  ftalem3  25911  ftalem7  25915  vmalelog  26040  chtub  26047  chpchtsum  26054  bclbnd  26115  efexple  26116  bposlem5  26123  bposlem6  26124  bposlem7  26125  lgsdilem  26159  2lgslem1a2  26225  2sqreuop  26297  2sqreuopnn  26298  2sqreuoplt  26299  2sqreuopltb  26300  2sqreuopnnlt  26301  2sqreuopnnltb  26302  dchrisumlem3  26326  dchrmusumlema  26328  dchrmusum2  26329  dchrvmasumlem2  26333  dchrvmasumlema  26335  dchrvmasumiflem1  26336  dchrisum0flblem2  26344  dchrisum0flb  26345  dchrisum0lema  26349  dchrisum0lem1b  26350  dchrisum0lem2  26353  pntrlog2bndlem2  26413  pntibndlem2  26426  pntlemf  26440  ostth2lem1  26453  qabvle  26460  legso  26644  iscgra  26854  isleag  26892  iseqlg  26912  brbtwn2  26950  axlowdim  27006  ewlksfval  27643  isnvlem  28645  nvtri  28705  nmlnoubi  28831  nmblolbii  28834  nmblolbi  28835  blocnilem  28839  sii  28889  ubthlem2  28906  minvecolem3  28911  minvecolem5  28916  minvecolem6  28917  norm-ii  29173  norm3dif  29185  norm3adifi  29188  bcs  29216  pjnorm  29759  pjnel  29761  nmbdoplbi  30059  nmbdoplb  30060  nmcoplb  30065  lnconi  30068  nmbdfnlb  30085  nmcfnlb  30089  pjdifnormi  30202  mdslmd2i  30365  cvmd  30371  cvexch  30409  cdj1i  30468  cdj3lem1  30469  cdj3lem2b  30472  cdj3lem3b  30475  cdj3i  30476  isoun  30708  ismnt  30934  mgcmntco  30945  dfmgc2lem  30946  dfmgc2  30947  mgcf1o  30954  isomnd  31000  omndadd  31005  omndmul  31013  ogrpinvlt  31022  gsumle  31023  isinftm  31108  xrmulc1cn  31548  lmdvg  31571  nexple  31643  faeval  31880  brfae  31882  inelcarsg  31944  carsgsigalem  31948  carsgclctunlem2  31952  carsgclctun  31954  hgt750lemc  32293  hgt750lemd  32294  hgt749d  32295  sconnpht  32858  snmlval  32960  satfv1lem  32991  satfv1  32992  satfv0fun  33000  satfv0fvfmla0  33042  lediv2aALT  33302  faclim  33381  poseq  33482  sltval2  33545  sltres  33551  nolesgn2o  33560  nogesgn1o  33562  nodense  33581  nolt02o  33584  nogt01o  33585  noresle  33586  nosupbnd2lem1  33604  nosupbnd2  33605  noinfbnd2lem1  33619  noinfbnd2  33620  fvtransport  34020  idinside  34072  btwnconn1lem7  34081  btwnconn1lem11  34085  btwnconn1lem12  34086  nn0prpwlem  34197  bj-opabco  35043  poimirlem29  35492  heicant  35498  itg2addnclem  35514  itg2addnclem3  35516  itg2gt0cn  35518  ftc1anclem6  35541  ftc1anc  35544  ftc2nc  35545  dvasin  35547  areacirclem1  35551  seqpo  35591  incsequz  35592  metf1o  35599  mettrifi  35601  cntotbnd  35640  heiborlem4  35658  heiborlem6  35660  heiborlem10  35664  bfplem1  35666  bfplem2  35667  isopos  36880  oplecon3b  36900  atlatle  37020  4at2  37314  pmaple  37461  islaut  37783  lautcnvle  37789  lautco  37797  ltrncnvel  37842  cdlemeg49lebilem  38239  cdlemg17h  38368  tendoset  38459  tendotp  38461  cdlemk39s  38639  lcmineqlem23  39742  lcmineqlem  39743  intlewftc  39752  aks4d1p1p4  39761  dvle2  39762  2ap1caineq  39770  sticksstones1  39771  sticksstones2  39772  sticksstones3  39773  sticksstones8  39778  sticksstones10  39780  sticksstones11  39781  sticksstones12a  39782  sticksstones15  39786  factwoffsmonot  39826  brif12  39854  dvdsexpnn0  39990  dvdsexpb  39991  reltsub1  40018  irrapxlem2  40289  irrapxlem4  40291  irrapxlem5  40292  irrapxlem6  40293  pellexlem3  40297  monotuz  40407  monotoddzzfi  40408  monotoddzz  40409  jm2.17a  40426  jm2.17b  40427  rmygeid  40430  rmydioph  40480  expdiophlem1  40487  expdiophlem2  40488  ttac  40502  fnwe2lem2  40520  relexp01min  40939  cvgdvgrat  41545  monoords  42450  supxrgelem  42490  supxrge  42491  abslt2sqd  42513  ltmulneg  42546  ltdiv23neg  42548  monoordxrv  42638  monoordxr  42639  monoord2xrv  42640  monoord2xr  42641  evthiccabs  42650  sqrlearg  42707  climinf  42765  climinff  42770  limsupres  42864  climinf2  42866  climinf2mpt  42873  climinfmpt  42874  supcnvlimsup  42899  liminfval2  42927  liminflelimsuplem  42934  liminfltlem  42963  fprodsubrecnncnvlem  43066  fprodaddrecnncnvlem  43068  ioodvbdlimc1lem1  43090  ioodvbdlimc1lem2  43091  ioodvbdlimc2lem  43093  iblspltprt  43132  itgspltprt  43138  stoweidlem3  43162  fourierdlem2  43268  fourierdlem3  43269  fourierdlem11  43277  fourierdlem12  43278  fourierdlem15  43281  fourierdlem34  43300  fourierdlem41  43307  fourierdlem48  43313  fourierdlem49  43314  fourierdlem79  43344  fourierdlem83  43348  fourierdlem89  43354  fourierdlem91  43356  fourierdlem100  43365  fourierdlem107  43372  fourierdlem109  43374  fourierdlem112  43377  etransclem31  43424  etransclem32  43425  rrndistlt  43449  ioorrnopn  43464  ioorrnopnxrlem  43465  sge0less  43548  sge0le  43563  sge0split  43565  sge0lempt  43566  sge0iunmptlemre  43571  sge0isum  43583  sge0seq  43602  meaiuninclem  43636  meaiininclem  43642  meaiininc  43643  isome  43650  omeunile  43661  omeiunlempt  43676  carageniuncllem2  43678  0ome  43685  isomenndlem  43686  isomennd  43687  ovnsslelem  43716  ovnssle  43717  ovnsubadd  43728  hsphoidmvle2  43741  hsphoidmvle  43742  hoidmvval0  43743  hoidmv1lelem1  43747  hoidmv1lelem2  43748  hoidmv1lelem3  43749  hoidmv1le  43750  hoidmvlelem1  43751  hoidmvlelem2  43752  hoidmvlelem3  43753  hoidmvlelem4  43754  hoidmvlelem5  43755  hoidmvle  43756  hoidifhspdmvle  43776  hspmbllem2  43783  hspmbl  43785  ovnsubadd2lem  43801  ovolval4lem2  43806  ovolval4  43807  ovolval5lem2  43809  vonioolem2  43837  vonioo  43838  vonicclem2  43840  vonicc  43841  smfid  43903  smflimlem3  43923  2elfz2melfz  44426  smonoord  44439  iccpart  44484  iccpartimp  44485  iccpartres  44486  sqrtpwpw2p  44606  ismgmALT  45033  iscmgmALT  45034  issgrpALT  45035  iscsgrpALT  45036  lindslinindsimp2lem5  45419  rrx2plordisom  45685  aacllem  46119