Theorem breq12d 5132

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

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

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707

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 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-br 5120

This theorem is referenced by:  breq123d  5133  3brtr3d  5150  3brtr4d  5151  sbcbr  5174  pocl  5569  csbcnvgALT  5864  cnvpo  6276  sbcfung  6559  isoeq1  7309  isocnv  7322  isotr  7328  caovordig  7610  caovordg  7612  caovord2d  7614  caovord  7616  ofrfvalg  7677  ofrval  7681  ofrfval2  7690  caofref  7700  fnwelem  8128  poseq  8155  fundmeng  9044  enrefnn  9059  xpsneng  9068  xpcomeng  9076  xpdom2g  9080  limensuc  9166  infensuc  9167  pssnn  9180  unxpdom  9259  dif1ennnALT  9281  unfilem3  9315  fodomfi  9320  domunfican  9331  fodomfiOLD  9340  marypha1lem  9443  infsupprpr  9516  wemaplem1  9558  wemaplem2  9559  wemapwe  9709  ssttrcl  9727  ttrcltr  9728  ttrclss  9732  dmttrcl  9733  rnttrcl  9734  ttrclselem2  9738  dif1card  10022  infxpenlem  10025  nnadju  10210  pwsdompw  10215  infmap2  10229  sornom  10289  isfin5  10311  isfin6  10312  domtriomlem  10454  axdc2lem  10460  axdclem2  10532  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  11702  leadd2  11704  ltmul2  12090  lemul2  12092  lemul1a  12093  ltdiv1  12104  ltdiv2  12126  lediv2  12130  div4p1lem1div2  12494  nn0ledivnn  13120  xleadd1  13269  xltadd2  13271  xsubge0  13275  xlemul1a  13302  xlemul1  13304  xlemul2  13305  xltmul2  13307  ltdifltdiv  13849  fzennn  13984  monoord  14048  monoord2  14049  expmordi  14183  ltexp2r  14189  leexp1a  14191  sqlecan  14225  bernneq  14245  faclbnd  14306  faclbnd3  14308  faclbnd4lem1  14309  faclbnd4lem2  14310  faclbnd4lem3  14311  faclbnd4lem4  14312  faclbnd6  14315  facubnd  14316  rlimcld2  15592  isercoll2  15683  climsup  15684  iseraltlem2  15697  fsumabs  15815  fsumrlim  15825  climcndslem1  15863  climcndslem2  15864  supcvg  15870  geomulcvg  15890  cvgrat  15897  ntrivcvgtail  15914  ruclem2  16248  ruclem8  16253  addmodlteqALT  16342  fproddvdsd  16352  sadcaddlem  16474  sadcadd  16475  nn0seqcvgd  16587  algcvg  16593  algcvga  16596  eucalgcvga  16603  isprm5  16724  qnumgt0  16767  pcprendvds2  16859  pcpremul  16861  pcadd2  16908  prmreclem4  16937  prmreclem5  16938  prmreclem6  16939  2expltfac  17110  xpsle  17591  mreexexlemd  17654  issubc  17846  latjlej2  18462  latmlem2  18478  sylow1lem3  19579  isslw  19587  fislw  19604  efgi  19698  lt6abl  19874  ablfac1eu  20054  isabv  20769  abvtri  20780  psdmul  22102  cayleyhamilton1  22828  isucn  24214  ispsmet  24241  psmettri2  24246  ismet  24260  isxmet  24261  xmettri2  24277  imasdsf1olem  24310  imasf1oxmet  24312  blvalps  24322  blval  24323  comet  24450  stdbdxmet  24452  nrmmetd  24511  tngngp  24591  tngngp3  24593  nmofval  24651  nmolb2d  24655  nmoi  24665  nmoix  24666  icopnfhmeo  24890  xrhmeo  24893  evth2  24908  pi1grplem  24998  minveclem6  25384  ovolfiniun  25452  ovoliunlem3  25455  voliunlem3  25503  ioombl1  25513  mbfmax  25600  mbfpos  25602  itg1climres  25665  mbfi1fseqlem2  25667  mbfi1fseqlem6  25671  mbfi1fseq  25672  mbfmullem  25676  itg2split  25700  itg2monolem1  25701  itg2monolem3  25703  itg2mono  25704  itg2i1fseqle  25705  itg2i1fseq  25706  itg2i1fseq2  25707  itg2addlem  25709  rolle  25944  dvlip  25948  c1lip1  25952  dvcnvrelem1  25972  dvcvx  25975  ply1divex  26092  q1pval  26110  fta1glem2  26124  fta1g  26125  fta1b  26127  plydivlem3  26253  fta1lem  26265  fta1  26266  aalioulem3  26292  aalioulem4  26293  aaliou3lem2  26301  aaliou3lem8  26303  aaliou3lem9  26308  ulmdvlem1  26359  ulmdvlem3  26361  abelthlem2  26392  abelthlem7a  26397  argrege0  26570  cxplt  26653  cxplea  26655  cxple2  26656  cxplt3  26659  logbleb  26743  logblt  26744  rlimcxp  26934  scvxcvx  26946  jensenlem2  26948  ftalem3  27035  ftalem7  27039  vmalelog  27166  chtub  27173  chpchtsum  27180  bclbnd  27241  efexple  27242  bposlem5  27249  bposlem6  27250  bposlem7  27251  lgsdilem  27285  2lgslem1a2  27351  2sqreuop  27423  2sqreuopnn  27424  2sqreuoplt  27425  2sqreuopltb  27426  2sqreuopnnlt  27427  2sqreuopnnltb  27428  dchrisumlem3  27452  dchrmusumlema  27454  dchrmusum2  27455  dchrvmasumlem2  27459  dchrvmasumlema  27461  dchrvmasumiflem1  27462  dchrisum0flblem2  27470  dchrisum0flb  27471  dchrisum0lema  27475  dchrisum0lem1b  27476  dchrisum0lem2  27479  pntrlog2bndlem2  27539  pntibndlem2  27552  pntlemf  27566  ostth2lem1  27579  qabvle  27586  sltval2  27618  sltres  27624  nolesgn2o  27633  nogesgn1o  27635  nodense  27654  nolt02o  27657  nogt01o  27658  noresle  27659  nosupbnd2lem1  27677  nosupbnd2  27678  noinfbnd2lem1  27692  noinfbnd2  27693  addsproplem1  27919  addsprop  27926  sltadd2im  27936  sleadd2im  27938  sleadd1  27939  sleadd2  27940  sltadd1  27942  sltsub1  28023  sltsub2  28024  sltsubsubbd  28030  sltsubsub2bd  28031  posdifsd  28044  subsge0d  28046  mulsproplemcbv  28058  mulsproplem1  28059  mulsprop  28073  slemuld  28081  sltmul1d  28116  sltmulneg1d  28119  sltmulneg2d  28120  slemul1ad  28125  legso  28524  iscgra  28734  isleag  28772  iseqlg  28792  brbtwn2  28830  axlowdim  28886  ewlksfval  29527  isnvlem  30537  nvtri  30597  nmlnoubi  30723  nmblolbii  30726  nmblolbi  30727  blocnilem  30731  sii  30781  ubthlem2  30798  minvecolem3  30803  minvecolem5  30808  minvecolem6  30809  norm-ii  31065  norm3dif  31077  norm3adifi  31080  bcs  31108  pjnorm  31651  pjnel  31653  nmbdoplbi  31951  nmbdoplb  31952  nmcoplb  31957  lnconi  31960  nmbdfnlb  31977  nmcfnlb  31981  pjdifnormi  32094  mdslmd2i  32257  cvmd  32263  cvexch  32301  cdj1i  32360  cdj3lem1  32361  cdj3lem2b  32364  cdj3lem3b  32367  cdj3i  32368  isoun  32625  nexple  32769  ismnt  32909  mgcmntco  32920  dfmgc2lem  32921  dfmgc2  32922  mgcf1o  32929  ischn  32932  chnltm1  32934  chnind  32937  chnub  32938  isomnd  33015  omndadd  33020  omndmul  33028  ogrpinvlt  33037  gsumle  33038  isinftm  33125  rlocaddval  33209  rlocmulval  33210  fldext2chn  33708  constrextdg2lem  33728  constrext2chn  33739  xrmulc1cn  33907  lmdvg  33930  faeval  34223  brfae  34225  inelcarsg  34289  carsgsigalem  34293  carsgclctunlem2  34297  carsgclctun  34299  hgt750lemc  34625  hgt750lemd  34626  hgt749d  34627  sconnpht  35197  snmlval  35299  satfv1lem  35330  satfv1  35331  satfv0fun  35339  satfv0fvfmla0  35381  lediv2aALT  35645  faclim  35709  fvtransport  35996  idinside  36048  btwnconn1lem7  36057  btwnconn1lem11  36061  btwnconn1lem12  36062  ditgeq123dv  36185  cbvditgdavw2  36262  nn0prpwlem  36286  weiunlem1  36426  weiunfrlem  36428  bj-opabco  37152  poimirlem29  37619  heicant  37625  itg2addnclem  37641  itg2addnclem3  37643  itg2gt0cn  37645  ftc1anclem6  37668  ftc1anc  37671  ftc2nc  37672  dvasin  37674  areacirclem1  37678  seqpo  37717  incsequz  37718  metf1o  37725  mettrifi  37727  cntotbnd  37766  heiborlem4  37784  heiborlem6  37786  heiborlem10  37790  bfplem1  37792  bfplem2  37793  isopos  39144  oplecon3b  39164  atlatle  39284  4at2  39579  pmaple  39726  islaut  40048  lautcnvle  40054  lautco  40062  ltrncnvel  40107  cdlemeg49lebilem  40504  cdlemg17h  40633  tendoset  40724  tendotp  40726  cdlemk39s  40904  lcmineqlem23  42010  lcmineqlem  42011  intlewftc  42020  aks4d1p1p4  42030  dvle2  42031  aks4d1p8d2  42044  aks4d1p9  42047  aks4d1  42048  2ap1caineq  42104  sticksstones1  42105  sticksstones2  42106  sticksstones3  42107  sticksstones8  42112  sticksstones10  42114  sticksstones11  42115  sticksstones12a  42116  sticksstones15  42120  aks6d1c7lem3  42141  unitscyglem1  42154  factwoffsmonot  42201  brif12  42222  dvdsexpnn0  42330  dvdsexpb  42331  reltsub1  42376  irrapxlem2  42793  irrapxlem4  42795  irrapxlem5  42796  irrapxlem6  42797  pellexlem3  42801  monotuz  42912  monotoddzzfi  42913  monotoddzz  42914  jm2.17a  42931  jm2.17b  42932  rmygeid  42935  rmydioph  42985  expdiophlem1  42992  expdiophlem2  42993  ttac  43007  fnwe2lem2  43022  relexp01min  43684  cvgdvgrat  44285  relpeq1  44917  monoords  45274  supxrgelem  45312  supxrge  45313  abslt2sqd  45335  ltmulneg  45367  ltdiv23neg  45369  monoordxrv  45456  monoordxr  45457  monoord2xrv  45458  monoord2xr  45459  evthiccabs  45473  sqrlearg  45530  climinf  45583  climinff  45588  limsupres  45682  climinf2  45684  climinf2mpt  45691  climinfmpt  45692  supcnvlimsup  45717  liminfval2  45745  liminfltlem  45781  fprodsubrecnncnvlem  45884  fprodaddrecnncnvlem  45886  ioodvbdlimc1lem1  45908  ioodvbdlimc1lem2  45909  ioodvbdlimc2lem  45911  iblspltprt  45950  itgspltprt  45956  stoweidlem3  45980  fourierdlem2  46086  fourierdlem3  46087  fourierdlem11  46095  fourierdlem12  46096  fourierdlem15  46099  fourierdlem34  46118  fourierdlem41  46125  fourierdlem48  46131  fourierdlem49  46132  fourierdlem79  46162  fourierdlem83  46166  fourierdlem89  46172  fourierdlem91  46174  fourierdlem100  46183  fourierdlem107  46190  fourierdlem109  46192  fourierdlem112  46195  etransclem31  46242  etransclem32  46243  rrndistlt  46267  ioorrnopn  46282  ioorrnopnxrlem  46283  sge0less  46369  sge0le  46384  sge0split  46386  sge0lempt  46387  sge0iunmptlemre  46392  sge0isum  46404  sge0seq  46423  meaiuninclem  46457  meaiininclem  46463  meaiininc  46464  isome  46471  omeunile  46482  omeiunlempt  46497  carageniuncllem2  46499  0ome  46506  isomenndlem  46507  isomennd  46508  ovnssle  46538  ovnsubadd  46549  hsphoidmvle2  46562  hsphoidmvle  46563  hoidmvval0  46564  hoidmv1lelem1  46568  hoidmv1lelem2  46569  hoidmv1lelem3  46570  hoidmv1le  46571  hoidmvlelem1  46572  hoidmvlelem2  46573  hoidmvlelem3  46574  hoidmvlelem4  46575  hoidmvlelem5  46576  hoidmvle  46577  hoidifhspdmvle  46597  hspmbllem2  46604  hspmbl  46606  ovnsubadd2lem  46622  ovolval4lem2  46627  ovolval4  46628  ovolval5lem2  46630  vonioolem2  46658  vonioo  46659  vonicclem2  46661  vonicc  46662  smfid  46729  smflimlem3  46750  ormkglobd  46852  natglobalincr  46854  tworepnotupword  46863  squeezedltsq  46866  2elfz2melfz  47295  smonoord  47333  iccpart  47378  iccpartimp  47379  iccpartres  47380  sqrtpwpw2p  47500  grlicsym  47966  grlictr  47968  ismgmALT  48146  iscmgmALT  48147  issgrpALT  48148  iscsgrpALT  48149  lindslinindsimp2lem5  48386  rrx2plordisom  48651  aacllem  49613